Quantum Fourier Transform

The quantum Fourier transform (QFT) on n qubits is the 2^n × 2^n unitary matrix mapping computational basis states to Fourier basis states [dW19, qcnotes.tex:1692; Lin22, phaseestimation.tex:351]:

QFT |x⟩ = (1/√N) Σ_{y=0}^{N-1} ω^{xy} |y⟩

where N = 2^n and ω = e^{2πi/N} is the primitive N-th root of unity.

Conventions

• Sign: forward transform uses ω = e^{+2πi/N} (standard physics sign convention, matching [dW19, qcnotes.tex:1690] and [Lin22, phaseestimation.tex:349]).
• Normalization: 1/√N prefactor makes the transform unitary.
• Endianness: big-endian, matching LeanPool.LeanQuantumAlg.PureState.

Main definitions

• LeanPool.LeanQuantumAlg.omega n — primitive 2^n-th root of unity e^{2πi/2^n}.
• LeanPool.LeanQuantumAlg.invSqrtN n — normalization factor 1/√(2^n).
• LeanPool.LeanQuantumAlg.QFT n — the QFT gate on n qubits.

Main results

• LeanPool.LeanQuantumAlg.omega_pow_eq_one — ω^(2^n) = 1.
• LeanPool.LeanQuantumAlg.norm_omega — ‖ω‖ = 1.
• LeanPool.LeanQuantumAlg.QFT_apply_ket — component formula for QFT |x⟩.
• LeanPool.LeanQuantumAlg.sum_omega_zpow_eq_zero — full-period geometric sums of nontrivial powers of ω vanish (column orthogonality).
• LeanPool.LeanQuantumAlg.QuantumFourierTransform.main — the QFT is unitary.

Pinned Mathlib API: Complex.exp, Complex.exp_nat_mul, Complex.exp_eq_one_iff, Complex.norm_exp_ofReal_mul_I, Complex.isPrimitiveRoot_exp, Matrix.of_apply, Real.mul_self_sqrt, RCLike.inv_eq_conj, IsPrimitiveRoot.zpow_eq_one_iff_dvd, geom_sum_eq, Fin.sum_univ_eq_sum_range, Int.eq_zero_of_abs_lt_dvd, Int.abs_sub_lt_of_lt_lt, Matrix.mem_unitaryGroup_iff'.

Root of unity

noncomputable def QuantumAlg.omega (n : ℕ) : ℂ

Primitive 2^n-th root of unity: ω_n = e^{2πi/2^n} [dW19, qcnotes.tex:1690]. Forward-transform sign convention (+2πi, not −2πi).

Equations

• QuantumAlg.omega n = Complex.exp (↑(2 * Real.pi / 2 ^ n) * Complex.I)

theorem QuantumAlg.omega_pow_eq_one (n : ℕ) : omega n ^ 2 ^ n = 1

ω_n ^ (2^n) = 1: the root has exact period 2^n.

@[simp]

theorem QuantumAlg.norm_omega (n : ℕ) : ‖omega n‖ = 1

‖ω_n‖ = 1: roots of unity lie on the unit circle.

theorem QuantumAlg.omega_isPrimitiveRoot (n : ℕ) : IsPrimitiveRoot (omega n) (2 ^ n)

omega n is a primitive 2^n-th root of unity.

Normalization

noncomputable def QuantumAlg.invSqrtN (n : ℕ) : ℂ

QFT normalization factor: 1/√(2^n), generalizing PureState.invSqrt2.

Equations

• QuantumAlg.invSqrtN n = (↑√(2 ^ n))⁻¹

@[simp]

theorem QuantumAlg.star_invSqrtN (n : ℕ) : star (invSqrtN n) = invSqrtN n

theorem QuantumAlg.invSqrtN_ne_zero (n : ℕ) : invSqrtN n ≠ 0

@[simp]

theorem QuantumAlg.invSqrtN_mul_self (n : ℕ) : invSqrtN n * invSqrtN n = (↑(2 ^ n))⁻¹

QFT gate

noncomputable def QuantumAlg.QFTMatrix (n : ℕ) : HilbertOperator n

The quantum Fourier transform on n qubits [dW19, qcnotes.tex:1692]. Entry (j, k) = invSqrtN n * ω_n^{j·k}.

Equations

• QuantumAlg.QFTMatrix n = Matrix.of fun (j k : Fin (2 ^ n)) => QuantumAlg.invSqrtN n * QuantumAlg.omega n ^ (↑j * ↑k)

@[simp]

theorem QuantumAlg.QFT_entry (n : ℕ) (j k : Fin (2 ^ n)) : QFTMatrix n j k = invSqrtN n * omega n ^ (↑j * ↑k)

Action on basis kets

theorem QuantumAlg.QFTMatrix_apply_ket_column (n : ℕ) (x i : Fin (2 ^ n)) : QFTMatrix n i x = invSqrtN n * omega n ^ (↑i * ↑x)

Component formula for the QFT acting on a basis ket: (QFT |x⟩)ᵢ = (1/√N) · ω^{i·x} [dW19, qcnotes.tex:1692].

Unitarity

theorem QuantumAlg.omega_ne_zero (n : ℕ) : omega n ≠ 0

@[simp]

theorem QuantumAlg.star_omega (n : ℕ) : star (omega n) = (omega n)⁻¹

star ω_n = ω_n⁻¹: conjugation inverts a point on the unit circle.

theorem QuantumAlg.omega_zpow_eq_one_iff (n : ℕ) (d : ℤ) : omega n ^ d = 1 ↔ ↑(2 ^ n) ∣ d

Integer-power version of periodicity: ω_n ^ d = 1 iff 2^n ∣ d.

theorem QuantumAlg.sum_omega_zpow_eq_zero (n : ℕ) {d : ℤ} (hd : ¬↑(2 ^ n) ∣ d) : ∑ l : Fin (2 ^ n), omega n ^ (↑↑l * d) = 0

Column orthogonality [dW19, qcnotes.tex:1698]: the full-period geometric sum ∑_{l<2^n} ω^{l·d} vanishes when 2^n ∤ d.

theorem QuantumAlg.QFT_mem_unitaryGroup (n : ℕ) : QFTMatrix n ∈ Matrix.unitaryGroup (Fin (2 ^ n)) ℂ

The QFT is unitary [dW19, qcnotes.tex:1696]: columns are normalized and pairwise orthogonal. Entry-by-entry, star (QFT n) * QFT n at (j, k) is invSqrtN² · ∑_l ω^{l·(k−j)}, which sum_omega_zpow_eq_zero collapses to if j = k then 1 else 0.

noncomputable def QuantumAlg.QFT (n : ℕ) : Gate n

The quantum Fourier transform on n qubits as a unitary gate.

Equations

• QuantumAlg.QFT n = QuantumAlg.Gate.ofUnitary (QuantumAlg.QFTMatrix n) ⋯

@[simp]

theorem QuantumAlg.QFT_coe (n : ℕ) : (QFT n).op = QFTMatrix n

Action on basis kets

theorem QuantumAlg.QFT_apply_ket (n : ℕ) (x i : Fin (2 ^ n)) : ((QFT n).apply (PureState.ket x)).vec.ofLp i = invSqrtN n * omega n ^ (↑i * ↑x)

Component formula for the QFT acting on a basis ket: (QFT |x⟩)_i = (1/√N) · ω^{i·x} [dW19, qcnotes.tex:1692].

def QuantumAlg.QFTCircuitProfile (n : ℕ) : CircuitGateProfile

Fixed-circuit gate profile for the standard QFT decomposition: n Hadamard gates, n(n-1)/2 controlled-phase gates, and n/2 final register swaps in this natural-number convention.

Equations

• QuantumAlg.QFTCircuitProfile n = { hadamardGates := n, controlledPhaseGates := n * (n - 1) / 2, swapGates := n / 2 }

theorem QuantumAlg.QFTCircuitProfile_exact (n : ℕ) : (QFTCircuitProfile n).HasExactCounts n (n * (n - 1) / 2) (n / 2)

theorem QuantumAlg.QuantumFourierTransform.main (n : ℕ) (x : Fin (2 ^ n)) : (∀ (i : Fin (2 ^ n)), ((QFT n).apply (PureState.ket x)).vec.ofLp i = invSqrtN n * omega n ^ (↑i * ↑x)) ∧ (QFTCircuitProfile n).HasExactCounts n (n * (n - 1) / 2) (n / 2)

QFT basis action paired with the fixed-circuit gate counts used by the standard decomposition.