Section 7 hypercube graph: closed forms of the variances

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

The vendored file computes, for a matrix realization model of an operator family and a density (MatrixRealization/), the squared differences and the closed forms of the global variance and of the local trace form in the correlations ev(A_v† A_u). Here the realization is the family A : Point params → (K →L[ℂ] K) and the vector state V themselves: corr_symm and sqdiff_eq_corr keep their vendored names, with model replaced by A and V, and the closed forms are stated for globalVariance and localVarianceTraceForm directly. The classical half of the vendored file (the row and column sums of the edge weights, their symmetry, and the edge-difference form of the Laplacian) is imported.

New here

• sqdiff_eq_diag_corr: the squared difference in the two diagonal terms and one correlation;
• globalVariance_eq_closedForm: the closed form of the global variance, the vendored matrixGlobalVariance_eq_closedForm without the matrix realization;
• localVarianceTraceForm_eq_closedForm: the closed form of the local trace form, the vendored matrixLocalVarianceTraceForm_eq_closedForm without the matrix realization.

Not ported

• orthogonalModeProjector_re_sum: classical (a scalar identity for any z), imported.
• matrixGlobalVarianceTraceForm_eq_closedForm: the matrix realization; its content is globalVarianceTraceForm_eq_closedForm (Theorems/Foundations.lean).
• matrixGlobalVariance_eq_closedForm: the matrix realization; replaced by globalVariance_eq_closedForm.
• rerandomizeCoordWeight_rowSum: classical, imported.
• update_eq_fixed_count: classical, imported.
• rerandomizeCoordWeight_colSum: classical, imported.
• update_swap: classical, imported.
• update_value_eq: classical, imported.
• rerandomizeCoordWeight_symm: classical, imported.
• laplacian_eq_edgeDifferenceForm: classical, imported.
• matrixLocalVarianceTraceForm_eq_closedForm: the matrix realization; replaced by localVarianceTraceForm_eq_closedForm.

References

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

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

theorem MIPRE.LIDT.Co.ExpansionHypercubeGraph.hypercubeAdjacencyWeight_eq_rerandomizeCoordWeight (params : MIPStarRE.LDT.Parameters) (u v : MIPStarRE.LDT.Point params) : MIPStarRE.LDT.ExpansionHypercubeGraph.hypercubeAdjacencyWeight params u v = ↑(MIPStarRE.LDT.ExpansionHypercubeGraph.rerandomizeCoordWeight params u v)

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.corr_symm {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) (u v : MIPStarRE.LDT.Point params) : V.ev (star (A v) * A u) = V.ev (star (A u) * A v)

The correlation term is symmetric under swapping the two points.

theorem MIPRE.LIDT.Co.ExpansionHypercubeGraph.sqdiff_eq_corr {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) (u v : MIPStarRE.LDT.Point params) : V.ev (pointDifferenceSquaredOperator A u v) = V.ev (star (A u) * A u) + V.ev (star (A v) * A v) - V.ev (star (A u) * A v) - V.ev (star (A v) * A u)

Expand the squared-difference expectation into diagonal and correlation terms.

theorem MIPRE.LIDT.Co.ExpansionHypercubeGraph.sqdiff_eq_diag_corr {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) (u v : MIPStarRE.LDT.Point params) : V.ev (pointDifferenceSquaredOperator A u v) = V.ev (star (A u) * A u) + V.ev (star (A v) * A v) - 2 * V.ev (star (A v) * A u)

The squared difference in the diagonal terms and one correlation.

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

Closed form for the global variance.

theorem MIPRE.LIDT.Co.ExpansionHypercubeGraph.localVarianceTraceForm_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) : localVarianceTraceForm 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 trace expression.