Documentation

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

Weighted operators and variance families #

noncomputable def MIPStarRE.LDT.GlobalVariance.polynomialWeightSqrtOperator {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (G : SubMeas (Polynomial params) ι) (g : Polynomial params) :

The operator (G_g)^{1/2} used throughout expansion.tex. Uses CFC.sqrt (continuous functional calculus) to compute the matrix square root of the PSD operator G.outcome g.

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

    The weighted state |ψ_g⟩ = (I ⊗ √G_g)|ψ⟩, modeled as a density-matrix transformation: ρ_g = W_g ρ W_g† where W_g = I ⊗ √(G_g).

    This is not necessarily normalized — normalization would require dividing by Tr(G_g ρ_B). We keep it unnormalized since the variance quantities in the paper use unnormalized weighted expectations.

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

      The concrete operator A^u_{g(u)} for a fixed polynomial g.

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

        The two-outcome point event selecting the answer g(u).

        This is the submeasurement form of the point operator used in the first and last steps of lem:local-variance-of-points (expansion.tex, lines 305 and 311). Its some () outcome is exactly A^u_{g(u)}; the none outcome is the complementary point-answer mass.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[simp]
          theorem MIPStarRE.LDT.GlobalVariance.pointConditionedEventSubMeasAtPolynomial_some {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (g : Polynomial params) (u : Point params) :

          The selected outcome of pointConditionedEventSubMeasAtPolynomial is A^u_{g(u)}.

          noncomputable def MIPStarRE.LDT.GlobalVariance.weightedPointConditionedOperatorAtPolynomial {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (G : SubMeas (Polynomial params) ι) (g : Polynomial params) (u : Point params) :
          Quantum.Op (ι × ι)

          The paper's weighted operator 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.weightedPointConditionedRightOperatorAtPolynomial {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (G : SubMeas (Polynomial params) ι) (g : Polynomial params) (u : Point params) :
            Quantum.Op (ι × ι)

            The right-register intermediate I ⊗ (G_g)^{1/2} A^u_{g(u)} from the first and last self-consistency moves of lem:local-variance-of-points (expansion.tex, lines 306 and 310).

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

              The local variance of A(g) on the weighted state |ψ_g⟩. Operators are lifted to the left tensor factor of the bipartite state.

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

                The global variance of A(g) on the weighted state |ψ_g⟩. Operators are lifted to the left tensor factor of the bipartite state.

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

                  The polynomial-averaged local variance of the conditioned points family.

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

                    The polynomial-averaged global variance of the conditioned points family.

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

                      The Option Unit event submeasurement selecting axis-line answers that match g(u) at the queried point u on the left side of lem:generalize-b.

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

                        The Option Unit event submeasurement selecting axis-line answers that match the restriction of g to on the right side of lem:generalize-b.

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

                          The residual projective Option Unit event from the proof of lem:generalize-b: axis-line answers that collide with g at the sampled point u, but are not the restricted polynomial g|_ℓ. After the projective-measurement expansion, the squared difference is controlled by this collision event.

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

                            The residual event above, forgetting projectivity to a submeasurement. Keeping this definition as the toSubMeas of generalizeBCollisionEventProjMeasAtPolynomial prevents the projective and submeasurement views from drifting apart.

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

                              The event operator for the residual line-collision event in lem:generalize-b.

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

                                The event operator B^ℓ_{[f(u)=g(u)]}: sum of axis-line measurement outcomes f that evaluate to the same value as g at point u.

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

                                  The event operator B^ℓ_{[f = g|_ℓ]}: sum of axis-line measurement outcomes f that agree with g restricted to line .

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

                                    The weighted left operator in 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.weightedGeneralizeBRightOperatorAtPolynomial {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (G : SubMeas (Polynomial params) ι) (g : Polynomial params) (qu : AxisParallelLineQuestion params) :
                                      Quantum.Op (ι × ι)

                                      The weighted right operator in lem:generalize-b on the bipartite space d * d.

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