Section 7 hypercube graph: the variance decomposition and the trace forms

The counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/ExpansionHypercubeGraph/Defs/Fourier.lean in the port of planning/c6b-plan.md (milestone M5, section "Port conventions").

The Fourier analysis of the vendored file (the additive characters, the Fourier basis of ℂ^{F_q^m}, its orthonormality, and the eigenvalues of the adjacency matrix and the Laplacian) is scalar and is imported, not ported. What is ported is the operator side of lem:local-rewrite and lem:global-rewrite: the decomposition A^u = A_avg + A_⊥^u of an operator family (generic over any complex module, as it uses no product) and the two trace forms. The vendored trace forms are Re τ of a matrix witness A_combineᴴ (P ⊗ ρ) A_combine; here they are the real parts of the sums those traces evaluate to, combinedTraceForm P A V (Defs/Core.lean), at P = L for the local form and at P = 1 on the orthogonal residual for the global one.

Not ported

• addCharFq: classical, imported.
• dotProductFq: classical, imported.
• fourierBasisState: classical, imported.
• dotProductZMod: classical, imported.
• addCharFq_eq_stdAddChar: classical, imported.
• addCharFq_dotProduct_eq_stdAddChar_dotProductZMod: classical, imported.
• dotProductZMod_update: classical, imported.
• sum_stdAddChar_mul_fin: classical, imported.
• fourierBasisState_update_sum: classical, imported.
• fourierBasisProjector: classical (a scalar matrix on the vertices), imported.
• localVarianceTraceWitness: the matrix A_combineᴴ (L ⊗ ρ) A_combine; a vector state has no density, and localVarianceTraceForm is defined by the sum its trace evaluates to.
• globalVarianceTraceWitness: the matrix A_⊥combineᴴ (1 ⊗ ρ) A_⊥combine; as localVarianceTraceWitness, replaced in globalVarianceTraceForm by the sum its trace evaluates to.
• frequencyWeight: classical, imported.
• frequencyWeight_le_m: classical, imported.
• zeroCoordinateCount_eq: classical, imported.
• zeroCoordinateContributionSum: classical, imported.
• fourierBasisState_total_update_sum: classical, imported.
• fourierBasisInnerProduct: classical, imported.
• pointAddChar: classical, imported.
• pointAddCharRight: classical, imported.
• dotProductZMod_single_one: classical, imported.
• pointAddChar_eq_zero_iff: classical, imported.
• fourierBasisState_inner_product: classical, imported.
• eigenvectors_orthonormality: classical, imported.
• adjacencyEigenvalue: classical, imported.
• laplacianEigenvalue: classical, imported.
• hypercubeSpectralGap: classical, imported.
• eigenvectors_card: classical, imported.
• eigenvectors: classical, imported.
• laplacianEigenvalue_eq: classical, imported.
• hypercubeSpectralGap_le_laplacianEigenvalue: classical, imported.
• laplacianEigenvalue_of_weight_one: classical, imported.

References

In LionSR/MIPStarRE at commit 507e8122, not in this repository:

• references/ldt-paper/expansion.tex, lem:local-rewrite and lem:global-rewrite
• blueprint/src/chapter/ch05_expansion.tex

structure MIPRE.LIDT.Co.ExpansionHypercubeGraph.GlobalVarianceDecomposition {R : Type u_1} [AddCommGroup R] [Module ℂ R] (params : MIPStarRE.LDT.Parameters) (A : MIPStarRE.LDT.Point params → R) : Type u_1

A packaged decomposition for lem:global-rewrite.

The 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_⊥. It uses only the complex module structure of the operators, so it is stated over any complex module R (the vendored Op ι).

• averageComponent : R

  The average A_avg = (1/M) ∑_u A^u.

• orthogonalComponent : MIPStarRE.LDT.Point params → R

  The residual family u ↦ A^u - A_avg.

• averageComponent_eq : self.averageComponent = (↑(MIPStarRE.LDT.ExpansionHypercubeGraph.hypercubeVertexCount params))⁻¹ • ∑ u : MIPStarRE.LDT.Point params, A u

  The average component is (1/M) ∑_u A^u.

• orthogonal_sum_zero : ∑ u : MIPStarRE.LDT.Point params, self.orthogonalComponent u = 0

  The residual family sums to zero.

• decomposition (u : MIPStarRE.LDT.Point params) : A u = self.averageComponent + self.orthogonalComponent u

  Each A^u is the average plus its residual.

theorem MIPRE.LIDT.Co.ExpansionHypercubeGraph.GlobalVarianceDecomposition.orthogonalComponent_eq_sub_average {R : Type u_1} [AddCommGroup R] [Module ℂ R] {params : MIPStarRE.LDT.Parameters} {A : MIPStarRE.LDT.Point params → R} (decomp : GlobalVarianceDecomposition params A) (u : MIPStarRE.LDT.Point params) : decomp.orthogonalComponent u = A u - decomp.averageComponent

Recover the centered residual as A^u - A_avg.

theorem MIPRE.LIDT.Co.ExpansionHypercubeGraph.centered_sum_eq_zero {R : Type u_1} [AddCommGroup R] [Module ℂ R] (params : MIPStarRE.LDT.Parameters) (A : MIPStarRE.LDT.Point params → R) : ∑ u : MIPStarRE.LDT.Point params, (A u - (↑(MIPStarRE.LDT.ExpansionHypercubeGraph.hypercubeVertexCount params))⁻¹ • ∑ v : MIPStarRE.LDT.Point params, A v) = 0

The centered family u ↦ A^u - (1/M) ∑_v A^v sums to zero.

noncomputable def MIPRE.LIDT.Co.ExpansionHypercubeGraph.canonicalGlobalVarianceDecomposition {R : Type u_1} [AddCommGroup R] [Module ℂ R] (params : MIPStarRE.LDT.Parameters) (A : MIPStarRE.LDT.Point params → R) : 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 MIPRE.LIDT.Co.ExpansionHypercubeGraph.localVarianceTraceForm {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) (A : MIPStarRE.LDT.Point params → K →L[ℂ] K) (V : VecState K) : ℝ

The local-variance trace expression from lem:local-rewrite: the vendored Re τ(A_combineᴴ (L ⊗ ρ) A_combine), written as the real part of the sum this trace evaluates to, ∑ u v, L u v · ⟪Ψ, A_v† A_u Ψ⟫.

Equations

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

noncomputable def MIPRE.LIDT.Co.ExpansionHypercubeGraph.globalVarianceTraceForm {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) (A : MIPStarRE.LDT.Point params → K →L[ℂ] K) (V : VecState K) (decomp : GlobalVarianceDecomposition params A) : ℝ

The global-variance trace expression from lem:global-rewrite: the vendored (1/M) Re τ(A_⊥combineᴴ (1 ⊗ ρ) A_⊥combine) on the orthogonal residual of the decomposition, written through the sum this trace evaluates to.

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.