Documentation

MIPRE.Background.LIDT.MIPStarRE.LDT.GlobalVariance.Defs.Families

Section 8 global variance: operator families #

Positivity and normalization lemmas for the point-conditioned outcome operator families used to build the global-variance comparisons.

References #

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

The squared norm expression controlled by lem:generalize-b for a fixed g. Uses bipartite state ψbi on d * d.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    noncomputable def MIPStarRE.LDT.GlobalVariance.generalizeBDeviation {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (ψbi : QuantumState (ι × ι)) (G : SubMeas (Polynomial params) ι) :

    The polynomial-averaged deviation controlled by lem:generalize-b.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      noncomputable def MIPStarRE.LDT.GlobalVariance.generalizeBCollisionResidual {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (ψbi : QuantumState (ι × ι)) (G : SubMeas (Polynomial params) ι) (g : Polynomial params) :

      The line-collision residual obtained after expanding the projective line measurement in lem:generalize-b and moving the polynomial weight from (G_g)^{1/2} to G_g. The remaining unproved analytic step is to bound this quantity by Schwartz--Zippel and the submeasurement property of G.

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

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        noncomputable def MIPStarRE.LDT.GlobalVariance.generalizeBSeedCollisionExpansion {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (ψbi : QuantumState (ι × ι)) (G : SubMeas (Polynomial params) ι) (g : Polynomial params) :

        Uniform line/parameter seed expansion of the lem:generalize-b collision residual.

        This is the paper's expansion.tex, lines 286--288, after replacing an incident line question (ℓ,u) by a line and affine parameter t with u = ℓ(t), but before commuting the finite average over t past the finite sum over line answers f. The equality from the original collision residual to this seed expansion is proved in generalizeBCollisionResidual_eq_seedCollisionExpansion.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          noncomputable def MIPStarRE.LDT.GlobalVariance.generalizeBLineCollisionExpansion {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (ψbi : QuantumState (ι × ι)) (G : SubMeas (Polynomial params) ι) (g : Polynomial params) :

          Explicit line/parameter expansion of the lem:generalize-b collision residual.

          This is the commuted finite-sum form of generalizeBSeedCollisionExpansion: for fixed and f, the coefficient is the fraction of parameters where the line answer f both collides with g|_ℓ at t and is not equal to g|_ℓ.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            noncomputable def MIPStarRE.LDT.GlobalVariance.generalizeBLeftFamily {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (G : SubMeas (Polynomial params) ι) :

            Aggregated family for the left-hand side of lem:generalize-b on the bipartite space d * d.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              noncomputable def MIPStarRE.LDT.GlobalVariance.generalizeBRightFamily {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (G : SubMeas (Polynomial params) ι) :

              Aggregated family for the right-hand side of lem:generalize-b on the bipartite space d * d.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                noncomputable def MIPStarRE.LDT.GlobalVariance.localVarianceLeftFamily {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (G : SubMeas (Polynomial params) ι) :

                Aggregated family for A^u_[g(u)] ⊗ (G_g)^{1/2} on the bipartite space d * d.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  noncomputable def MIPStarRE.LDT.GlobalVariance.localVarianceRightFamily {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (G : SubMeas (Polynomial params) ι) :

                  Aggregated family for A^v_[g(v)] ⊗ (G_g)^{1/2} on the bipartite space d * d.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    noncomputable def MIPStarRE.LDT.GlobalVariance.globalVarianceLeftFamily {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (G : SubMeas (Polynomial params) ι) :

                    The same weighted operator on the first independently sampled point. On the bipartite space d * d.

                    Equations
                    Instances For
                      noncomputable def MIPStarRE.LDT.GlobalVariance.globalVarianceRightFamily {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (G : SubMeas (Polynomial params) ι) :

                      The same weighted operator on the second independently sampled point. On the bipartite space d * d.

                      Equations
                      Instances For
                        noncomputable def MIPStarRE.LDT.GlobalVariance.localVarianceDeviationAtPolynomial {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (ψbi : QuantumState (ι × ι)) (G : SubMeas (Polynomial params) ι) (g : Polynomial params) :

                        The edgewise squared norm expression in lem:local-variance-of-points. Uses bipartite state ψbi on d * d.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          noncomputable def MIPStarRE.LDT.GlobalVariance.globalVarianceDeviationAtPolynomial {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (ψbi : QuantumState (ι × ι)) (G : SubMeas (Polynomial params) ι) (g : Polynomial params) :

                          The independently sampled squared norm expression in lem:global-variance-of-points. Uses bipartite state ψbi on d * d.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            noncomputable def MIPStarRE.LDT.GlobalVariance.localVarianceDeviation {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (ψbi : QuantumState (ι × ι)) (G : SubMeas (Polynomial params) ι) :

                            The polynomial-averaged local squared norm expression.

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

                              The displayed error term in lem:generalize-b.

                              Equations
                              Instances For

                                The post-triangle-inequality error term for the six-step transport in lem:local-variance-of-points.

                                The six comparisons at references/ldt-paper/expansion.tex, lines 305--311 have errors , , md/q, md/q, , and , whose sum is 4ε + 4δ + 2md/q. The paper then applies prop:triangle-inequality-for-approx_delta (preliminaries.tex:622--642) with k = 6, yielding 6 * (4ε + 4δ + 2md/q). This is the genuine residual that the six-step chain is expected to prove before it is absorbed by the displayed 24(ε + δ + md/q) slack.

                                Equations
                                Instances For

                                  The displayed error term in lem:local-variance-of-points.

                                  Equations
                                  Instances For

                                    The displayed error term in lem:global-variance-of-points.

                                    Equations
                                    Instances For