Documentation

MIPRE.Background.LIDT.MIPStarRE.LDT.Commutativity.Transport.FullSlice.Averages

Full-slice averages and index equivalences #

Zero-family definition, shared average-reindexing helpers, and averaged scalar and tensor quantities for the full-slice outcome space, together with data-reindexing equivalences.

The tensor-form averages are internal to the scalar/tensor comparison recorded in docs/decisions/713-scalar-tensor-decision.md; downstream code should use the scalar public API.

References #

theorem MIPStarRE.LDT.Commutativity.fullSliceCommutation_avg_swap_terms {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) :
((avgOver (uniformDistribution (FullSliceQuestion params)) fun (q : FullSliceQuestion params) => gh : FullSliceOutcome params, fullSliceBABTerm params strategy family q gh) = avgOver (uniformDistribution (FullSliceQuestion params)) fun (q : FullSliceQuestion params) => gh : FullSliceOutcome params, fullSliceABATerm params strategy family q gh) (avgOver (uniformDistribution (FullSliceQuestion params)) fun (q : FullSliceQuestion params) => gh : FullSliceOutcome params, fullSliceBABATerm params strategy family q gh) = avgOver (uniformDistribution (FullSliceQuestion params)) fun (q : FullSliceQuestion params) => gh : FullSliceOutcome params, fullSliceABABTerm params strategy family q gh

Swapping the full-slice question and outcome identifies the averaged BAB/ABA terms and the averaged BABA/ABAB terms.

noncomputable def MIPStarRE.LDT.Commutativity.zeroFullSliceOpFamily {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] :
OpFamily (FullSliceOutcome params) (ι × ι)

The zero operator family on the full-slice outcome space.

Equations
Instances For
    noncomputable def MIPStarRE.LDT.Commutativity.fullSliceABAAvg {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) :

    Full-slice ABA scalar average: E_{x,y} ∑_{g,h} ⟨ψ| G^x_g G^y_h G^x_g ⊗ I |ψ⟩.

    Full-polynomial analog of the evaluated evaluatedSliceABATerm (line 664); obtained from it by replacing the evaluated outcomes a,b with polynomial outcomes g,h summed over FullSliceOutcome.

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

      Full-slice ABAB scalar average: E_{x,y} ∑_{g,h} ⟨ψ| G^x_g G^y_h G^x_g G^y_h ⊗ I |ψ⟩.

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

        Evaluated-slice ABA scalar average: E_{u,v,x,y} ∑_{a,b} ⟨ψ| G^x_[g(u)=a] G^y_[h(v)=b] G^x_[g(u)=a] ⊗ I |ψ⟩.

        Averaged analog of evaluatedSliceABATerm (line 664) over the full slice question.

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

          Evaluated-slice ABAB scalar average: E_{u,v,x,y} ∑_{a,b} ⟨ψ| G^x_[g(u)=a] G^y_[h(v)=b] G^x_[g(u)=a] G^y_[h(v)=b] ⊗ I |ψ⟩.

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

            Full-slice BAB ⊗ A tensor average (paper eq:gcom4 RHS, commutativity-G.tex line 334): E_{x,y} ∑_{g,h} ⟨ψ| G^y_h G^x_g G^y_h ⊗ G^x_g |ψ⟩.

            This is the manifestly-PSD tensor-form partner of fullSliceABAAvg used by the marginalization step: each summand factors as V† V with V = (G^x_g G^y_h) ⊗ √(G^x_g), so the outer absolute value drops and the Schwartz–Zippel collision bound applies per outcome. This tensor-form average is internal to the scalar public API recorded by decision #713.

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

              Full-slice ABA ⊗ B tensor average (y-side analogue): E_{x,y} ∑_{g,h} ⟨ψ| G^x_g G^y_h G^x_g ⊗ G^y_h |ψ⟩.

              Naming convention (consistent with the sibling fullSliceBABAtensorAvg for BAB ⊗ A): the four-letter operator string ABAB decomposes as left register ABA followed by right register B. This is not the same operator as the scalar fullSliceABABAvg, whose left register is the full quartic G^x_g G^y_h G^x_g G^y_h; the tensorAvg suffix marks the tensor split.

              The manifestly-PSD tensor-form partner of fullSliceABABAvg reached from it by closenessOfIP (moving the trailing G^y_h factor from the left register to the right). Each summand factors as V† V with V = (G^y_h G^x_g) ⊗ √(G^y_h). Internal per #713.

              The evaluated-side analogue is evaluatedSliceABABtensorAvg below.

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

                Evaluated-slice ABA ⊗ B tensor average (evaluated-side analogue of fullSliceABABtensorAvg): E_{u,v,x,y} ∑_{a,b} ⟨ψ| G^x_[g(u)=a] G^y_[h(v)=b] G^x_[g(u)=a] ⊗ G^y_[h(v)=b] |ψ⟩.

                This is the second tensor-form endpoint in paper commutativity-G.tex lines 356-360. The scalar-to-tensor comparison evaluatedSliceABAB_scalar_to_ABABtensor reaches it by moving the trailing G^y_[h(v)=b] factor from the left register to the right register.

                The shared tensor endpoint is defined here so the evaluated-side transport lemmas can use the same notation as the full-slice transport lemmas.

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

                  X-evaluated BAB ⊗ A tensor average.

                  This is the intermediate obtained from fullSliceBABAtensorAvg after postprocessing only the first/full-x polynomial outcome by a sampled point u : Point params; the second/y polynomial outcome remains full. The x-side tensor marginalization lemma below identifies its difference from the full tensor average with fullSliceBABAxCollisionFactored.

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

                    X-evaluated, y-full ABAB scalar average.

                    This is the scalar endpoint in the display from eq:evaluate-gcom-at-points to eq:don't-understand-the-numbering-system: the x polynomial outcome has been postprocessed at u, but the second closenessOfIP move has not yet transferred the trailing G^y_h to the right register.

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

                      X-evaluated, y-full ABA ⊗ B tensor average.

                      This is the y-side intermediate in paper eq:evaluate-gcom-at-points-part-dos: the first/x family has already been postprocessed at u, while the second/y family still ranges over full polynomial outcomes. The y-side tensor marginalization lemma below compares this to evaluatedSliceABABtensorAvg.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        theorem MIPStarRE.LDT.Commutativity.avgOver_xEvaluatedQuestion_to_pointNext (params : Parameters) [FieldModel params.q] (f : Point params.nextError) :
                        (avgOver (uniformDistribution (Point params × FullSliceQuestion params)) fun (ux : Point params × FullSliceQuestion params) => f (appendPoint params ux.1 ux.2.1)) = avgOver (uniformDistribution (Point params.next)) f

                        Averaging mixed x-evaluated data and ignoring the full-y coordinate gives the uniform average over Point params.next.

                        theorem MIPStarRE.LDT.Commutativity.xEvaluatedSliceBABAtensorAvg_eq_xFullData {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) :
                        xEvaluatedSliceBABAtensorAvg params strategy family = avgOver (uniformDistribution (Point params × FullSliceQuestion params)) fun (ux : Point params × FullSliceQuestion params) => have A := evaluateAt params ux.1 (family.meas ux.2.1).toSubMeas; have B := (family.meas ux.2.2).toSubMeas; a : Fq params, h : Polynomial params, ev strategy.state (leftTensor (B.outcome h * A.outcome a * B.outcome h) * rightTensor (A.outcome a))

                        Reindex xEvaluatedSliceBABAtensorAvg into the mixed (u,x,y) data order.

                        Reindex evaluated-slice questions as ((u, (x, y)), v).

                        This product order is tailored to the y-marginalization expansion: the residual is indexed by the already x-evaluated data (u, x, y), and the remaining uniform average is over the y-evaluation point v.

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