Documentation

MIPStarRE.LDT.Commutativity.GCommStability.Scalar.First

Section 11 commutativity: first scalar stability bound #

The first scalar stability defect and its Cauchy--Schwarz boundedness proof.

source
noncomputable def MIPStarRE.LDT.Commutativity.gCommStabilityR {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (y : Fq params) :
SubMeas (Polynomial params) ι

The paper's slice submeasurement R^y_g = E_{u,x} \sum_a G^{u,x}_a G^y_g G^{u,x}_a.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def MIPStarRE.LDT.Commutativity.gCommStabilityScalarDefect {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (G : Fq params → SubMeas (Polynomial params) ι) (y : Fq params) :
    Error

    Named scalar defect for the first paper stability claim.

    For fixed y, this is the collapsed scalar from commutativity-G.tex, equation eq:bound-this-right-now!: gCommStabilityR contains the averaged left-register sandwich R_g^y = E_{u,x} \sum_a G_a^{u,x} G_g^y G_a^{u,x}, the factor (1 - (G y).total) is the paper's left-register (I - G^y), and IdxPolyFamily.averagedSlicePointEvaluationOperator is the right-register average E_v A^{v,y}_{g(v)}. Thus each summand has tensor placement (R_g^y (I-G^y)) ⊗ E_v A^{v,y}_{g(v)}. This is the scalar expression bounded by gCommStability_scalar, not the overlap SDDOpRel package.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem MIPStarRE.LDT.Commutativity.gCommStability_scalar {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (zeta : Error) (hnorm : strategy.state.IsNormalized) (family : IdxPolyFamily params ι) (G : Fq params → SubMeas (Polynomial params) ι) (hG : ∀ (x : Fq params), G x = (family.meas x).toSubMeas) (hbound : IdxPolyFamily.SliceBoundednessInput strategy family zeta) :
      |avgOver (uniformDistribution (Fq params)) (gCommStabilityScalarDefect params strategy family G)| ≤ √zeta

      Direct boundedness proof for the first paper scalar stability estimate.

      This is the Cauchy--Schwarz/Z^y part of references/ldt-paper/commutativity-G.tex, clm:g-comm-stability (lines 135--179). It is intentionally separate from the overlap-style gCommStability_overlap theorem: the overlap theorem bounds an internal SDDOpRel package, while this theorem uses SliceBoundednessInput to control the paper scalar defect after the finite marginalization/reindexing step.