Section 6 -- Diagonal Restricted Probability Bounds #
This module contains the diagonal-line part of the restricted-probability bookkeeping for the main induction step.
References #
blueprint/src/chapter/ch10_induction.tex
theorem
MIPStarRE.LDT.MainInductionStep.weighted_diagonal_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).diagonalFailureProbability) ≤ gamma
The weighted average of the restricted diagonal slice errors is bounded by the ambient diagonal-line test error.