Section 12 pasting: over all outcomes — Schwartz–Zippel bounds and final assembly #
Schwartz–Zippel aggregation, the line-consistent indicator bound, and the final chained
assembly of lem:over-all-outcomes.
References #
references/ldt-paper/ld-pasting.texblueprint/src/chapter/ch09_pasting.tex
theorem
MIPStarRE.LDT.Pasting.overAllOutcomes_ofLinePointBounds
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(strategy : SymStrat params.next ι)
(eps delta gamma zeta : Error)
(heps_nonneg : 0 ≤ eps)
(hdelta_nonneg : 0 ≤ delta)
(hgamma_nonneg : 0 ≤ gamma)
(hzeta_nonneg : 0 ≤ zeta)
(hdq_le : params.d ≤ params.q)
(hd : 0 < params.d)
(family : IdxPolyFamily params ι)
(k : ℕ)
(hline : ∀ i < k, LdSandwichLineOnePointStatement params strategy family eps delta gamma zeta k i)
:
OverAllOutcomesStatement params strategy family eps delta gamma zeta k
Internal form of lem:over-all-outcomes from the one-point sandwich
estimates.
The proof of the mass comparison uses the estimates
lem:ld-sandwich-line-one-point in the interpolation-eligible case. Once those
estimates are supplied explicitly, the remaining argument only needs
nonnegativity of the scalar error parameters and the usual degree and field-size
side conditions.
theorem
MIPStarRE.LDT.Pasting.overAllOutcomes_ofGHatFacts_of_axis_self
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(strategy : SymStrat params.next ι)
(eps delta gamma zeta : Error)
(haxis : strategy.axisParallelFailureProbability ≤ eps)
(hself_good : strategy.selfConsistencyFailureProbability ≤ delta)
(hgamma_nonneg : 0 ≤ gamma)
(hzeta_nonneg : 0 ≤ zeta)
(hzeta_le : zeta ≤ 1)
(hdq_le : params.d ≤ params.q)
(hd : 0 < params.d)
(family : IdxPolyFamily params ι)
(hcons : family.ConsistentWithPoints strategy zeta)
(hfacts : GHatFactsStatement params strategy.state family gamma zeta)
(k : ℕ)
:
OverAllOutcomesStatement params strategy family eps delta gamma zeta k
Internal form of lem:over-all-outcomes from cor:G-hat-facts.
theorem
MIPStarRE.LDT.Pasting.overAllOutcomes_ofComMain_of_axis_self
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(strategy : SymStrat params.next ι)
(eps delta gamma zeta : Error)
(haxis : strategy.axisParallelFailureProbability ≤ eps)
(hself_good : strategy.selfConsistencyFailureProbability ≤ delta)
(hgamma_nonneg : 0 ≤ gamma)
(hgamma_le : gamma ≤ 1)
(hzeta_nonneg : 0 ≤ zeta)
(hzeta_le : zeta ≤ 1)
(hdq_le : params.d ≤ params.q)
(hd : 0 < params.d)
(family : IdxPolyFamily params ι)
(hcons : family.ConsistentWithPoints strategy zeta)
(hself : family.StronglySelfConsistent strategy.state zeta)
(hcom : Commutativity.ComMainConclusion params strategy family gamma zeta)
(k : ℕ)
:
OverAllOutcomesStatement params strategy family eps delta gamma zeta k
Internal form of lem:over-all-outcomes from the Section 11 commutativity
conclusion.
theorem
MIPStarRE.LDT.Pasting.overAllOutcomes
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(strategy : SymStrat params.next ι)
(eps delta gamma zeta : Error)
(hgood : strategy.IsGood eps delta gamma)
(hgamma_le : gamma ≤ 1)
(hzeta_le : zeta ≤ 1)
(hdq_le : params.d ≤ params.q)
(hd : 0 < params.d)
(family : IdxPolyFamily params ι)
(hcons : family.ConsistentWithPoints strategy zeta)
(hself : family.StronglySelfConsistent strategy.state zeta)
(hbound : IdxPolyFamily.SliceBoundednessInput strategy family zeta)
(k : ℕ)
:
OverAllOutcomesStatement params strategy family eps delta gamma zeta k
lem:over-all-outcomes.