noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.perturbation (D d ε t : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.perturbation D d ε t = (1 + (t + ε) ^ d / Real.log D) ^ t

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.tendsto_fixed_perturbation (d t : ℝ) : Filter.Tendsto (fun (D : ℝ) => perturbation D d 0 t) Filter.atTop (nhds 1)

For fixed exponent and point, the zero-shift perturbation tends to one.

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.perturbationSlope (D d ε t : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.perturbationSlope D d ε t = Real.log (1 + (t + ε) ^ d / Real.log D) + t * (d * (t + ε) ^ (d - 1) / Real.log D) / (1 + (t + ε) ^ d / Real.log D)

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.perturbationSlope_le {D d ε t σ : ℝ} (hlog : 0 < Real.log D) (hd : 0 ≤ d) (ht : 1 ≤ t) (htσ : t ≤ σ) (hε0 : 0 ≤ ε) (hε1 : ε ≤ 1) : perturbationSlope D d ε t ≤ (1 + σ * d) * (σ + 1) ^ d / Real.log D

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.hasDerivAt_perturbation {D d ε t : ℝ} (hlog : 0 < Real.log D) (hte : 0 < t + ε) : HasDerivAt (perturbation D d ε) (perturbation D d ε t * (Real.log (1 + (t + ε) ^ d / Real.log D) + t * (d * (t + ε) ^ (d - 1) / Real.log D) / (1 + (t + ε) ^ d / Real.log D))) t

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.hasDerivAt_lambda_of_contract {H : Section13HatLayers} {β D d ε t : ℝ} (hH : Section13HatContract H β) (sign : ErrorSign) (hlog : 0 < Real.log D) (hte : 0 < t + ε) (hthreshold : β + sign.epsilon < t) : HasDerivAt (lambda H sign D d ε) (perturbation D d ε t * (weightedHat H sign t * (Real.log (1 + (t + ε) ^ d / Real.log D) + t * (d * (t + ε) ^ (d - 1) / Real.log D) / (1 + (t + ε) ^ d / Real.log D)) - t * H.T sign.opposite (t - 1))) t

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.lambda_antitoneOn_Icc_of_log_bound {H : Section13HatLayers} {β D d ε σ ρ : ℝ} (hH : Section13HatContract H β) (sign : ErrorSign) (hd : 0 ≤ d) (hε0 : 0 ≤ ε) (hε1 : ε ≤ 1) (hσ : β + sign.epsilon ≤ σ) (_hρ : 0 < ρ) (hlog : 0 < Real.log D) (hDlarge : (1 + σ * d) * (σ + 1) ^ d ≤ ρ * Real.log D) (hdelay : ∀ (t : ℝ), β + sign.epsilon < t → t ≤ σ → ρ * weightedHat H sign t ≤ t * H.T sign.opposite (t - 1)) : AntitoneOn (lambda H sign D d ε) (Set.Icc (β + sign.epsilon) σ)

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.exists_delayRatioMargin {H : Section13HatLayers} {β σ : ℝ} (hH : Section13HatContract H β) (sign : ErrorSign) (hσ : β + sign.epsilon ≤ σ) : ∃ (ρ : ℝ), 0 < ρ ∧ ∀ (t : ℝ), β + sign.epsilon ≤ t → t ≤ σ → ρ * weightedHat H sign t ≤ t * H.T sign.opposite (t - 1)

On a compact Section 13 interval, positivity and continuity give a uniform positive lower bound for the delayed-to-current ratio.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.exists_common_delayRatioMargin {H : Section13HatLayers} {β σ : ℝ} (hH : Section13HatContract H β) (hσ : ∀ (sign : ErrorSign), β + sign.epsilon ≤ σ) : ∃ (ρ : ℝ), 0 < ρ ∧ ∀ (sign : ErrorSign) (t : ℝ), β + sign.epsilon < t → t ≤ σ → ρ * weightedHat H sign t ≤ t * H.T sign.opposite (t - 1)

The two signs admit one common positive delay-ratio margin on their compact intervals. This discharges the old source-level hdelay premise internally.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.claim14_6_i_of_log_bound {H : Section13HatLayers} {β D d σ ρ : ℝ} (hH : Section13HatContract H β) (hd : 0 ≤ d) (hσ : ∀ (sign : ErrorSign), β + sign.epsilon ≤ σ) (hρ : 0 < ρ) (hlog : 0 < Real.log D) (hDlarge : (1 + σ * d) * (σ + 1) ^ d ≤ ρ * Real.log D) (hdelay : ∀ (sign : ErrorSign) (t : ℝ), β + sign.epsilon < t → t ≤ σ → ρ * weightedHat H sign t ≤ t * H.T sign.opposite (t - 1)) (sign : ErrorSign) (ε : ℝ) : ε = 0 ∨ ε = 1 → AntitoneOn (lambda H sign D d ε) (Set.Icc (β + sign.epsilon) σ)

Quantitative Claim 14.6(i): one common delay-ratio margin ρ works for both ε=0,1; the displayed lower bound on log D is sufficient.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.claim14_6_i_for_sufficiently_large_D {H : Section13HatLayers} {β d σ : ℝ} (hH : Section13HatContract H β) (hd : 0 ≤ d) (hσ : ∀ (sign : ErrorSign), β + sign.epsilon ≤ σ) : ∃ (D₀ : ℝ), 1 < D₀ ∧ ∀ (D : ℝ), D₀ ≤ D → ∀ (sign : ErrorSign) (ε : ℝ), ε = 0 ∨ ε = 1 → AntitoneOn (lambda H sign D d ε) (Set.Icc (β + sign.epsilon) σ)

Claim 14.6(i) with no external delay-margin premise: Section 13 positivity and continuity first produce a common margin for both signs, and every D beyond an explicit existential threshold makes both ε = 0,1 lambda factors antitone on their compact intervals.