Section 6 -- Axis-Parallel Restricted Probability Bounds

This module contains the axis-parallel part of the restricted-probability bookkeeping for the main induction step.

References

• blueprint/src/chapter/ch10_induction.tex

theorem MIPStarRE.LDT.MainInductionStep.weighted_axisParallel_bound {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (eps delta gamma : Error) (hgood : strategy.IsGood eps delta gamma) : (avgOver (uniformDistribution (Fq params)) fun (x : Fq params) => 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.