Statement structures

structure MIPStarRE.LDT.GlobalVariance.GeneralizeBStatement {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (ψbi : QuantumState (ι × ι)) (G : SubMeas (Polynomial params) ι) : Prop

Paper origin: references/ldt-paper/expansion.tex:273-291 (\label{lem:generalize-b}).

Conclusion statement for lem:generalize-b. ψbi is the bipartite state on d * d (passed as strategy.state by callers).

• aggregateFamilyComparison : SDDRel ψbi (axisParallelLineQuestionDistribution params) (generalizeBLeftFamily params strategy G) (generalizeBRightFamily params strategy G) (generalizeBError params)

  The aggregated left and right generalize-b families are close in SDDRel.

• pointwiseNormBound (g : Polynomial params) : generalizeBDeviationAtPolynomial params strategy ψbi G g ≤ generalizeBError params

  Each fixed polynomial satisfies the claimed deviation bound.

• averagedNormBound : generalizeBDeviation params strategy ψbi G ≤ generalizeBError params

  The polynomial average of the deviations satisfies the same bound.

structure MIPStarRE.LDT.GlobalVariance.LocalVarianceOfPointsStatement {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (ψbi : QuantumState (ι × ι)) (G : SubMeas (Polynomial params) ι) (eps delta : Error) : Prop

Paper origin: references/ldt-paper/expansion.tex:292-324 (\label{lem:local-variance-of-points}).

Conclusion statement for lem:local-variance-of-points.

• aggregateEdgeComparison : SDDRel ψbi (ExpansionHypercubeGraph.rerandomizeCoord params) (localVarianceLeftFamily params strategy G) (localVarianceRightFamily params strategy G) (localVarianceOfPointsError params eps delta)

  The aggregated edge families are close in SDDRel.

• pointwiseEdgeNormBound (g : Polynomial params) : localVarianceDeviationAtPolynomial params strategy ψbi G g ≤ localVarianceOfPointsError params eps delta

  Each fixed polynomial satisfies the edgewise squared-difference bound.

• pointwiseLocalVarianceBound (g : Polynomial params) : pointConditionedLocalVarianceAtPolynomial params strategy G g ≤ localVarianceOfPointsError params eps delta

  Each fixed polynomial satisfies the local-variance bound.

• averagedLocalVarianceBound : pointConditionedLocalVariance params strategy G ≤ localVarianceOfPointsError params eps delta

  The polynomial average of the local variances satisfies the same bound.

structure MIPStarRE.LDT.GlobalVariance.GlobalVarianceOfPointsStatement {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (ψbi : QuantumState (ι × ι)) (G : SubMeas (Polynomial params) ι) (eps delta : Error) : Prop

Paper origin: references/ldt-paper/expansion.tex:325-353 (\label{lem:global-variance-of-points}).

Conclusion statement for lem:global-variance-of-points.

• aggregateGlobalComparison : SDDRel ψbi (ExpansionHypercubeGraph.independentPointPair params) (globalVarianceLeftFamily params strategy G) (globalVarianceRightFamily params strategy G) (globalVarianceOfPointsError params eps delta)

  The aggregated global families are close in SDDRel.

• pointwiseGlobalNormBound (g : Polynomial params) : globalVarianceDeviationAtPolynomial params strategy ψbi G g ≤ globalVarianceOfPointsError params eps delta

  Each fixed polynomial satisfies the global squared-difference bound.

• pointwiseExpansionTransfer (g : Polynomial params) : pointConditionedGlobalVarianceAtPolynomial params strategy G g ≤ ↑params.m * pointConditionedLocalVarianceAtPolynomial params strategy G g

  Each fixed polynomial satisfies the local-to-global transfer estimate.

• pointwiseGlobalVarianceBound (g : Polynomial params) : pointConditionedGlobalVarianceAtPolynomial params strategy G g ≤ globalVarianceOfPointsError params eps delta

  Each fixed polynomial satisfies the claimed global-variance bound.

• averagedGlobalVarianceBound : pointConditionedGlobalVariance params strategy G ≤ globalVarianceOfPointsError params eps delta

  The polynomial average of the global variances satisfies the same bound.