theorem
MathlibNt.SieveTheory.errorEnvelope_antitoneOn_plus_lowStrip
{H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers}
(hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatContract H 2)
{N : ℕ}
{D d : ℝ}
(hsign :
SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N = SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.plus)
(hd : 0 ≤ d)
(hD : 1 < D)
(hlarge : (1 + 3 * d) * 4 ^ d ≤ 1 / 3 * Real.log D)
:
AntitoneOn (SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H N D d) (Set.Icc 1 3)
On the odd predecessor's initial strip, the exact Section-13 value
weightedHat H plus = 1 turns the envelope into perturbation/t; for a
large enough recursive argument this quotient is antitone on [1,3].
theorem
MathlibNt.SieveTheory.errorEnvelope_coordinate_transport_full
{H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers}
(hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatContract H 2)
{N : ℕ}
{D d σ x y : ℝ}
(hd : 0 ≤ d)
(hD : 1 < D)
(hlarge : (1 + 3 * d) * 4 ^ d ≤ 1 / 3 * Real.log D)
(hi : SwitchingPrinciple.SuzukiLemma144KappaOne.Claim14_6_MonotoneLambdaPremise H D d σ)
(hxdom : x ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 N)
(hxy : x ≤ y)
(hyσ : y ≤ σ)
:
Full coordinate transport. The minus predecessor is already in the
Claim-14.6(i) interval. For the plus predecessor, the proof uses the exact
initial formula below 3, Claim 14.6(i) above 3, and composes the two bounds
when the coordinate pair crosses 3.