Section 6 — Averaged Slice Error Bounds: Core Estimates

This module contains the Jensen and averaging estimates for ordinary and answer-valued restricted slice errors.

theorem MIPStarRE.LDT.MainInductionStep.average_sliceSelfImprovementError_le {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (eps delta gamma : Error) (hgood : strategy.IsGood eps delta gamma) (hrestrict : SliceRestrictionData params strategy eps delta gamma) : (avgOver (uniformDistribution (Fq params)) fun (x : Fq params) => sliceSelfImprovementError params hrestrict x) ≤ selfImprovementInInductionError params.next eps delta gamma

Averaging the slice self-improvement errors gives the paper's displayed bound on \mathbb{E}_x[\zeta_x], i.e. the first inequality from inductive_step.tex:555-567.

theorem MIPStarRE.LDT.MainInductionStep.average_sliceError_le {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (eps delta gamma : Error) (k : ℕ) (hgood : strategy.IsGood eps delta gamma) (hrestrict : SliceRestrictionData params strategy eps delta gamma) (hinduction : PerSliceInductionData params strategy eps delta gamma hrestrict k) : avgOver (uniformDistribution (Fq params)) hinduction.sliceError ≤ ↑params.m ^ 2 * (mainInductionNu params.next k eps delta gamma + Real.exp (-(↑k / (80000 * ↑params.m ^ 2))))

Averaging the recursive slice errors \sigma_x and telescoping the slice main-induction bound yields the paper's \mathbb{E}_x[\sigma_x] estimate used in the final pasting-data record error calculation.

theorem MIPStarRE.LDT.MainInductionStep.average_answerSuccessorSliceSelfImprovementError_le {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : AnswerSymStrat params.next ι) (eps delta gamma : Error) (hgood : strategy.IsGood eps delta gamma) (profile : AnswerSuccessorRestrictedFailureProfile params strategy) (haxis : averageAnswerSuccessorRestrictedAxisParallelError params profile ≤ sliceConditioningLoss params * eps) (hself : averageAnswerSuccessorRestrictedSelfConsistencyError params profile ≤ delta) : (avgOver (uniformDistribution (Fq params)) fun (x : Fq params) => selfImprovementInInductionError params (profile.axisParallel x) (profile.selfConsistency x) (profile.diagonal x)) ≤ selfImprovementInInductionError params.next eps delta gamma

Answer-valued successor analogue of the averaged self-improvement error estimate.

For the restricted profiles of an ambient AnswerSymStrat successor, the average of the slice errors \zeta_x is bounded by the next-dimensional quantity \zeta. This is the scalar part of the answer-valued self-improvement averaging in inductive_step.tex:486-551.

theorem MIPStarRE.LDT.MainInductionStep.average_answerSuccessorSliceMainInductionNu_le {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : AnswerSymStrat params.next ι) (eps delta gamma : Error) (k : ℕ) (hgood : strategy.IsGood eps delta gamma) (profile : AnswerSuccessorRestrictedFailureProfile params strategy) (haxis : averageAnswerSuccessorRestrictedAxisParallelError params profile ≤ sliceConditioningLoss params * eps) (hself : averageAnswerSuccessorRestrictedSelfConsistencyError params profile ≤ delta) (hdiag : averageAnswerSuccessorRestrictedDiagonalError params profile ≤ sliceConditioningLoss params * gamma) : (avgOver (uniformDistribution (Fq params)) fun (x : Fq params) => mainInductionNu params k (profile.axisParallel x) (profile.selfConsistency x) (profile.diagonal x)) ≤ mainInductionNu params.next k eps delta gamma

Answer-valued successor analogue of the averaged recursive induction parameter estimate.

For an ambient AnswerSymStrat in dimension m + 1, the restricted answer-valued slice profile satisfies the same Jensen and conditioning estimate as in the ordinary successor route. This is the scalar calculation needed after the recursive answer-valued predecessor calls.

theorem MIPStarRE.LDT.MainInductionStep.average_answerSuccessorSliceMainInductionError_le {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : AnswerSymStrat params.next ι) (eps delta gamma : Error) (k : ℕ) (hgood : strategy.IsGood eps delta gamma) (profile : AnswerSuccessorRestrictedFailureProfile params strategy) (haxis : averageAnswerSuccessorRestrictedAxisParallelError params profile ≤ sliceConditioningLoss params * eps) (hself : averageAnswerSuccessorRestrictedSelfConsistencyError params profile ≤ delta) (hdiag : averageAnswerSuccessorRestrictedDiagonalError params profile ≤ sliceConditioningLoss params * gamma) : (avgOver (uniformDistribution (Fq params)) fun (x : Fq params) => mainInductionError params k (profile.axisParallel x) (profile.selfConsistency x) (profile.diagonal x)) ≤ ↑params.m ^ 2 * (mainInductionNu params.next k eps delta gamma + Real.exp (-(↑k / (80000 * ↑params.m ^ 2))))

Average of the recursive main-induction errors for answer-valued successor slices.

This is the scalar estimate used after applying the predecessor answer-valued induction hypothesis to each restricted successor slice.