Section 12 pasting: scalar bounds for complementary Bernoulli branches

This file collects the elementary scalar estimates used by the complementary branches of thm:ld-pasting. These estimates correspond to the large-error reduction in references/ldt-paper/ld-pasting.tex, lines 52--55.

theorem MIPStarRE.LDT.Pasting.kappa_nonneg_of_complete {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) {kappa : Error} (hcomplete : family.Complete strategy.state kappa) : 0 ≤ kappa

The scalar κ in a complete family is nonnegative.

theorem MIPStarRE.LDT.Pasting.ldPasting_kappa_coefficient_nonneg (params : Parameters) : 0 ≤ 1 + 1 / (100 * ↑params.m)

The coefficient multiplying κ in the pasting error is nonnegative.

theorem MIPStarRE.LDT.Pasting.ldPasting_degreeRatio_nonneg (params : Parameters) [FieldModel params.q] : 0 ≤ ↑params.d / ↑params.q

The ratio d / q is nonnegative in the error scalar field.

theorem MIPStarRE.LDT.Pasting.one_le_ldPastingNu_coefficient (params : Parameters) (k : ℕ) (hk_pos : 1 ≤ k) : 1 ≤ 100 * ↑k ^ 2 * ↑params.m

The scalar coefficient multiplying the five small error terms is at least one when the number of sampled coordinates is positive.

theorem MIPStarRE.LDT.Pasting.one_le_ldPastingNu_of_one_le_sum (params : Parameters) (k : ℕ) (eps delta gamma zeta : Error) (hk_pos : 1 ≤ k) (hsum : 1 ≤ Real.rpow eps (1 / 32) + Real.rpow delta (1 / 32) + Real.rpow gamma (1 / 32) + Real.rpow zeta (1 / 32) + Real.rpow (↑params.d / ↑params.q) (1 / 32)) : 1 ≤ MainInductionStep.ldPastingInInductionNu params k eps delta gamma zeta

A unit lower bound on the five-term scalar sum gives a unit lower bound on the section-local pasting parameter ν.

theorem MIPStarRE.LDT.Pasting.one_le_ldPastingError_of_one_le_nu (params : Parameters) (k : ℕ) (eps delta gamma kappa zeta : Error) (hkappa_nonneg : 0 ≤ kappa) (hnu : 1 ≤ MainInductionStep.ldPastingInInductionNu params k eps delta gamma zeta) : 1 ≤ MainInductionStep.ldPastingInInductionError params k eps delta gamma kappa zeta

A unit lower bound on ν gives a unit lower bound on the final pasting error.

theorem MIPStarRE.LDT.Pasting.one_le_ldPastingError_of_k_eq_zero (params : Parameters) (k : ℕ) (eps delta gamma kappa zeta : Error) (hkappa_nonneg : 0 ≤ kappa) (hk_zero : k = 0) : 1 ≤ MainInductionStep.ldPastingInInductionError params k eps delta gamma kappa zeta

If k = 0, the exponential term alone gives the trivial pasting bound.

theorem MIPStarRE.LDT.Pasting.one_le_ldPastingNu_of_large_gamma {ι : 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) (family : IdxPolyFamily params ι) (hcons : family.ConsistentWithPoints strategy zeta) (k : ℕ) (hk_pos : 1 ≤ k) (hgamma : 1 < gamma) : 1 ≤ MainInductionStep.ldPastingInInductionNu params k eps delta gamma zeta

The ν term is at least one when γ > 1 and k ≥ 1.

theorem MIPStarRE.LDT.Pasting.one_le_ldPastingNu_of_large_zeta {ι : 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) (k : ℕ) (hk_pos : 1 ≤ k) (hzeta : 1 < zeta) : 1 ≤ MainInductionStep.ldPastingInInductionNu params k eps delta gamma zeta

The ν term is at least one when ζ > 1 and k ≥ 1.

theorem MIPStarRE.LDT.Pasting.one_le_ldPastingNu_of_large_degreeRatio {ι : 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) (family : IdxPolyFamily params ι) (hcons : family.ConsistentWithPoints strategy zeta) (k : ℕ) (hk_pos : 1 ≤ k) (hdq : params.q < params.d) : 1 ≤ MainInductionStep.ldPastingInInductionNu params k eps delta gamma zeta

The ν term is at least one when d / q > 1 and k ≥ 1.