Documentation

MIPRE.Background.LIDT.MIPStarRE.LDT.CommutativityPoints.AnswerTheorems

Section 10 commutativity points: answer-valued diagonal measurements #

This file proves the commutativity-at-points theorem using the answer-valued diagonal-line verifier relation. The conclusion concerns only the point measurements, hence it can later be transferred to the ordinary carrier used by self-improvement, but the proof does not use the carrier's inert diagonal measurement.

References #

source
def MIPStarRE.LDT.CommutativityPoints.answerSampledPointMeasurement {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : AnswerSymStrat params ι) :
IdxSubMeas (PointDiagonalLineQuestion params) (Fq params) ι

The point measurement, reindexed by a sampled diagonal line and a parameter on it, for an answer-valued strategy.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def MIPStarRE.LDT.CommutativityPoints.answerSampledDiagonalLineEvaluation {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : AnswerSymStrat params ι) :
    IdxSubMeas (PointDiagonalLineQuestion params) (Fq params) ι

    Evaluate an answer-valued diagonal-line measurement at the sampled parameter.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def MIPStarRE.LDT.CommutativityPoints.answerPointMeasurementProductLeft {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : AnswerSymStrat params ι) :
      IdxOpFamily (GlobalVariance.PointPairQuestion params) (PointPairOutcome params) (ι × ι)

      The ordered point product (A^u_a A^v_b) ⊗ I for an answer-valued strategy.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def MIPStarRE.LDT.CommutativityPoints.answerPointMeasurementProductRight {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : AnswerSymStrat params ι) :
        IdxOpFamily (GlobalVariance.PointPairQuestion params) (PointPairOutcome params) (ι × ι)

        The reversed point product (A^v_b A^u_a) ⊗ I for an answer-valued strategy.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem MIPStarRE.LDT.CommutativityPoints.answerCommutativityPoints {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : AnswerSymStrat params ι) (eps delta gamma : Error) (hgood : strategy.IsGood eps delta gamma) :
          SDDOpRel strategy.state (uniformDistribution (GlobalVariance.PointPairQuestion params)) (answerPointMeasurementProductLeft params strategy) (answerPointMeasurementProductRight params strategy) (commutativityPointsError params gamma)

          Answer-valued form of thm:commutativity-points.

          The proof is the paper's diagonal-line bridge argument, but the diagonal-line measurement is the answer-valued measurement of strategy.