Section 7 — Matrix variance trace forms

This file contains the matrix-level variance quantities and trace-form rewrite statements used after the Fourier spectral-gap material in MatrixRealization.Core.

References

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

noncomputable def MIPStarRE.LDT.ExpansionHypercubeGraph.matrixSquaredDifferenceExpectation {H : MakingMeasurementsProjective.FiniteHilbertSpace} (ρ : MakingMeasurementsProjective.PositiveMatrixState H) (X Y : MakingMeasurementsProjective.MatrixOperator H) : Error

The quadratic form τ(ρ (X-Y)^*(X-Y)).

Equations

• MIPStarRE.LDT.ExpansionHypercubeGraph.matrixSquaredDifferenceExpectation ρ X Y = (MIPStarRE.LDT.MakingMeasurementsProjective.matrixExpectation ρ (Matrix.conjTranspose (X - Y) * (X - Y))).re

noncomputable def MIPStarRE.LDT.ExpansionHypercubeGraph.matrixLocalVariance (params : Parameters) (model : MatrixOperatorFamilyRealization params) : Error

The actual local variance, averaged over the hypercube edge set. This matches the Section 7.1 rerandomization distribution on ordered edges.

Equations

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

noncomputable def MIPStarRE.LDT.ExpansionHypercubeGraph.matrixGlobalVariance (params : Parameters) (model : MatrixOperatorFamilyRealization params) : Error

The actual global variance, averaged over two independent points.

Equations

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

noncomputable def MIPStarRE.LDT.ExpansionHypercubeGraph.matrixCombinedOperator (params : Parameters) (model : MatrixOperatorFamilyRealization params) : RectangularMatrixOperator model.space (tensorHilbertSpace (pointHilbertSpace params) model.space)

The matrix-level combined column operator used for the trace rewrites. Its u-th block is (A^u)ᴴ, so that the trace witnesses match the quadratic forms τ(ρ · (A^u - A^v)ᴴ (A^u - A^v)) for arbitrary families.

Equations

• MIPStarRE.LDT.ExpansionHypercubeGraph.matrixCombinedOperator params model ui j = star (model.family ui.1 j ui.2)

noncomputable def MIPStarRE.LDT.ExpansionHypercubeGraph.matrixCombinedColumnOperator (params : Parameters) (model : MatrixOperatorFamilyRealization params) : RectangularMatrixOperator model.space (tensorHilbertSpace (pointHilbertSpace params) model.space)

Bridge for the column-operator view used in the quadratic-form witnesses.

Equations

• MIPStarRE.LDT.ExpansionHypercubeGraph.matrixCombinedColumnOperator params model = MIPStarRE.LDT.ExpansionHypercubeGraph.matrixCombinedOperator params model

noncomputable def MIPStarRE.LDT.ExpansionHypercubeGraph.matrixLocalVarianceTraceWitness (params : Parameters) (model : MatrixOperatorFamilyRealization params) : MakingMeasurementsProjective.MatrixOperator model.space

Paper origin: references/ldt-paper/expansion.tex:145-154 (\label{lem:local-rewrite}); trace witness for the local-variance rewrite, matrix realization.

Equations

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

noncomputable def MIPStarRE.LDT.ExpansionHypercubeGraph.matrixLocalVarianceTraceForm (params : Parameters) (model : MatrixOperatorFamilyRealization params) : Error

The actual trace form for the local variance.

Equations

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

noncomputable def MIPStarRE.LDT.ExpansionHypercubeGraph.matrixGlobalVarianceTraceWitness (params : Parameters) (model : MatrixOperatorFamilyRealization params) : MakingMeasurementsProjective.MatrixOperator model.space

Paper origin: references/ldt-paper/expansion.tex:179-190 (\label{lem:global-rewrite}); trace witness for the global-variance rewrite, matrix realization.

Equations

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

noncomputable def MIPStarRE.LDT.ExpansionHypercubeGraph.matrixGlobalVarianceTraceForm (params : Parameters) (model : MatrixOperatorFamilyRealization params) : Error

The actual trace form for the global variance.

The 1 / hypercubeVertexCount factor (= 1 / M where M = q^m) matches the paper's lem:global-rewrite: the global variance equals (1/M) · Tr(⟨φ⊥| ⊗ A⊥ · (I ⊗ |ψ⟩⟨ψ|) · |φ⊥⟩ ⊗ A⊥), which in turn equals (1/2) · E_{u,v} ⟨ψ| (Aᵘ − Aᵛ)² ⊗ I |ψ⟩.

Equations

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

theorem MIPStarRE.LDT.ExpansionHypercubeGraph.conjTranspose_mul_mul_mono {H : MakingMeasurementsProjective.FiniteHilbertSpace} {K : MakingMeasurementsProjective.FiniteHilbertSpace} (M : RectangularMatrixOperator H K) {A B : MakingMeasurementsProjective.MatrixOperator K} (hAB : A ≤ B) : Matrix.conjTranspose M * (A * M) ≤ Matrix.conjTranspose M * (B * M)

Adjoint sandwiching is monotone in the middle factor.

theorem MIPStarRE.LDT.ExpansionHypercubeGraph.normalizedTrace_re_mono {H : MakingMeasurementsProjective.FiniteHilbertSpace} {A B : MakingMeasurementsProjective.MatrixOperator H} (hAB : A ≤ B) : (Quantum.normalizedTrace A).re ≤ (Quantum.normalizedTrace B).re

Monotonicity of Re τ with respect to the matrix order.

structure MIPStarRE.LDT.ExpansionHypercubeGraph.MatrixLocalRewriteStatement (params : Parameters) (model : MatrixOperatorFamilyRealization params) : Prop

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

Matrix-level rewrite identity for the local variance.

• traceFormula : matrixLocalVariance params model = matrixLocalVarianceTraceForm params model

structure MIPStarRE.LDT.ExpansionHypercubeGraph.MatrixGlobalRewriteStatement (params : Parameters) (model : MatrixOperatorFamilyRealization params) : Prop

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

Matrix-level rewrite identity for the global variance.

• traceFormula : matrixGlobalVariance params model = matrixGlobalVarianceTraceForm params model