Documentation

CsdLean4.Mathlib.QuantumInfo.Fourier

Quantum Fourier transform and its unitarity (R5) #

Category: 1-Mathlib (CSD-free).

Glossary: https://glossary.constraintsurfacedynamics.com/quantum-fourier-transform/ Plain-language, CSD-role and formal statements of the QFT, with this module as its Lean anchor. Kept symmetric by scripts/check-glossary.sh.

Phase R5 of specs/nqubit-register-plan.md: the quantum Fourier transform on N levels, as the N × N matrix

F j k = (1/√N) · ω^{jk}, ω = exp(2πi/N) a primitive N-th root of unity,

and the key fact that it is unitary (qft_unitary, Fᴴ * F = 1). Entrywise the unitary identity reads

(Fᴴ F) j j' = (1/N) ∑ₖ ω^{k(j'-j)} = [j = j'],

i.e. the roots-of-unity orthogonality ∑_{k=0}^{N-1} ζ^k = N·[ζ=1] (a geometric series), which is the ℂ-analogue of the ±1-character orthogonality behind the Hadamard transform (R3). The QFT is a finite N × N unitary; nothing here leaves the finite-dimensional setting.

The transform is defined on a general level count N (not specialised to N = 2ⁿ), so it is directly the discrete Fourier unitary; the qubit instance is the N = 2ⁿ case.

source
noncomputable def QuantumInfo.qftω (N : ℕ) :
ℂ

The primitive N-th root of unity ω = exp(2πi/N).

Equations
Instances For
    source
    theorem QuantumInfo.qftω_primitive (N : ℕ) [NeZero N] :
    IsPrimitiveRoot (qftω N) N

    ω is a primitive N-th root of unity.

    source
    theorem QuantumInfo.qftω_pow_N (N : ℕ) [NeZero N] :
    qftω N ^ N = 1

    ωᴺ = 1.

    source
    theorem QuantumInfo.qftω_ne_zero (N : ℕ) :
    qftω N ≠ 0

    ω is nonzero (a value of exp).

    source
    theorem QuantumInfo.qftω_conj (N : ℕ) :
    (starRingEnd ℂ) (qftω N) = (qftω N)⁻¹

    ω is unimodular: conjugation inverts it.

    source
    theorem QuantumInfo.sqrtN_mul_self (N : ℕ) :
    ↑√↑N * ↑√↑N = ↑N

    √N · √N = N over ℂ.

    source
    theorem QuantumInfo.inv_sqrtN_sq (N : ℕ) :
    (↑√↑N)⁻¹ * (↑√↑N)⁻¹ = (↑N)⁻¹

    (√N)⁻¹ · (√N)⁻¹ = N⁻¹.

    source
    noncomputable def QuantumInfo.qftMatrix (N : ℕ) :
    Matrix (Fin N) (Fin N) ℂ

    The quantum Fourier transform as an N × N matrix: F j k = (1/√N) ω^{jk}.

    Equations
    Instances For
      source
      @[simp]
      theorem QuantumInfo.qftMatrix_apply (N : ℕ) (j k : Fin N) :
      qftMatrix N j k = (↑√↑N)⁻¹ * qftω N ^ (↑j * ↑k)
      source
      theorem QuantumInfo.qftMatrix_symm (N : ℕ) (j k : Fin N) :
      qftMatrix N j k = qftMatrix N k j

      The QFT matrix is symmetric (Fᵀ = F), since jk = kj.

      source
      theorem QuantumInfo.qft_unitary (N : ℕ) [NeZero N] :
      (qftMatrix N).conjTranspose * qftMatrix N = 1

      The quantum Fourier transform is unitary: Fᴴ * F = 1. The entrywise identity is the roots-of-unity orthogonality (1/N) ∑ₖ ω^{k(j'-j)} = [j = j'], a geometric series that vanishes for j ≠ j' and sums to N for j = j'.