Section 7 hypercube graph: local-to-global variance theorems

The counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/ExpansionHypercubeGraph/Theorems/Results.lean in the port of planning/c6b-plan.md (milestone M5, section "Port conventions"): the local and global variance rewrites (localRewrite, globalRewrite) and the local-to-global inequality (localToGlobal, and localToGlobalBipartite for a family placed by S.L).

The vendored proof of localToGlobal goes through the matrix realization of the family and the density: the matrix inequality gap · P_⊥ ≤ L is tensored with ρ, conjugated by the block matrix A_combine, and traced. Here the same inequality is read through Gram positivity (re_combinedTraceForm_nonneg, Theorems/Foundations.lean): L - gap · P_⊥ is positive semidefinite (hypercubeSpectralGap_operator_posSemidef, imported, scalar), so its trace form is nonnegative, and the two trace forms are m · the global variance and the local variance (traceForm_localToGlobal). The statements hold for every family A : Point params → (K →L[ℂ] K) and every vector state.

A vendored variance on a weighted state W ρ Wᴴ (GlobalVariance's weightedPolynomialState, which is not normalized) is, on a vector state, the variance of the family u ↦ A u * W on V: ev_{WρWᴴ}(X) = ev_ρ(Wᴴ X W) and Wᴴ (A_u - A_v)ᴴ (A_u - A_v) W = pointDifferenceSquaredOperator (fun u => A u * W) u v. So the theorems here apply to it unchanged.

New here

• localVariance_eq_closedForm: the closed form of the local variance, the vendored matrixLocalVariance_eq_closedForm without the matrix realization;
• traceForm_localToGlobal: the trace-form inequality by Gram positivity, the vendored matrixTraceForm_localToGlobal without the matrix realization.

Not ported

• avgOver_independentPointPair_eq_uniform_prod: classical, imported.
• matrixLocalVariance_eq_closedForm: the matrix realization; replaced by localVariance_eq_closedForm.
• matrixTraceForm_localToGlobal: the matrix realization (trace monotonicity under conjugation by A_combine); replaced by Gram positivity, traceForm_localToGlobal.
• matrixLocalToGlobal: the matrix realization; its content is localToGlobal.
• matrixLocalRewrite: the matrix realization; its content is localRewrite.
• matrixGlobalRewrite: the matrix realization; its content is globalRewrite.
• laplacianRewrite: classical (an identity of scalar vertex matrices), imported.

References

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

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

theorem MIPRE.LIDT.Co.ExpansionHypercubeGraph.hypercubeSpectralGap_operator_posSemidef (params : MIPStarRE.LDT.Parameters) : Matrix.PosSemidef (MIPStarRE.LDT.ExpansionHypercubeGraph.matrixLaplacianOperator params - ↑(MIPStarRE.LDT.ExpansionHypercubeGraph.hypercubeSpectralGap params) • MIPStarRE.LDT.ExpansionHypercubeGraph.orthogonalModeProjectorMatrix params)

Upstream proves this from its Fourier diagonalization, through a dozen private lemmas; the port derives it from the public Loewner-order form hypercubeSpectralGap_operator, which is the same statement by Matrix.le_iff.

theorem MIPRE.LIDT.Co.ExpansionHypercubeGraph.orthogonalModeProjector_re_sum (params : MIPStarRE.LDT.Parameters) (z : MIPStarRE.LDT.Point params → MIPStarRE.LDT.Point params → ℂ) : (∑ u : (MIPStarRE.LDT.ExpansionHypercubeGraph.pointHilbertSpace params).carrier, ∑ v : (MIPStarRE.LDT.ExpansionHypercubeGraph.pointHilbertSpace params).carrier, MIPStarRE.LDT.ExpansionHypercubeGraph.orthogonalModeProjectorMatrix params u v * z u v).re = ∑ u : MIPStarRE.LDT.Point params, (z u u).re - (↑(MIPStarRE.LDT.ExpansionHypercubeGraph.hypercubeVertexCount params))⁻¹ * ∑ u : MIPStarRE.LDT.Point params, ∑ v : MIPStarRE.LDT.Point params, (z u v).re

Upstream keeps this helper private since its Lean-module port (LionSR/MIPStarRE at 5fc363b); the port carries its own copy, with upstream's proof.

theorem MIPRE.LIDT.Co.ExpansionHypercubeGraph.localVariance_eq_closedForm {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) : localVariance params A V = (↑(MIPStarRE.LDT.ExpansionHypercubeGraph.hypercubeVertexCount params))⁻¹ * ∑ u : MIPStarRE.LDT.Point params, V.ev (star (A u) * A u) - ∑ u : MIPStarRE.LDT.Point params, ∑ v : MIPStarRE.LDT.Point params, MIPStarRE.LDT.ExpansionHypercubeGraph.rerandomizeCoordWeight params u v * V.ev (star (A v) * A u)

Closed form for the local variance: the diagonal expectations averaged over the vertices, minus the correlations weighted by the edge distribution.

theorem MIPRE.LIDT.Co.ExpansionHypercubeGraph.traceForm_localToGlobal {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) : globalVarianceTraceForm params A V decomp ≤ ↑params.m * localVarianceTraceForm params A V

The trace-form inequality behind lem:local-to-global, by Gram positivity: the global trace form is at most m times the local one. The vendored matrixTraceForm_localToGlobal proves it on a matrix realization, by tensoring gap · P_⊥ ≤ L with the density and tracing.

noncomputable def MIPRE.LIDT.Co.ExpansionHypercubeGraph.bipartiteLocalVariance {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {𝔓 : Type u_2} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) (A : MIPStarRE.LDT.Point params → 𝔓) (S : SymModel 𝔓 K) : ℝ

The local variance for a symmetric model when the operator family acts on the first player's side: the vendored localVariance of u ↦ leftTensor (A u) on the bipartite state.

Equations

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

noncomputable def MIPRE.LIDT.Co.ExpansionHypercubeGraph.bipartiteGlobalVariance {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {𝔓 : Type u_2} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) (A : MIPStarRE.LDT.Point params → 𝔓) (S : SymModel 𝔓 K) : ℝ

The global variance for a symmetric model when the operator family acts on the first player's side.

Equations

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

theorem MIPRE.LIDT.Co.ExpansionHypercubeGraph.localRewrite {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) : LocalRewriteStatement params A V

lem:local-rewrite: the local variance agrees with the Laplacian trace form of the family.

theorem MIPRE.LIDT.Co.ExpansionHypercubeGraph.globalRewrite {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) : GlobalRewriteStatement params A V

lem:global-rewrite. The existential witness is canonicalGlobalVarianceDecomposition, whose averageComponent is the paper's A_avg = E_u A^u = (1/M) · ∑_u A^u.

theorem MIPRE.LIDT.Co.ExpansionHypercubeGraph.localToGlobal {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) : globalVariance params A V ≤ ↑params.m * localVariance params A V

General local-to-global inequality for an arbitrary operator family on a vector state: the global variance over two independent vertices is bounded by m times the local variance over the rerandomized-coordinate edge distribution.

theorem MIPRE.LIDT.Co.ExpansionHypercubeGraph.localToGlobalBipartite {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {𝔓 : Type u_2} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) (A : MIPStarRE.LDT.Point params → 𝔓) (S : SymModel 𝔓 K) : bipartiteGlobalVariance params A S ≤ ↑params.m * bipartiteLocalVariance params A S

lem:local-to-global, in bipartite form: the local-to-global variance inequality for the family S.L (A u) (the vendored A^u ⊗ I). The spectral estimate holds for every family.