def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.MovingDDEAsymptoticCertificate (H : Section13HatLayers) (sign : ErrorSign) (d M : ℝ) : Prop

The minimal missing Proposition 13.1 input. It is pointwise and upstream of integration: on each of the two source ranges it says that the perturbation slope is absorbed by the delayed/current DDE ratio.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.MovingDDEAsymptoticCertificate H sign d M = ∃ (D₀ : ℝ), 1 < D₀ ∧ ∀ (D : ℝ), D₀ ≤ D → M ≤ MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d ∧ (∀ (t : ℝ), M ≤ t → t ≤ Real.log D ^ (1 / d) → MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.weightedHat H sign t * MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.perturbationSlope D d 0 t ≤ t * H.T sign.opposite (t - 1) * (t ^ d / Real.log D / (1 + t ^ d / Real.log D))) ∧ ∀ (t : ℝ), Real.log D ^ (1 / d) < t → t ≤ MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d → MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.weightedHat H sign t * MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.perturbationSlope D d 0 t ≤ t * H.T sign.opposite (t - 1) * (t ^ d / Real.log D / (1 + t ^ d / Real.log D))

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.qD_eq_dde_main {H : Section13HatLayers} {D d Δ t : ℝ} (sign : ErrorSign) (hlog : 0 < Real.log D) (ht : 1 < t) : qD H sign.opposite D d Δ t = perturbation D d 0 t * (t * H.T sign.opposite (t - 1)) / (1 + t ^ d / Real.log D) * ((t - 1) / t) ^ (1 - Δ)

Express the delayed kernel as its perturbation-weighted DDE main term.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.eventually_movingSigma_large_s_differential_tail {H : Section13HatLayers} (hH : Section13HatContract H 2) (sign : ErrorSign) {d Δ t₀ : ℝ} (ht₀ : 2 < t₀) (hΔ : Δ < 1) (hcert : MovingDDEAsymptoticCertificate H sign d (t₀ + 2)) : ∃ (D₀ : ℝ), 1 < D₀ ∧ ∀ (D : ℝ), D₀ ≤ D → t₀ + 2 ≤ sourceSigma D d ∧ ∀ (s : ℝ), t₀ + 2 ≤ s → s ≤ sourceSigma D d → ∫ (t : ℝ) in s..sourceSigma D d, qD H sign.opposite D d Δ t ≤ (1 - 1 / sourceSigma D d) ^ (1 - Δ) * lambda H sign D d 0 s

The large-s moving tail from pp. 90--91. The split point is fixed as M=t₀+2; the conclusion is derived by differential domination and FTC, never assumed as a premise.