Documentation

MIPRE.Background.LIDT.MIPStarRE.LDT.CommutativityPoints.Approximation

Section 10 — commutativity points approximation layer #

Restricted-diagonal approximation infrastructure for commutativity at points.

source
def MIPStarRE.LDT.CommutativityPoints.pointNextEquiv (params : Parameters) [FieldModel params.q] :
Point params.next ≃ Point params × Fq params

Decompose a point in Point params.next into its truncated point and final coordinate.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem MIPStarRE.LDT.CommutativityPoints.avgOver_uniform_pointNext_decompose (params : Parameters) [FieldModel params.q] (f : Point params.next → Error) :
    avgOver (uniformDistribution (Point params.next)) f = avgOver (uniformDistribution (Fq params)) fun (x : Fq params) => avgOver (uniformDistribution (Point params)) fun (u : Point params) => f (appendPoint params u x)

    Decompose the uniform average over a next-level point into a height and prefix average.

    source
    theorem MIPStarRE.LDT.CommutativityPoints.avgOver_uniform_pointNext_height (params : Parameters) [FieldModel params.q] (f : Fq params → Error) :
    (avgOver (uniformDistribution (Point params.next)) fun (u : Point params.next) => f (pointHeight params u)) = avgOver (uniformDistribution (Fq params)) f

    Marginalizing a uniform point in Point params.next to its height coordinate gives the uniform distribution on Fq params.

    source
    noncomputable def MIPStarRE.LDT.CommutativityPoints.opFamilyOfOutcome {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Outcome : Type u_2} [Fintype Outcome] (outcome : Outcome → Quantum.Op ι) :
    OpFamily Outcome ι

    Build an operator family from its outcomes, taking the total to be their sum.

    Equations
    Instances For
      source
      @[reducible, inline]
      abbrev MIPStarRE.LDT.CommutativityPoints.pointPairOutcomeSwapEquiv (params : Parameters) :
      PointPairOutcome params ≃ PointPairOutcome params
      Equations
      Instances For
        source
        theorem MIPStarRE.LDT.CommutativityPoints.sampledDiagonalLineApproximation_pointWithDiagonalLine {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (eps delta gamma : Error) (hgood : strategy.IsGood eps delta gamma) :
        SDDRel strategy.state (pointWithDiagonalLineDistribution params) (sampledPointMeasurement params strategy).liftLeft (sampledDiagonalLineEvaluation params strategy).liftRight (pointDiagonalLineApproxError params gamma)

        Transport the corrected restricted-diagonal approximation bound to the shared point-with-diagonal-line distribution used downstream.

        The reindexing runs through rebasedLastRestrictedQuestionEquiv, which turns a restricted sample together with an evaluation parameter into the corresponding rebased diagonal-line question.

        source
        theorem MIPStarRE.LDT.CommutativityPoints.answer_sampledDiagonalLineApproximation_pointWithDiagonalLine {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : AnswerSymStrat params ι) (eps delta gamma : Error) (hgood : strategy.IsGood eps delta gamma) :
        SDDRel strategy.state (pointWithDiagonalLineDistribution params) (IdxSubMeas.liftLeft fun (q : PointDiagonalLineQuestion params) => (strategy.pointMeasurement (sampledPointFromDiagonalQuestion params q)).toSubMeas) (IdxSubMeas.liftRight fun (q : PointDiagonalLineQuestion params) => postprocess (strategy.diagonalMeasurement.toIdxProjMeas q.1).toSubMeas fun (f : DiagonalLineAnswer params) => f q.2) (pointDiagonalLineApproxError params gamma)

        Answer-valued version of sampledDiagonalLineApproximation_pointWithDiagonalLine.

        This is the Section 10 diagonal approximation needed by the answer-valued commutativity route: it uses the answer-valued diagonal verifier relation directly and does not pass through an ordinary dummy diagonal measurement.