Section 7 hypercube graph: core definitions

The counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/ExpansionHypercubeGraph/Defs/Core.lean in the port of planning/c6b-plan.md (milestone M5, section "Port conventions"): the local and global variances of a family of operators A : Point params → (K →L[ℂ] K) on a vector state V : VecState K (the vendored QuantumState ι, a state on one space; the variances use only the state, so they are VecState quantities, and the bipartite form A^u ⊗ 1 is S.L (A u)).

The vendored file also writes the trace τ((L ⊗ ρ) · A_combine A_combineᴴ) of the paper's lem:local-rewrite through the block matrix A_combine (combinedOperator). A vector state has no density and no trace; what that trace evaluates to, the sum ∑ u v, P u v · ⟪Ψ, A_v† A_u Ψ⟫ for a scalar matrix P on the vertices, is combinedTraceForm P A V here, and both trace forms of Defs/Fourier.lean are defined through it. Its positivity for a positive semidefinite P (Gram positivity, Theorems/Foundations.lean) is what replaces the vendored matrix realization.

The classical half of the vendored file (the hypercube graph, its edge distribution, and the adjacency and Laplacian matrices, which are scalar matrices on the vertex register and use no state) is not ported: this file imports the vendored file and names those declarations through an explicit open MIPStarRE.LDT.ExpansionHypercubeGraph (…) list.

New here

• combinedTraceForm: the trace form Tr(A_combineᴴ (P ⊗ ρ) A_combine) of a scalar vertex matrix P, as the sum it evaluates to on a vector state.

Not ported

• hypercubeVertexCount: classical, imported.
• coordinateDisagreementSet: classical, imported.
• coordinateDisagreementCount: classical, imported.
• IsHypercubeEdge: classical, imported.
• instDecidableIsHypercubeEdge: classical, imported.
• instDecidablePredHypercubeEdgePair: classical, imported.
• rerandomizeCoordWeight: classical, imported.
• RerandomizeCoordSample: classical, imported.
• rerandomizeCoordSampleToPair: classical, imported.
• rerandomizeCoord: classical, imported.
• rerandomizeCoord_isProbability: classical, imported.
• rerandomizeCoord_toPMF: classical, imported.
• rerandomizeCoord_mass_eq_one: classical, imported.
• avgOver_rerandomizeCoord_eq_uniform_sample: classical, imported.
• avgOver_rerandomizeCoord_eq_weight_sum: classical, imported.
• independentPointPair: classical, imported.
• pointHilbertSpace: classical (the vertex register of the scalar matrices), imported.
• hypercubeAdjacencyWeight: classical, imported.
• matrixAdjacencyOperator: classical (a scalar matrix on the vertices), imported.
• matrixLaplacianOperator: classical (a scalar matrix on the vertices), imported.
• adjacency: classical (a scalar matrix on the vertices), imported.
• laplacian: classical (a scalar matrix on the vertices), imported.
• laplacianDifferenceForm: classical (a scalar matrix on the vertices), imported.
• combinedColumnIndex: the index type of the block matrix A_combine; replaced by combinedTraceForm.
• combinedOperator: the block matrix A_combine of a matrix family; a vector state has no trace to evaluate it against, and the trace it serves is combinedTraceForm.

References

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

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

noncomputable def MIPRE.LIDT.Co.ExpansionHypercubeGraph.pointDifferenceSquaredOperator {R : Type u_1} [Ring R] [StarRing R] {params : MIPStarRE.LDT.Parameters} (A : MIPStarRE.LDT.Point params → R) (u v : MIPStarRE.LDT.Point params) : R

The squared difference operator (A^u - A^v)† (A^u - A^v).

Equations

• MIPRE.LIDT.Co.ExpansionHypercubeGraph.pointDifferenceSquaredOperator A u v = star (A u - A v) * (A u - A v)

noncomputable def MIPRE.LIDT.Co.ExpansionHypercubeGraph.localVariance {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) : ℝ

The local variance from def:local-and-variance.

Equations

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

noncomputable def MIPRE.LIDT.Co.ExpansionHypercubeGraph.globalVariance {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) : ℝ

The global variance from def:local-and-variance.

Equations

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

noncomputable def MIPRE.LIDT.Co.ExpansionHypercubeGraph.localAndVariance {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) : ℝ × ℝ

Combined accessor for the local and global variances.

Equations

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

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

The trace form Tr(A_combineᴴ (P ⊗ ρ) A_combine) of a scalar matrix P on the index set of an operator family A, as the sum it evaluates to on a vector state: ∑ u v, P u v · ⟪Ψ, A_v† A_u Ψ⟫. The vendored trace witnesses (localVarianceTraceWitness, globalVarianceTraceWitness) are this sum at P = L and at P = 1.

Equations

• MIPRE.LIDT.Co.ExpansionHypercubeGraph.combinedTraceForm P A V = ∑ u : n, ∑ v : n, P u v * inner ℂ V.Ψ ((star (A v) * A u) V.Ψ)