Documentation

MIPRE.Background.LIDT.Co.MainInductionStep.Theorems.RestrictedProbabilities.Axis

Section 6 — Axis-parallel restricted probability bounds #

The axis-parallel part of the restricted-probability bookkeeping for the main induction step: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/MainInductionStep/Theorems/RestrictedProbabilities/Axis.lean in the port of planning/c6b-plan.md (milestone M12, section "Port conventions").

A strategy is a SymStrat params.next 𝔓 K (Co/Test/StrategyCore.lean), whose state is the symmetric model strategy.state : SymModel 𝔓 K; the vendored qBipartiteConsDefect strategy.state A B is strategy.state.qBipartiteConsDefect A B (Co/Test/Defs.lean), with the point answers placed by S.L and the line answers by S.R, and errors are real numbers (the vendored Error := ℝ). The restricted strategy keeps the state, so every restricted defect is a defect of strategy.state.

The restricted axis-parallel measurement (restrictAxisParallelMeasurement, Co MainInductionStep/Defs.lean) is the transport of the ambient one along axisLinePolynomialEquiv up to its total, 1 against the ambient total, which equals 1; so restrictedAxisSampleError_eq is one extensionality step and SubMeas.postprocess_transport, as in the vendored proof. The vendored avg_congr steps are written with avgOver_congr, and the try rfl steps of the vendored file are gone.

Not ported #

Every declaration of the vendored file has a counterpart here.

References #

In LionSR/MIPStarRE at commit 507e8122, not in this repository:

source
theorem MIPRE.LIDT.Co.MainInductionStep.restrictedAxisSampleError_eq {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (x : MIPStarRE.LDT.Fq params) (u : MIPStarRE.LDT.Point params) (i : Fin params.m) :
strategy.state.qBipartiteConsDefect ((xRestrictedStrategy params strategy x).axisParallelPointAnswerFamily (u, i)) ((xRestrictedStrategy params strategy x).axisParallelLineAnswerFamily (u, i)) = strategy.state.qBipartiteConsDefect (axisParallelPointAnswerFamily strategy (MIPStarRE.LDT.appendPoint params u x, MIPStarRE.LDT.embedCoord params i)) (axisParallelLineAnswerFamily strategy (MIPStarRE.LDT.appendPoint params u x, MIPStarRE.LDT.embedCoord params i))

The axis-parallel defect of the x-restricted strategy at the slice sample (u, i) is the ambient defect at the appended point (u, x) and the embedded direction i.

source
noncomputable def MIPRE.LIDT.Co.MainInductionStep.sliceAxisDirectionError {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (x : MIPStarRE.LDT.Fq params) (i : Fin params.m) :
ℝ

Per-direction axis-parallel consistency defect of the restricted x-slice strategy at embedded direction i, averaged over the slice point space Point params.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def MIPRE.LIDT.Co.MainInductionStep.axisDirectionError {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (i : Fin params.next.m) :
    ℝ

    Per-direction axis-parallel consistency defect of the ambient (m+1)-dimensional strategy at direction i, averaged over the ambient point space Point params.next.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem MIPRE.LIDT.Co.MainInductionStep.sliceAxisDirectionErrorAverage_eq_axisDirectionError {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (i : Fin params.m) :
      (MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Fq params)) fun (x : MIPStarRE.LDT.Fq params) => sliceAxisDirectionError params strategy x i) = axisDirectionError params strategy (MIPStarRE.LDT.embedCoord params i)

      Averaging the restricted per-direction axis-parallel error over the slice height gives the ambient per-direction error at the embedded direction.

      source
      theorem MIPRE.LIDT.Co.MainInductionStep.averageRestrictedAxisFailure_eq_embeddedAxisDirections {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) :
      (MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Fq params)) fun (x : MIPStarRE.LDT.Fq params) => (xRestrictedStrategy params strategy x).axisParallelFailureProbability) = MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (Fin params.m)) fun (i : Fin params.m) => axisDirectionError params strategy (MIPStarRE.LDT.embedCoord params i)

      The average over slice heights of the restricted axis-parallel failure probability is the average over embedded directions of the ambient per-direction error.

      source
      theorem MIPRE.LIDT.Co.MainInductionStep.weighted_axisParallel_bound {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (eps delta gamma : ℝ) (hgood : strategy.IsGood eps delta gamma) :
      (MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Fq params)) fun (x : MIPStarRE.LDT.Fq params) => MIPStarRE.LDT.MainInductionStep.sliceTransverseDirectionWeight params * (xRestrictedStrategy params strategy x).axisParallelFailureProbability) ≤ eps

      The weighted average of the restricted axis-parallel slice errors is bounded by the ambient axis-parallel test error.