Section 7 hypercube graph: core definitions

Vertex-set cardinality and the hypercube graph edge relation on F_q^m.

References

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

def MIPStarRE.LDT.ExpansionHypercubeGraph.hypercubeVertexCount (params : Parameters) : ℕ

The number of vertices in the hypercube graph C.

Equations

• MIPStarRE.LDT.ExpansionHypercubeGraph.hypercubeVertexCount params = params.q ^ params.m

def MIPStarRE.LDT.ExpansionHypercubeGraph.coordinateDisagreementSet (params : Parameters) (u v : Point params) : Finset (Fin params.m)

The set of coordinates on which two points disagree.

Equations

• MIPStarRE.LDT.ExpansionHypercubeGraph.coordinateDisagreementSet params u v = {i : Fin params.m | u i ≠ v i}

def MIPStarRE.LDT.ExpansionHypercubeGraph.coordinateDisagreementCount (params : Parameters) (u v : Point params) : ℕ

The number of coordinates on which two points disagree.

Equations

• MIPStarRE.LDT.ExpansionHypercubeGraph.coordinateDisagreementCount params u v = (MIPStarRE.LDT.ExpansionHypercubeGraph.coordinateDisagreementSet params u v).card

def MIPStarRE.LDT.ExpansionHypercubeGraph.IsHypercubeEdge (params : Parameters) (u v : Point params) : Prop

The hypercube edge relation: two points differ in at most one coordinate.

Equations

• MIPStarRE.LDT.ExpansionHypercubeGraph.IsHypercubeEdge params u v = (MIPStarRE.LDT.ExpansionHypercubeGraph.coordinateDisagreementCount params u v ≤ 1)

@[instance_reducible]

instance MIPStarRE.LDT.ExpansionHypercubeGraph.instDecidableIsHypercubeEdge (params : Parameters) (u v : Point params) : Decidable (IsHypercubeEdge params u v)

Decidability of the hypercube edge relation, obtained from the finite coordinate disagreement count.

Equations

• MIPStarRE.LDT.ExpansionHypercubeGraph.instDecidableIsHypercubeEdge params u v = id inferInstance

@[instance_reducible]

instance MIPStarRE.LDT.ExpansionHypercubeGraph.instDecidablePredHypercubeEdgePair (params : Parameters) : DecidablePred fun (uv : Point params × Point params) => IsHypercubeEdge params uv.1 uv.2

Decidable predicate form of the hypercube edge relation on ordered pairs of vertices.

Equations

• MIPStarRE.LDT.ExpansionHypercubeGraph.instDecidablePredHypercubeEdgePair params uv = inferInstance

noncomputable def MIPStarRE.LDT.ExpansionHypercubeGraph.rerandomizeCoordWeight (params : Parameters) (u v : Point params) : Error

Edge sampling by rerandomizing a single coordinate. This is the Section 7.1 distribution: pick u ∈ F_q^m, i ∈ {1, ..., m}, and x ∈ F_q uniformly, then set v = u[i ↦ x].

Equations

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

@[reducible, inline]

abbrev MIPStarRE.LDT.ExpansionHypercubeGraph.RerandomizeCoordSample (params : Parameters) : Type

The finite sample space for a rerandomized hypercube edge: a point, a coordinate, and the new value placed in that coordinate.

Equations

• MIPStarRE.LDT.ExpansionHypercubeGraph.RerandomizeCoordSample params = ((MIPStarRE.LDT.Point params × Fin params.m) × MIPStarRE.LDT.Fq params)

def MIPStarRE.LDT.ExpansionHypercubeGraph.rerandomizeCoordSampleToPair (params : Parameters) (sample : RerandomizeCoordSample params) : Point params × Point params

The map from a rerandomization sample to the corresponding ordered edge.

Equations

• MIPStarRE.LDT.ExpansionHypercubeGraph.rerandomizeCoordSampleToPair params sample = (sample.1.1, Function.update sample.1.1 sample.1.2 sample.2)

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

The probability distribution on ordered edges of the hypercube graph used in the paper's local variance. It samples a vertex u, a coordinate, and a new coordinate value, then records the ordered pair (u, v).

Equations

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

theorem MIPStarRE.LDT.ExpansionHypercubeGraph.rerandomizeCoord_isProbability (params : Parameters) : (rerandomizeCoord params).IsProbability

The rerandomized-coordinate edge distribution is a probability distribution.

theorem MIPStarRE.LDT.ExpansionHypercubeGraph.rerandomizeCoord_toPMF (params : Parameters) : (rerandomizeCoord params).toPMF ⋯ = PMF.map (rerandomizeCoordSampleToPair params) (PMF.uniformOfFintype (RerandomizeCoordSample params))

The rerandomized-coordinate distribution is the Mathlib push-forward of the uniform PMF on its finite sample space.

theorem MIPStarRE.LDT.ExpansionHypercubeGraph.rerandomizeCoord_mass_eq_one (params : Parameters) : ∑ uv ∈ (rerandomizeCoord params).support, (rerandomizeCoord params).weight uv = 1

The rerandomized-coordinate edge distribution has total mass one.

theorem MIPStarRE.LDT.ExpansionHypercubeGraph.avgOver_rerandomizeCoord_eq_uniform_sample (params : Parameters) (f : Point params × Point params → Error) : avgOver (rerandomizeCoord params) f = avgOver (uniformDistribution (RerandomizeCoordSample params)) fun (sample : RerandomizeCoordSample params) => f (rerandomizeCoordSampleToPair params sample)

Averaging over rerandomizeCoord is the same as averaging over the uniform sample space of a point, a coordinate, and a replacement coordinate value.

theorem MIPStarRE.LDT.ExpansionHypercubeGraph.avgOver_rerandomizeCoord_eq_weight_sum (params : Parameters) (f : Point params × Point params → Error) : avgOver (rerandomizeCoord params) f = ∑ uv : Point params × Point params, rerandomizeCoordWeight params uv.1 uv.2 * f uv

The push-forward presentation of rerandomizeCoord has the same averages as the explicit counting coefficient rerandomizeCoordWeight.

The explicit coefficient remains useful for the matrix calculation of the hypercube adjacency and Laplacian. This lemma identifies its weighted sum with the probability-side push-forward average.

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

The product distribution on two independently sampled hypercube vertices, used in the paper's global variance.

Equations

• MIPStarRE.LDT.ExpansionHypercubeGraph.independentPointPair params = MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params × MIPStarRE.LDT.Point params)

def MIPStarRE.LDT.ExpansionHypercubeGraph.pointHilbertSpace (params : Parameters) : MakingMeasurementsProjective.FiniteHilbertSpace

An honest finite matrix register for the hypercube vertices.

Equations

• MIPStarRE.LDT.ExpansionHypercubeGraph.pointHilbertSpace params = { carrier := MIPStarRE.LDT.Point params, instFintype := inferInstance, instDecidableEq := inferInstance, instNonempty := ⋯ }

noncomputable def MIPStarRE.LDT.ExpansionHypercubeGraph.hypercubeAdjacencyWeight (params : Parameters) (u v : Point params) : ℂ

The paper's normalized adjacency weight for an ordered pair of vertices. This update-sum is equivalent to the older case-split via coordinateDisagreementCount: when u ≠ v, each differing coordinate contributes the unique update sending u i to v i, while when u = v the q self-loop updates contribute once for each coordinate.

Equations

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

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

The actual adjacency matrix of the edge-graph on F_q^m.

Equations

• MIPStarRE.LDT.ExpansionHypercubeGraph.matrixAdjacencyOperator params u v = MIPStarRE.LDT.ExpansionHypercubeGraph.hypercubeAdjacencyWeight params u v

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

The actual Laplacian matrix (1 / M) I - K on the vertex register.

Equations

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

noncomputable def MIPStarRE.LDT.ExpansionHypercubeGraph.adjacency (params : Parameters) : Quantum.Op (Point params)

The normalized adjacency matrix K of the hypercube graph on F_q^m, as a matrix indexed by Point params directly.

Equations

• MIPStarRE.LDT.ExpansionHypercubeGraph.adjacency params = MIPStarRE.LDT.ExpansionHypercubeGraph.matrixAdjacencyOperator params

noncomputable def MIPStarRE.LDT.ExpansionHypercubeGraph.laplacian (params : Parameters) : Quantum.Op (Point params)

The Laplacian L = (1/M) I - K on the hypercube vertex space, as a matrix indexed by Point params directly.

Equations

• MIPStarRE.LDT.ExpansionHypercubeGraph.laplacian params = MIPStarRE.LDT.ExpansionHypercubeGraph.matrixLaplacianOperator params

noncomputable def MIPStarRE.LDT.ExpansionHypercubeGraph.laplacianDifferenceForm (params : Parameters) : Quantum.Op (Point params)

The edge-difference form of the Laplacian from prop:laplacian-rewrite: L = (1/2) · 𝔼_{(u,v)∼C} (|u⟩-|v⟩)(⟨u|-⟨v|).

Defined entrywise via the rerandomizeCoordWeight distribution on ordered vertex pairs: at index (a, b) the projector |u⟩⟨v| becomes the indicator [a = u][v = b]. The equality with laplacian is proved in MIPStarRE.LDT.ExpansionHypercubeGraph.laplacian_eq_edgeDifferenceForm.

Equations

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

noncomputable def MIPStarRE.LDT.ExpansionHypercubeGraph.pointDifferenceSquaredOperator {ι : Type u_1} [Fintype ι] {params : Parameters} (A : Point params → Quantum.Op ι) (u v : Point params) : Quantum.Op ι

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

Equations

• MIPStarRE.LDT.ExpansionHypercubeGraph.pointDifferenceSquaredOperator A u v = Matrix.conjTranspose (A u - A v) * (A u - A v)

noncomputable def MIPStarRE.LDT.ExpansionHypercubeGraph.localVariance {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) (A : Point params → Quantum.Op ι) (ψ : QuantumState ι) : Error

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

Equations

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

noncomputable def MIPStarRE.LDT.ExpansionHypercubeGraph.globalVariance {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) (A : Point params → Quantum.Op ι) (ψ : QuantumState ι) : Error

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

Equations

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

noncomputable def MIPStarRE.LDT.ExpansionHypercubeGraph.localAndVariance {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) (A : Point params → Quantum.Op ι) (ψ : QuantumState ι) : Error × Error

Combined accessor for the local and global variances.

Equations

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

@[reducible, inline]

abbrev MIPStarRE.LDT.ExpansionHypercubeGraph.combinedColumnIndex (params : Parameters) (ι : Type u_2) : Type u_2

The column-space indices for A_combine.

Equations

• MIPStarRE.LDT.ExpansionHypercubeGraph.combinedColumnIndex params ι = (MIPStarRE.LDT.Point params × ι)

noncomputable def MIPStarRE.LDT.ExpansionHypercubeGraph.combinedOperator {ι : Type u_1} (params : Parameters) (A : Point params → Quantum.Op ι) : Matrix (combinedColumnIndex params ι) ι ℂ

The combined column operator used for the trace rewrites. Its u-th block is (A^u)ᴴ, so that the resulting trace expands to τ(ρ · (A^u - A^v)ᴴ (A^u - A^v)) for arbitrary operator families.

Equations

• MIPStarRE.LDT.ExpansionHypercubeGraph.combinedOperator params A ui j = star (A ui.1 j ui.2)