Documentation

MIPStarRE.LDT.MainInductionStep.Theorems.RestrictedProbabilities.Core

Section 6 -- Restricted Probability Statement #

This module collects the axis-parallel, self-consistency, and diagonal restricted-probability estimates into the statement used by the main induction step.

References #

source
theorem MIPStarRE.LDT.MainInductionStep.RestrictedProbabilitiesStatement.ofWeightedBounds {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (eps delta gamma : Error) (hgood : strategy.IsGood eps delta gamma) (haxisWeightedBound : (avgOver (uniformDistribution (Fq params)) fun (x : Fq params) => sliceTransverseDirectionWeight params * (xRestrictedStrategy params strategy x).axisParallelFailureProbability) ≤ eps) (hdiagonalWeightedBound : (avgOver (uniformDistribution (Fq params)) fun (x : Fq params) => sliceTransverseDirectionWeight params * (xRestrictedStrategy params strategy x).diagonalFailureProbability) ≤ gamma) :
RestrictedProbabilitiesStatement params strategy eps delta gamma

Data weighted restricted axis/diagonal bounds into the public RestrictedProbabilitiesStatement.

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

lem:restricted-probabilities.