Documentation

MIPStarRE.LDT.ExpansionHypercubeGraph.Theorems.Matrix

Section 7 hypercube graph: matrix-realization theorems #

Translating the squared-difference expectation of the hypercube graph operators into the ev-based inner-product language of the matrix realization model.

References #

source
theorem MIPStarRE.LDT.ExpansionHypercubeGraph.corr_symm (params : Parameters) (model : MatrixOperatorFamilyRealization params) (u v : Point params) :
ev (matrixModelState model) (Matrix.conjTranspose (model.family v) * model.family u) = ev (matrixModelState model) (Matrix.conjTranspose (model.family u) * model.family v)

The matrix correlation term is symmetric under swapping the two points.

source
theorem MIPStarRE.LDT.ExpansionHypercubeGraph.sqdiff_eq_corr (params : Parameters) (model : MatrixOperatorFamilyRealization params) (u v : Point params) :
matrixSquaredDifferenceExpectation model.state (model.family u) (model.family v) = ev (matrixModelState model) (Matrix.conjTranspose (model.family u) * model.family u) + ev (matrixModelState model) (Matrix.conjTranspose (model.family v) * model.family v) - ev (matrixModelState model) (Matrix.conjTranspose (model.family u) * model.family v) - ev (matrixModelState model) (Matrix.conjTranspose (model.family v) * model.family u)

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

source
theorem MIPStarRE.LDT.ExpansionHypercubeGraph.matrixGlobalVarianceTraceForm_eq_closedForm (params : Parameters) (model : MatrixOperatorFamilyRealization params) :
matrixGlobalVarianceTraceForm params model = (↑(hypercubeVertexCount params))⁻¹ * ∑ u : Point params, ev (matrixModelState model) (Matrix.conjTranspose (model.family u) * model.family u) - (↑(hypercubeVertexCount params))⁻¹ * (↑(hypercubeVertexCount params))⁻¹ * ∑ u : Point params, ∑ v : Point params, ev (matrixModelState model) (Matrix.conjTranspose (model.family v) * model.family u)

Closed form for the matrix global-variance trace expression.

source
theorem MIPStarRE.LDT.ExpansionHypercubeGraph.matrixGlobalVariance_eq_closedForm (params : Parameters) (model : MatrixOperatorFamilyRealization params) :
matrixGlobalVariance params model = (↑(hypercubeVertexCount params))⁻¹ * ∑ u : Point params, ev (matrixModelState model) (Matrix.conjTranspose (model.family u) * model.family u) - (↑(hypercubeVertexCount params))⁻¹ * (↑(hypercubeVertexCount params))⁻¹ * ∑ u : Point params, ∑ v : Point params, ev (matrixModelState model) (Matrix.conjTranspose (model.family v) * model.family u)

Closed form for the matrix global variance.

source
theorem MIPStarRE.LDT.ExpansionHypercubeGraph.rerandomizeCoordWeight_rowSum (params : Parameters) (u : Point params) :
∑ v : Point params, rerandomizeCoordWeight params u v = (↑(hypercubeVertexCount params))⁻¹

The rerandomized-edge weight sums to the uniform point weight across each source row.

source
theorem MIPStarRE.LDT.ExpansionHypercubeGraph.rerandomizeCoordWeight_colSum (params : Parameters) (v : Point params) :
∑ u : Point params, rerandomizeCoordWeight params u v = (↑(hypercubeVertexCount params))⁻¹

The rerandomized-edge weight sums to the uniform point weight across each target column.

Symmetry of edge weights and the Laplacian edge-difference form #

source
theorem MIPStarRE.LDT.ExpansionHypercubeGraph.rerandomizeCoordWeight_symm (params : Parameters) (u v : Point params) :
rerandomizeCoordWeight params u v = rerandomizeCoordWeight params v u

The rerandomizeCoordWeight is symmetric: w(u,v) = w(v,u).

source
theorem MIPStarRE.LDT.ExpansionHypercubeGraph.laplacian_eq_edgeDifferenceForm (params : Parameters) :
matrixLaplacianOperator params = laplacianDifferenceForm params

prop:laplacian-rewrite: the Laplacian equals the edge-difference form (1/2) · E_{(u,v)∼C} (|u⟩-|v⟩)(⟨u|-⟨v|), proved entrywise using the symmetry and row/column-sum properties of the edge distribution.

source
theorem MIPStarRE.LDT.ExpansionHypercubeGraph.matrixLocalVarianceTraceForm_eq_closedForm (params : Parameters) (model : MatrixOperatorFamilyRealization params) :
matrixLocalVarianceTraceForm params model = (↑(hypercubeVertexCount params))⁻¹ * ∑ u : Point params, ev (matrixModelState model) (Matrix.conjTranspose (model.family u) * model.family u) - ∑ u : Point params, ∑ v : Point params, rerandomizeCoordWeight params u v * ev (matrixModelState model) (Matrix.conjTranspose (model.family v) * model.family u)

Closed form for the matrix local-variance trace expression.