Section 7 — Matrix realization

This file gives concrete finite-dimensional matrix realizations of the hypercube variance operators, Fourier projectors, and spectral inequalities introduced in Defs.

References

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

def MIPStarRE.LDT.ExpansionHypercubeGraph.tensorHilbertSpace (H : MakingMeasurementsProjective.FiniteHilbertSpace) (K : MakingMeasurementsProjective.FiniteHilbertSpace) : MakingMeasurementsProjective.FiniteHilbertSpace

Tensor two finite Hilbert spaces by taking the cartesian product of indices.

Equations

• MIPStarRE.LDT.ExpansionHypercubeGraph.tensorHilbertSpace H K = { carrier := H.carrier × K.carrier, instFintype := inferInstance, instDecidableEq := inferInstance, instNonempty := ⋯ }

def MIPStarRE.LDT.ExpansionHypercubeGraph.matrixTensorOperator {H : MakingMeasurementsProjective.FiniteHilbertSpace} {K : MakingMeasurementsProjective.FiniteHilbertSpace} (A : MakingMeasurementsProjective.MatrixOperator H) (B : MakingMeasurementsProjective.MatrixOperator K) : MakingMeasurementsProjective.MatrixOperator (tensorHilbertSpace H K)

Kronecker product of two concrete operators.

Equations

• MIPStarRE.LDT.ExpansionHypercubeGraph.matrixTensorOperator A B = Matrix.kronecker A B

@[reducible, inline]

abbrev MIPStarRE.LDT.ExpansionHypercubeGraph.RectangularMatrixOperator (H : MakingMeasurementsProjective.FiniteHilbertSpace) (K : MakingMeasurementsProjective.FiniteHilbertSpace) : Type (max u_2 u_1)

Rectangular operators from H into K, represented as concrete matrices.

Equations

• MIPStarRE.LDT.ExpansionHypercubeGraph.RectangularMatrixOperator H K = Matrix K.carrier H.carrier ℂ

structure MIPStarRE.LDT.ExpansionHypercubeGraph.MatrixOperatorFamilyRealization (params : Parameters) : Type (u + 1)

The concrete matrix family underlying the variance calculations.

• space : MakingMeasurementsProjective.FiniteHilbertSpace
• state : MakingMeasurementsProjective.PositiveMatrixState self.space
• family : Point params → MakingMeasurementsProjective.MatrixOperator self.space

noncomputable def MIPStarRE.LDT.ExpansionHypercubeGraph.matrixHypercubeEdgeDistribution (params : Parameters) : Distribution (Point params × Point params)

The Section 7.1 edge distribution used by the matrix model.

Equations

• MIPStarRE.LDT.ExpansionHypercubeGraph.matrixHypercubeEdgeDistribution params = MIPStarRE.LDT.ExpansionHypercubeGraph.rerandomizeCoord params

noncomputable def MIPStarRE.LDT.ExpansionHypercubeGraph.constantModeProjectorMatrix (params : Parameters) : MakingMeasurementsProjective.MatrixOperator (pointHilbertSpace params)

The normalized all-ones projector onto the constant mode.

Equations

• MIPStarRE.LDT.ExpansionHypercubeGraph.constantModeProjectorMatrix params x✝¹ x✝ = (↑(MIPStarRE.LDT.ExpansionHypercubeGraph.hypercubeVertexCount params))⁻¹

noncomputable def MIPStarRE.LDT.ExpansionHypercubeGraph.orthogonalModeProjectorMatrix (params : Parameters) : MakingMeasurementsProjective.MatrixOperator (pointHilbertSpace params)

The projector onto the orthogonal complement of the constant mode.

Equations

• MIPStarRE.LDT.ExpansionHypercubeGraph.orthogonalModeProjectorMatrix params = 1 - MIPStarRE.LDT.ExpansionHypercubeGraph.constantModeProjectorMatrix params

theorem MIPStarRE.LDT.ExpansionHypercubeGraph.hypercubeVertexCount_pos (params : Parameters) : 0 < hypercubeVertexCount params

theorem MIPStarRE.LDT.ExpansionHypercubeGraph.hypercubeVertexCount_one_lt (params : Parameters) : 1 < hypercubeVertexCount params

theorem MIPStarRE.LDT.ExpansionHypercubeGraph.hypercubeSpectralGap_operator (params : Parameters) : ↑(hypercubeSpectralGap params) • orthogonalModeProjectorMatrix params ≤ matrixLaplacianOperator params

The operator spectral gap inequality for the hypercube: (1 / (m M)) · P⊥ ≤ L, with M = q^m.

structure MIPStarRE.LDT.ExpansionHypercubeGraph.LaplacianSpectralGapConclusion (params : Parameters) : Prop

Fourier-indexed spectral-gap conclusion supporting cor:laplacian-spectral-gap.

Paper origin: references/ldt-paper/expansion.tex:102-109.

The paper states this corollary as an ordered-spectrum assertion: if λ₁ ≤ λ₂ ≤ ... ≤ λ_M are the eigenvalues of the Laplacian L, then λ₁ = 0 and λ₂ = 1 / (mM). In the finite Fourier formulation, this is the assertion that the zero-frequency mode has eigenvalue 0, every nonzero mode has eigenvalue at least 1 / (mM), and a weight-one mode attains this value.

• zeroEigenvalue : laplacianEigenvalue params 0 = 0
• nonzeroEigenvalue_ge_gap (α : Point params) : α ≠ 0 → hypercubeSpectralGap params ≤ laplacianEigenvalue params α
• gap_attained : ∃ (α : Point params), α ≠ 0 ∧ laplacianEigenvalue params α = hypercubeSpectralGap params
• gap_eq : hypercubeSpectralGap params = 1 / (↑params.m * ↑(params.q ^ params.m))

theorem MIPStarRE.LDT.ExpansionHypercubeGraph.laplacianSpectralGap (params : Parameters) : LaplacianSpectralGapConclusion params

cor:laplacian-spectral-gap: the hypercube Laplacian has bottom eigenvalue 0 and spectral gap 1 / (mM), expressed through the Fourier diagonalization of L.

theorem MIPStarRE.LDT.ExpansionHypercubeGraph.laplacianSpectralGapOrdered_of_list_bounds (params : Parameters) (lambda : Fin (hypercubeVertexCount params) → Error) (hordered : ∀ (i j : Fin (hypercubeVertexCount params)), ↑i ≤ ↑j → lambda i ≤ lambda j) (hnonneg : ∀ (i : Fin (hypercubeVertexCount params)), 0 ≤ lambda i) (hzero : ∃ (i : Fin (hypercubeVertexCount params)), lambda i = 0) (hgap_lower : ∀ (i : Fin (hypercubeVertexCount params)), i ≠ ⟨0, ⋯⟩ → hypercubeSpectralGap params ≤ lambda i) (hgap_attained : ∃ (i : Fin (hypercubeVertexCount params)), i ≠ ⟨0, ⋯⟩ ∧ lambda i = hypercubeSpectralGap params) : lambda ⟨0, ⋯⟩ = 0 ∧ lambda ⟨1, ⋯⟩ = 1 / (↑params.m * ↑(hypercubeVertexCount params))

Formalization-only criterion for the ordered spectrum in cor:laplacian-spectral-gap.

This auxiliary lemma records the finite ordering argument used after spectral identification. If an ordered list is nonnegative, has a zero entry, has all entries except the first bounded below by the spectral gap, and attains that gap, then its first two entries have the values stated in the paper.

theorem MIPStarRE.LDT.ExpansionHypercubeGraph.laplacianSpectralGapOrdered_of_fourier_eigenvalue_order (params : Parameters) (lambda : Fin (hypercubeVertexCount params) → Error) (enum : Fin (hypercubeVertexCount params) ≃ Point params) (hordered : ∀ (i j : Fin (hypercubeVertexCount params)), ↑i ≤ ↑j → lambda i ≤ lambda j) (hlambda : ∀ (i : Fin (hypercubeVertexCount params)), lambda i = laplacianEigenvalue params (enum i)) : lambda ⟨0, ⋯⟩ = 0 ∧ lambda ⟨1, ⋯⟩ = 1 / (↑params.m * ↑(hypercubeVertexCount params))

Formalization-only criterion from an explicit ordering of the Fourier eigenvalues.

This auxiliary lemma supports cor:laplacian-spectral-gap. After the roots of the characteristic polynomial have been identified with the Fourier eigenvalues of the Laplacian, an enumeration of the Fourier modes whose eigenvalues form the ordered list gives the first two ordered eigenvalues stated in the paper.

theorem MIPStarRE.LDT.ExpansionHypercubeGraph.laplacianSpectralGapOrdered (params : Parameters) (lambda : Fin (hypercubeVertexCount params) → Error) (hordered : ∀ (i j : Fin (hypercubeVertexCount params)), ↑i ≤ ↑j → lambda i ≤ lambda j) (hroots : Multiset.map Complex.re (Matrix.charpoly (matrixLaplacianOperator params)).roots = Multiset.map lambda Finset.univ.val) : lambda ⟨0, ⋯⟩ = 0 ∧ lambda ⟨1, ⋯⟩ = 1 / (↑params.m * ↑(hypercubeVertexCount params))

cor:laplacian-spectral-gap, in the ordered-eigenvalue form stated in the paper.

Paper origin: references/ldt-paper/expansion.tex:102-109.

The hypothesis hordered records the ordering lambda_1 <= lambda_2 <= ... <= lambda_M, while hroots records that the entries of lambda are the real parts of the roots of the characteristic polynomial of the actual Laplacian matrix L, counted with multiplicity. Thus hroots formalizes the paper phrase "are the eigenvalues of L"; it does not assume the Fourier diagonalization used in the proof. The conclusion is the source statement: lambda_1 = 0 and lambda_2 = 1 / (mM), with M = q^m. Lean indexes the displayed list from 0, so the first two paper eigenvalues are represented by lambda ⟨0, _⟩ and lambda ⟨1, _⟩.