Section 7 hypercube graph: Fourier basis

Additive characters and the Fourier basis of ℂ^{F_q^m} used to diagonalize the hypercube adjacency matrix K.

References

• references/ldt-paper/expansion.tex
• blueprint/src/chapter/ch05_expansion.tex

Fourier analysis on the hypercube F_q^m

The Fourier basis of ℂ^{F_q^m} consists of the character vectors φ_α(u) = (1/√M) · ω^{⟨u, α⟩} for α ∈ F_q^m, where ω = exp(2πi/q) and ⟨u, α⟩ = ∑ᵢ uᵢ · αᵢ (mod q).

These are eigenvectors of the adjacency matrix K with known eigenvalues (prop:eigenvectors in the paper).

noncomputable def MIPStarRE.LDT.ExpansionHypercubeGraph.addCharFq (params : Parameters) (a : Fq params) : ℂ

The additive character χ_q : F_q → ℂ sending a ↦ exp(2πi · a / q).

Equations

• MIPStarRE.LDT.ExpansionHypercubeGraph.addCharFq params a = Complex.exp (2 * ↑Real.pi * Complex.I * ↑↑a / ↑params.q)

def MIPStarRE.LDT.ExpansionHypercubeGraph.dotProductFq (params : Parameters) (u α : Point params) : Fq params

The dot product ⟨u, α⟩ = ∑ᵢ uᵢ · αᵢ in F_q, computed via natural number arithmetic and reduced mod q.

Equations

• MIPStarRE.LDT.ExpansionHypercubeGraph.dotProductFq params u α = ⟨(∑ i : Fin params.m, ↑(u i) * ↑(α i)) % params.q, ⋯⟩

noncomputable def MIPStarRE.LDT.ExpansionHypercubeGraph.fourierBasisState (params : Parameters) (α : Point params) : Point params → ℂ

The Fourier basis vector φ_α : Point params → ℂ, defined by φ_α(u) = (1/√M) · exp(2πi ⟨u, α⟩ / q).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPStarRE.LDT.ExpansionHypercubeGraph.dotProductZMod (params : Parameters) (u α : Point params) : ZMod params.q

The same dot product as dotProductFq, but computed directly in ZMod q.

Equations

• MIPStarRE.LDT.ExpansionHypercubeGraph.dotProductZMod params u α = ∑ i : Fin params.m, ↑↑(u i) * ↑↑(α i)

theorem MIPStarRE.LDT.ExpansionHypercubeGraph.addCharFq_eq_stdAddChar (params : Parameters) (a : Fq params) : addCharFq params a = ZMod.stdAddChar ↑↑a

theorem MIPStarRE.LDT.ExpansionHypercubeGraph.addCharFq_dotProduct_eq_stdAddChar_dotProductZMod (params : Parameters) (u α : Point params) : addCharFq params (dotProductFq params u α) = ZMod.stdAddChar (dotProductZMod params u α)

theorem MIPStarRE.LDT.ExpansionHypercubeGraph.dotProductZMod_update (params : Parameters) (u α : Point params) (i : Fin params.m) (x : Fq params) : dotProductZMod params (Function.update u i x) α = dotProductZMod params u α + (↑↑x - ↑↑(u i)) * ↑↑(α i)

theorem MIPStarRE.LDT.ExpansionHypercubeGraph.sum_stdAddChar_mul_fin (params : Parameters) (a : ZMod params.q) : ∑ x : Fq params, ZMod.stdAddChar (↑↑x * a) = ↑(if a = 0 then params.q else 0)

theorem MIPStarRE.LDT.ExpansionHypercubeGraph.fourierBasisState_update_sum (params : Parameters) (u α : Point params) (i : Fin params.m) : ∑ x : Fq params, fourierBasisState params α (Function.update u i x) = ↑(if α i = 0 then params.q else 0) * fourierBasisState params α u

noncomputable def MIPStarRE.LDT.ExpansionHypercubeGraph.fourierBasisProjector (params : Parameters) (α : Point params) : Quantum.Op (Point params)

The Fourier basis projector |φ_α⟩⟨φ_α| as a matrix on Point params.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPStarRE.LDT.ExpansionHypercubeGraph.localVarianceTraceWitness {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) (A : Point params → Quantum.Op ι) (ψ : QuantumState ι) : Quantum.Op ι

Paper origin: references/ldt-paper/expansion.tex:145-154 (\label{lem:local-rewrite}); trace witness for the local-variance rewrite.

Equations

• One or more equations did not get rendered due to their size.

structure MIPStarRE.LDT.ExpansionHypercubeGraph.GlobalVarianceDecomposition {ι : Type u_1} (params : Parameters) (A : Point params → Quantum.Op ι) : Type u_1

A packaged decomposition for lem:global-rewrite.

The Lean witness stores the pointwise average A_avg = E_u A^u together with the full residual family u ↦ A^u - A_avg. This carries the same geometric content as writing A_combine = |φ₀⟩ ⊗ A₀ + |φ_⊥⟩ ⊗ A_⊥, but it does not force the orthogonal part to be rank one on Point params ⊗ ι.

• averageComponent : Quantum.Op ι
• orthogonalComponent : Point params → Quantum.Op ι
• averageComponent_eq : self.averageComponent = (↑(hypercubeVertexCount params))⁻¹ • ∑ u : Point params, A u
• orthogonal_sum_zero : ∑ u : Point params, self.orthogonalComponent u = 0
• decomposition (u : Point params) : A u = self.averageComponent + self.orthogonalComponent u

theorem MIPStarRE.LDT.ExpansionHypercubeGraph.GlobalVarianceDecomposition.orthogonalComponent_eq_sub_average {ι : Type u_1} {params : Parameters} {A : Point params → Quantum.Op ι} (decomp : GlobalVarianceDecomposition params A) (u : Point params) : decomp.orthogonalComponent u = A u - decomp.averageComponent

Recover the centered residual as A^u - A_avg.

noncomputable def MIPStarRE.LDT.ExpansionHypercubeGraph.canonicalGlobalVarianceDecomposition {ι : Type u_1} (params : Parameters) (A : Point params → Quantum.Op ι) : GlobalVarianceDecomposition params A

The canonical decomposition from lem:global-rewrite.

Its averageComponent is the paper's A_avg = E_u A^u = (1/M) · ∑_u A^u, and its orthogonal component is the centered family u ↦ A^u - A_avg. Equivalently, the paper's coefficient A_0 = M^{-1/2} · ∑_u A^u is M^{1/2} · A_avg.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPStarRE.LDT.ExpansionHypercubeGraph.globalVarianceTraceWitness {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) (A : Point params → Quantum.Op ι) (ψ : QuantumState ι) (decomp : GlobalVarianceDecomposition params A) : Quantum.Op ι

Paper origin: references/ldt-paper/expansion.tex:179-190 (\label{lem:global-rewrite}); trace witness for the global-variance rewrite. This uses the orthogonal residual family supplied by the decomposition.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPStarRE.LDT.ExpansionHypercubeGraph.localVarianceTraceForm {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) (A : Point params → Quantum.Op ι) (ψ : QuantumState ι) : Error

The local-variance trace expression from lem:local-rewrite.

Equations

• MIPStarRE.LDT.ExpansionHypercubeGraph.localVarianceTraceForm params A ψ = (MIPStarRE.Quantum.normalizedTrace (MIPStarRE.LDT.ExpansionHypercubeGraph.localVarianceTraceWitness params A ψ)).re

noncomputable def MIPStarRE.LDT.ExpansionHypercubeGraph.globalVarianceTraceForm {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) (A : Point params → Quantum.Op ι) (ψ : QuantumState ι) (decomp : GlobalVarianceDecomposition params A) : Error

The global-variance trace expression from lem:global-rewrite.

The prefactor 1 / hypercubeVertexCount params is the paper's 1 / M normalization from Section 7.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPStarRE.LDT.ExpansionHypercubeGraph.frequencyWeight (params : Parameters) (α : Point params) : ℕ

The number of nonzero coordinates of a frequency α ∈ F_q^m.

Equations

• MIPStarRE.LDT.ExpansionHypercubeGraph.frequencyWeight params α = {i : Fin params.m | α i ≠ ⟨0, ⋯⟩}.card

theorem MIPStarRE.LDT.ExpansionHypercubeGraph.frequencyWeight_le_m (params : Parameters) (α : Point params) : frequencyWeight params α ≤ params.m

The number of nonzero coordinates of α is at most m.

theorem MIPStarRE.LDT.ExpansionHypercubeGraph.zeroCoordinateCount_eq (params : Parameters) (α : Point params) : {i : Fin params.m | α i = 0}.card = params.m - frequencyWeight params α

theorem MIPStarRE.LDT.ExpansionHypercubeGraph.zeroCoordinateContributionSum (params : Parameters) (α : Point params) : ∑ i : Fin params.m, ↑(if α i = 0 then params.q else 0) = ↑(params.m - frequencyWeight params α) * ↑params.q

theorem MIPStarRE.LDT.ExpansionHypercubeGraph.fourierBasisState_total_update_sum (params : Parameters) (u α : Point params) : ∑ i : Fin params.m, ∑ x : Fq params, fourierBasisState params α (Function.update u i x) = ↑(params.m - frequencyWeight params α) * ↑params.q * fourierBasisState params α u

noncomputable def MIPStarRE.LDT.ExpansionHypercubeGraph.fourierBasisInnerProduct (params : Parameters) (α β : Point params) : ℂ

The actual inner product of two Fourier basis states on ℂ^{F_q^m}.

Since fourierBasisState already includes the 1 / √M normalization, this is just the finite sum ∑_u conj(φ_α(u)) * φ_β(u).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPStarRE.LDT.ExpansionHypercubeGraph.pointAddChar (params : Parameters) (α : Point params) : AddChar (Point params) ℂ

The additive character on Point params indexed by a frequency α.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPStarRE.LDT.ExpansionHypercubeGraph.pointAddCharRight (params : Parameters) (u : Point params) : AddChar (Point params) ℂ

The additive character on the frequency space obtained by fixing a point u.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPStarRE.LDT.ExpansionHypercubeGraph.dotProductZMod_single_one (params : Parameters) (α : Point params) (i : Fin params.m) : dotProductZMod params (Function.update 0 i ⟨1 % params.q, ⋯⟩) α = ↑↑(α i)

Updating the zero point at coordinate i with the field element 1 yields the standard basis vector e_i, whose ZMod q dot product with α is the i-th coordinate of α.

theorem MIPStarRE.LDT.ExpansionHypercubeGraph.pointAddChar_eq_zero_iff (params : Parameters) (α : Point params) : pointAddChar params α = 0 ↔ α = 0

pointAddChar params α is trivial exactly when α = 0.

Here the 0 on the left is the Zero instance on AddChar, i.e. the trivial character u ↦ 1, not the pointwise-zero function.

theorem MIPStarRE.LDT.ExpansionHypercubeGraph.fourierBasisState_inner_product (params : Parameters) (α β : Point params) : ∑ u : Point params, star (fourierBasisState params α u) * fourierBasisState params β u = if α = β then 1 else 0

The actual Fourier inner product equals the Kronecker delta. This proves ∑_u conj(φ_α(u)) * φ_β(u) = if α = β then 1 else 0.

theorem MIPStarRE.LDT.ExpansionHypercubeGraph.eigenvectors_orthonormality (params : Parameters) (α β : Point params) : fourierBasisInnerProduct params α β = if α = β then 1 else 0

prop:eigenvectors, item 1: orthonormality of the Fourier basis.

noncomputable def MIPStarRE.LDT.ExpansionHypercubeGraph.adjacencyEigenvalue (params : Parameters) (α : Point params) : Error

The eigenvalue of K on φ_α.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPStarRE.LDT.ExpansionHypercubeGraph.laplacianEigenvalue (params : Parameters) (α : Point params) : Error

The eigenvalue of L on φ_α.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPStarRE.LDT.ExpansionHypercubeGraph.hypercubeSpectralGap (params : Parameters) : Error

The spectral gap 1 / (m M) from cor:laplacian-spectral-gap.

Equations

• MIPStarRE.LDT.ExpansionHypercubeGraph.hypercubeSpectralGap params = 1 / (↑params.m * ↑(MIPStarRE.LDT.ExpansionHypercubeGraph.hypercubeVertexCount params))

theorem MIPStarRE.LDT.ExpansionHypercubeGraph.eigenvectors_card (params : Parameters) : Fintype.card (Point params) = hypercubeVertexCount params

The Fourier index set F_q^m has cardinality M = q^m.

theorem MIPStarRE.LDT.ExpansionHypercubeGraph.eigenvectors (params : Parameters) (α : Point params) : Matrix.mulVec (matrixAdjacencyOperator params) (fourierBasisState params α) = ↑(adjacencyEigenvalue params α) • fourierBasisState params α

prop:eigenvectors, item 2: each |φ_α⟩ is an eigenvector of the adjacency matrix K with eigenvalue λ_α.

theorem MIPStarRE.LDT.ExpansionHypercubeGraph.laplacianEigenvalue_eq (params : Parameters) (α : Point params) : laplacianEigenvalue params α = 1 / ↑(hypercubeVertexCount params) - adjacencyEigenvalue params α

cor:laplacian-spectral-gap, eigenvalue relation: λ_L(α) = 1/M − λ_K(α).

theorem MIPStarRE.LDT.ExpansionHypercubeGraph.hypercubeSpectralGap_le_laplacianEigenvalue (params : Parameters) (α : Point params) (hα : 0 < frequencyWeight params α) : hypercubeSpectralGap params ≤ laplacianEigenvalue params α

cor:laplacian-spectral-gap, spectral gap bound: for α ≠ 0, the spectral gap 1/(mM) lower-bounds the Laplacian eigenvalue λ_L(α).

theorem MIPStarRE.LDT.ExpansionHypercubeGraph.laplacianEigenvalue_of_weight_one (params : Parameters) (α : Point params) (hα : frequencyWeight params α = 1) : laplacianEigenvalue params α = hypercubeSpectralGap params

cor:laplacian-spectral-gap, attainment: for |α| = 1, the spectral gap is attained: λ_L(α) = 1/(mM).