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

This file assembles the public Section 7 results about the hypercube graph: the Laplacian edge-difference formula, the local and global variance rewrites, and the local-to-global inequality. The proof route passes through the matrix-realization theorems and then exposes the statements in the QuantumState and operator-family language used elsewhere in the LDT formalization.

References

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

theorem MIPStarRE.LDT.ExpansionHypercubeGraph.avgOver_independentPointPair_eq_uniform_prod (params : Parameters) [FieldModel params.q] (f : Point params × Point params → Error) : avgOver (independentPointPair params) f = avgOver (uniformDistribution (Point params × Point params)) f

Averaging over two independently sampled hypercube points is the same as averaging over the uniform distribution on the product of point types.

theorem MIPStarRE.LDT.ExpansionHypercubeGraph.matrixLocalToGlobal (params : Parameters) (model : MatrixOperatorFamilyRealization params) : matrixGlobalVariance params model ≤ ↑params.m * matrixLocalVariance params model

The concrete matrix-level counterpart of lem:local-to-global.

theorem MIPStarRE.LDT.ExpansionHypercubeGraph.matrixLocalRewrite (params : Parameters) (model : MatrixOperatorFamilyRealization params) : MatrixLocalRewriteStatement params model

The concrete matrix-level counterpart of lem:local-rewrite.

theorem MIPStarRE.LDT.ExpansionHypercubeGraph.matrixGlobalRewrite (params : Parameters) (model : MatrixOperatorFamilyRealization params) : MatrixGlobalRewriteStatement params model

The concrete matrix-level counterpart of lem:global-rewrite.

theorem MIPStarRE.LDT.ExpansionHypercubeGraph.laplacianRewrite (params : Parameters) : laplacian params = laplacianDifferenceForm params

prop:laplacian-rewrite — the edge-difference form of the Laplacian equals the standard (1/M)I - K form. Proved in MIPStarRE.LDT.ExpansionHypercubeGraph.laplacian_eq_edgeDifferenceForm.

Public theorem wrappers

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

The local variance for a bipartite state when the operator family acts on the left tensor factor. The squared difference is represented as (leftTensor (A u) - leftTensor (A v))ᴴ * (leftTensor (A u) - leftTensor (A v)); for self-adjoint A u, this is the operator-square expression appearing in the paper.

Equations

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

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

The global variance for a bipartite state when the operator family acts on the left tensor factor.

Equations

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

theorem MIPStarRE.LDT.ExpansionHypercubeGraph.localToGlobal {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) (A : Point params → Quantum.Op ι) (ψ : QuantumState ι) : globalVariance params A ψ ≤ ↑params.m * localVariance params A ψ

General local-to-global inequality for an arbitrary operator family on a finite-dimensional state space.

This is the abstract form behind lem:local-to-global: the global variance over two independent vertices is bounded by m times the local variance over the rerandomized-coordinate edge distribution.

theorem MIPStarRE.LDT.ExpansionHypercubeGraph.localToGlobalBipartite (params : Parameters) {ιA ιB : Type} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] (A : Point params → Quantum.Op ιA) (ψ : QuantumState (ιA × ιB)) : bipartiteGlobalVariance params A ψ ≤ ↑params.m * bipartiteLocalVariance params A ψ

lem:local-to-global, in bipartite form.

This is the local-to-global variance inequality for the bipartite operator family A^u ⊗ I. The surrounding paper section discusses positive contractions, but the spectral estimate itself is valid for every operator family.

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

lem:local-rewrite.

The local variance agrees with the Laplacian trace form of the combined operator family. The proof is obtained from the concrete matrix rewrite, with a separate zero-dimensional branch for the empty state space.

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

lem:global-rewrite. The existential witness is the canonical canonicalGlobalVarianceDecomposition, determined by params and A, whose averageComponent is the paper's A_avg = E_u A^u = (1/M) · ∑_u A^u; equivalently, A_0 = M^{1/2} · A_avg (expansion.tex §7.2, Local and global variance).