noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.compactDerivativeRatio (H : Section13HatLayers) (sign : ErrorSign) (t : ℝ) : ℝ

The pointwise DDE allowance divided by the positive weighted hat layer.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.compactDerivativeRatio H sign t = t * H.T sign.opposite (t - 1) / MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.weightedHat H sign t

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.compactDerivativeRatio_continuousOn {H : Section13HatLayers} (hH : Section13HatContract H 2) (sign : ErrorSign) (M : ℝ) : ContinuousOn (compactDerivativeRatio H sign) (Set.Icc 2 M)

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.compactDerivativeRatio_pos {H : Section13HatLayers} (hH : Section13HatContract H 2) (sign : ErrorSign) {t : ℝ} (ht : 2 ≤ t) : 0 < compactDerivativeRatio H sign t

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.exists_compactDerivativeRatio_bounds {H : Section13HatLayers} (hH : Section13HatContract H 2) {M : ℝ} (hM : 3 ≤ M) : ∃ (m : ℝ) (B : ℝ), 0 < m ∧ ∀ (sign : ErrorSign), ∀ t ∈ Set.Icc 2 M, m ≤ compactDerivativeRatio H sign t ∧ compactDerivativeRatio H sign t ≤ B

On a fixed compact head, the two DDE/weighted-hat ratios admit common strictly positive lower and finite upper bounds. Both bounds are independent of the sign, of ε ∈ {0,1}, and of the point in the head.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.eventually_derivativeDDE_domination_on_compactRange {H : Section13HatLayers} (hH : Section13HatContract H 2) {d M : ℝ} (hd : 0 ≤ d) (hM : 3 ≤ M) : ∃ (D₀ : ℝ), 1 < D₀ ∧ ∀ (D : ℝ), D₀ ≤ D → ∀ (sign : ErrorSign) (ε t : ℝ), ε = 0 ∨ ε = 1 → 2 + sign.epsilon < t → t ≤ M → weightedHat H sign t * perturbationSlope D d ε t ≤ t * H.T sign.opposite (t - 1)

Claim 14.6(i), compact-head part: after one threshold depending only on the fixed endpoint M (and on H,d), the exact derivative domination holds uniformly for both signs, both shifts ε = 0,1, and every 2 + sign.epsilon < t ≤ M. No certificate assumption is used.