Section 7 hypercube graph: trace-form foundations and Gram positivity

The counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/ExpansionHypercubeGraph/Theorems/Foundations.lean in the port of planning/c6b-plan.md (milestone M5, section "Port conventions"): the statement structures of lem:local-rewrite and lem:global-rewrite, and the closed forms of the global trace form.

The vendored proof of the local-to-global inequality realizes an operator family and its state as concrete matrices (MatrixRealization/), proves the operator inequality gap · P_⊥ ≤ L between scalar vertex matrices, tensors it with the density ρ, conjugates by the block matrix A_combine and takes the trace. On a vector state there is no density and no trace, and the same conclusion is Gram positivity (re_combinedTraceForm_nonneg): for a positive semidefinite scalar matrix P on the vertices and operators A_u on a Hilbert space,

Re ∑_{u,v} P u v · ⟪A_v Ψ, A_u Ψ⟫ ≥ 0,

because P is a sum of matrices star s * s and for each of them the sum is ∑_k ‖∑_v conj(s k v) • A_v Ψ‖². The scalar inequality gap · P_⊥ ≤ L itself is imported from the vendored matrix realization (hypercubeSpectralGap_operator_posSemidef), which is classical.

New here

• inner_star_mul_apply: ⟪Ψ, (star B * A) Ψ⟫ = ⟪B Ψ, A Ψ⟫;
• combinedTraceForm_add, combinedTraceForm_zero, combinedTraceForm_sub, combinedTraceForm_real_smul: linearity of the trace form in the scalar matrix;
• combinedTraceForm_star_mul_self, re_combinedTraceForm_nonneg: Gram positivity, which replaces the vendored matrix realization;
• re_combinedTraceForm_one: the trace form of the identity is the sum of the diagonal expectations.

Not ported

• abstractMatrixModel: the matrix realization of an operator family and a density; there is no matrix realization here, the variances being handled by Gram positivity.
• localVariance_eq_zero_of_isEmpty: the empty-carrier branch of the matrix realization; a Hilbert space with a unit vector is nonempty, and no proof here splits on it.
• globalVariance_eq_zero_of_isEmpty: as localVariance_eq_zero_of_isEmpty.
• localVarianceTraceForm_eq_zero_of_isEmpty: as localVariance_eq_zero_of_isEmpty.
• globalVarianceTraceForm_eq_zero_of_isEmpty: as localVariance_eq_zero_of_isEmpty.
• sum_reorder_four: classical, imported.
• sum_sum_mul_left: classical, imported.
• sum_sum_add: classical, imported.
• sum_sum_sub: classical, imported.
• matrixModelState: the density of the matrix realization; replaced by the vector state.
• trace_combined_tensor_eq: the trace of the combined tensor witness, entrywise; the trace forms here are defined by the sum it computes (combinedTraceForm).
• normalizedTrace_combined_tensor_eq: as trace_combined_tensor_eq.

The two files of the vendored ExpansionHypercubeGraph/MatrixRealization/ directory, MatrixRealization/Core.lean (the matrix realization, the Fourier projectors and the spectral gap as a matrix inequality) and MatrixRealization/TraceForms.lean (the matrix variances, trace witnesses and trace forms, and the trace monotonicity it uses), have no counterpart in the port: replaced by Gram positivity. Their scalar facts (hypercubeSpectralGap_operator_posSemidef, orthogonalModeProjectorMatrix) are 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

Statement structures

structure MIPRE.LIDT.Co.ExpansionHypercubeGraph.LocalRewriteStatement {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) : Prop

Paper origin: references/ldt-paper/expansion.tex:145-178 (\label{lem:local-rewrite}).

Conclusion statement for lem:local-rewrite: the local variance is rewritten as a trace-form expectation in the operator family A.

• traceFormula : localVariance params A V = localVarianceTraceForm params A V

  The local variance agrees with the trace form built from the Laplacian.

structure MIPRE.LIDT.Co.ExpansionHypercubeGraph.GlobalRewriteStatement {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) : Prop

Paper origin: references/ldt-paper/expansion.tex:179-269 (\label{lem:global-rewrite}).

Conclusion statement for lem:global-rewrite: the global variance is rewritten as a trace-form expectation along the eigenbasis of the hypercube graph Laplacian.

• decomposition : ∃ (decomp : GlobalVarianceDecomposition params A), globalVariance params A V = globalVarianceTraceForm params A V decomp

  A Fourier-mode decomposition whose trace form recovers the global variance.

The trace form: linearity and Gram positivity

theorem MIPRE.LIDT.Co.ExpansionHypercubeGraph.inner_star_mul_apply {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (V : VecState K) (A B : K →L[ℂ] K) : inner ℂ V.Ψ ((star B * A) V.Ψ) = inner ℂ (B V.Ψ) (A V.Ψ)

The expectation of star B * A is the inner product of B Ψ and A Ψ.

theorem MIPRE.LIDT.Co.ExpansionHypercubeGraph.combinedTraceForm_add {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {n : Type u_2} [Fintype n] (A : n → K →L[ℂ] K) (V : VecState K) (P Q : Matrix n n ℂ) : combinedTraceForm (P + Q) A V = combinedTraceForm P A V + combinedTraceForm Q A V

The trace form is additive in the scalar matrix.

@[simp]

theorem MIPRE.LIDT.Co.ExpansionHypercubeGraph.combinedTraceForm_zero {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {n : Type u_2} [Fintype n] (A : n → K →L[ℂ] K) (V : VecState K) : combinedTraceForm 0 A V = 0

The trace form of the zero matrix vanishes.

theorem MIPRE.LIDT.Co.ExpansionHypercubeGraph.combinedTraceForm_sub {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {n : Type u_2} [Fintype n] (A : n → K →L[ℂ] K) (V : VecState K) (P Q : Matrix n n ℂ) : combinedTraceForm (P - Q) A V = combinedTraceForm P A V - combinedTraceForm Q A V

The trace form is additive in the scalar matrix: differences.

theorem MIPRE.LIDT.Co.ExpansionHypercubeGraph.combinedTraceForm_real_smul {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {n : Type u_2} [Fintype n] (A : n → K →L[ℂ] K) (V : VecState K) (c : ℝ) (P : Matrix n n ℂ) : (combinedTraceForm (↑c • P) A V).re = c * (combinedTraceForm P A V).re

A real multiple of the scalar matrix scales the real part of the trace form.

theorem MIPRE.LIDT.Co.ExpansionHypercubeGraph.combinedTraceForm_star_mul_self {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {n : Type u_2} [Fintype n] (A : n → K →L[ℂ] K) (V : VecState K) (s : Matrix n n ℂ) : combinedTraceForm (star s * s) A V = ∑ k : n, inner ℂ (∑ v : n, star (s k v) • (A v) V.Ψ) (∑ u : n, star (s k u) • (A u) V.Ψ)

The trace form of star s * s is a sum of squared norms: with z_k = ∑_v conj(s k v) • A_v Ψ, it is ∑_k ⟪z_k, z_k⟫.

theorem MIPRE.LIDT.Co.ExpansionHypercubeGraph.re_combinedTraceForm_nonneg {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {n : Type u_2} [Fintype n] (A : n → K →L[ℂ] K) (V : VecState K) {P : Matrix n n ℂ} (hP : P.PosSemidef) : 0 ≤ (combinedTraceForm P A V).re

Gram positivity. For a positive semidefinite scalar matrix P and operators A_u, the real part of ∑_{u,v} P u v · ⟪A_v Ψ, A_u Ψ⟫ is nonnegative. This replaces the vendored matrix realization of the local-to-global inequality.

theorem MIPRE.LIDT.Co.ExpansionHypercubeGraph.re_combinedTraceForm_one {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {n : Type u_2} [Fintype n] [DecidableEq n] (A : n → K →L[ℂ] K) (V : VecState K) : (combinedTraceForm 1 A V).re = ∑ u : n, V.ev (star (A u) * A u)

The trace form of the identity matrix is the sum of the diagonal expectations.

Closed forms of the global trace form

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

Closed form of globalVarianceTraceForm as the average squared norm of the orthogonal residual family carried by the decomposition.

theorem MIPRE.LIDT.Co.ExpansionHypercubeGraph.globalVarianceTraceForm_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) (decomp : GlobalVarianceDecomposition params A) : globalVarianceTraceForm params A V decomp = (↑(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 of globalVarianceTraceForm in centered-correlation coordinates.