Documentation

MIPRE.Background.LIDT.MIPStarRE.LDT.Test.StrategyFailures

Symmetrized-strategy failure probabilities and test bounds #

Failure-probability surrogates and basic low-individual-degree test bounds for the split strategy interface.

Symmetrized strategies and tested-branch bounds #

source
noncomputable def MIPStarRE.LDT.SymStrat.axisParallelFailureProbability {params : Parameters} [FieldModel params.q] {ι : Type u_1} [Fintype ι] [DecidableEq ι] (strategy : SymStrat params ι) :
Error

Trace-based failure surrogate for the axis-parallel lines test. Point answers on the left register, line answers (evaluated at the base point) on the right register of the bipartite state.

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

    Trace-based failure surrogate for the self-consistency test. Uses bipartite SSC defect (cross-register overlap). For projective measurements this equals bipartiteConsError between the same measurement on both registers.

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

      Trace-based failure surrogate for the diagonal lines test. Averages over the restriction index j ∈ {0, …, m − 1}, then over the j-restricted diagonal test. For each j, direction vectors have the last m − j − 1 coordinates equal to zero.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        structure MIPStarRE.LDT.SymStrat.IsGood {params : Parameters} {ι : Type u_1} [Fintype ι] [DecidableEq ι] [FieldModel params.q] (strategy : SymStrat params ι) (eps delta gamma : Error) :
        Prop

        The paper's notion of an (ε,δ,γ)-good symmetric strategy.

        Matches the paper's Definition 3.1: three test-passing bounds with no extra hypotheses. The reparametrization covariance that was formerly listed here is now a structural property of SymStrat, where it belongs (the paper treats diagonal measurements as geometrically covariant by construction).

        Instances For
          source
          theorem MIPStarRE.LDT.diagonalFailureProbability_nonneg (params : Parameters) [FieldModel params.q] {ι : Type u_1} [Fintype ι] [DecidableEq ι] (strategy : SymStrat params ι) :
          0 ≤ strategy.diagonalFailureProbability

          The diagonal-line failure surrogate is nonnegative.

          source
          theorem MIPStarRE.LDT.eps_nonneg_of_isGood (params : Parameters) [FieldModel params.q] {ι : Type u_1} [Fintype ι] [DecidableEq ι] (strategy : SymStrat params ι) {eps delta gamma : Error} (hgood : strategy.IsGood eps delta gamma) :
          0 ≤ eps

          A good symmetric strategy has a nonnegative axis-parallel error parameter ε.

          source
          theorem MIPStarRE.LDT.delta_nonneg_of_isGood (params : Parameters) [FieldModel params.q] {ι : Type u_1} [Fintype ι] [DecidableEq ι] (strategy : SymStrat params ι) {eps delta gamma : Error} (hgood : strategy.IsGood eps delta gamma) :
          0 ≤ delta

          A good symmetric strategy has a nonnegative self-consistency error parameter δ.

          source
          theorem MIPStarRE.LDT.gamma_nonneg_of_isGood (params : Parameters) [FieldModel params.q] {ι : Type u_1} [Fintype ι] [DecidableEq ι] (strategy : SymStrat params ι) {eps delta gamma : Error} (hgood : strategy.IsGood eps delta gamma) :
          0 ≤ gamma

          A good symmetric strategy has a nonnegative diagonal-lines error parameter γ.

          Answer-valued symmetric strategies #

          source
          theorem MIPStarRE.LDT.answer_diagonalFailureProbability_nonneg (params : Parameters) [FieldModel params.q] {ι : Type u_1} [Fintype ι] [DecidableEq ι] (strategy : AnswerSymStrat params ι) :
          0 ≤ strategy.diagonalFailureProbability

          The answer-valued diagonal-line failure surrogate is nonnegative.

          source
          theorem MIPStarRE.LDT.answer_eps_nonneg_of_isGood (params : Parameters) [FieldModel params.q] {ι : Type u_1} [Fintype ι] [DecidableEq ι] (strategy : AnswerSymStrat params ι) {eps delta gamma : Error} (hgood : strategy.IsGood eps delta gamma) :
          0 ≤ eps

          A good answer-valued symmetric strategy has a nonnegative axis-parallel error parameter ε.

          source
          theorem MIPStarRE.LDT.answer_delta_nonneg_of_isGood (params : Parameters) [FieldModel params.q] {ι : Type u_1} [Fintype ι] [DecidableEq ι] (strategy : AnswerSymStrat params ι) {eps delta gamma : Error} (hgood : strategy.IsGood eps delta gamma) :
          0 ≤ delta

          A good answer-valued symmetric strategy has a nonnegative self-consistency error parameter δ.

          source
          theorem MIPStarRE.LDT.answer_gamma_nonneg_of_isGood (params : Parameters) [FieldModel params.q] {ι : Type u_1} [Fintype ι] [DecidableEq ι] (strategy : AnswerSymStrat params ι) {eps delta gamma : Error} (hgood : strategy.IsGood eps delta gamma) :
          0 ≤ gamma

          A good answer-valued symmetric strategy has a nonnegative diagonal-lines error parameter γ.

          source
          theorem MIPStarRE.LDT.three_summand_bounds_of_average_le {axis point diagonal eps : Error} (haxis : 0 ≤ axis) (hpoint : 0 ≤ point) (hdiagonal : 0 ≤ diagonal) (hmain : (axis + point + diagonal) / 3 ≤ eps) :
          axis ≤ 3 * eps ∧ point ≤ 3 * eps ∧ diagonal ≤ 3 * eps

          If three nonnegative summands have average at most eps, each summand is at most 3 * eps.