Suzuki §13 hat layers at sieve dimension one

This file records the literal κ=1 specialization of (13.1)--(13.7), rather than inventing a finite parity sum for T̂⁺,T̂⁻. In this branch κ̂=κ=1 and β̂=β; the weighted functions are s² T̂±(s).

Suzuki defines the hat layers as solutions of a delay differential equation with initial data and exponential decay. Section 13 does not define finite partial sums for them. The finite-level results below mean results on a compact interval [a,b]; the only limit input needed to turn the DDE into the tail integral (13.12)/(13.14) is decay at infinity.

def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.weightedHat (H : Section13HatLayers) (sign : ErrorSign) (s : ℝ) : ℝ

The weighted Section 13 unknown s^(κ̂+1) T̂±(s) at κ=1.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.weightedHat H sign s = s ^ 2 * H.T sign s

structure MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatContract (H : Section13HatLayers) (β : ℝ) : Prop

Literal κ=1 data from Suzuki (T1)--(T5), (13.2), and (13.7). The derivative equation is (T3); weighted_tendsto_zero is the only limiting input and follows in the paper from (T5).

• betaHat_eq : H.betaHat = β
• beta_gt_one : 1 < β
• continuous (sign : ErrorSign) : ContinuousOn (H.T sign) (Set.Ioi 0)
• positive (sign : ErrorSign) (s : ℝ) : 0 < s → 0 < H.T sign s
• initial_plus (s : ℝ) : 0 < s → s ≤ β + 1 → weightedHat H ErrorSign.plus s = β - 1
• initial_minus (s : ℝ) : 0 < s → s ≤ β → weightedHat H ErrorSign.minus s = β
• dde (sign : ErrorSign) (s : ℝ) : β + sign.epsilon < s → HasDerivAt (weightedHat H sign) (-s * H.T sign.opposite (s - 1)) s
• weighted_tendsto_zero (sign : ErrorSign) : Filter.Tendsto (weightedHat H sign) Filter.atTop (nhds 0)

@[simp]

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.kappaHat_eq_one (H : Section13HatLayers) : H.kappaHat = 1

@[simp]

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.lambda_eq_perturb_mul_weightedHat (H : Section13HatLayers) (sign : ErrorSign) (D d ε t : ℝ) : lambda H sign D d ε t = (1 + (t + ε) ^ d / Real.log D) ^ t * weightedHat H sign t

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.weightedHat_antitoneOn_Icc {H : Section13HatLayers} {β a b : ℝ} (hH : Section13HatContract H β) (sign : ErrorSign) (ha : β + sign.epsilon < a) : AntitoneOn (weightedHat H sign) (Set.Icc a b)

On every finite interval strictly beyond the delay threshold, (T3) and positivity already imply that s² T̂±(s) is antitone. No limiting theorem is used here.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.lambda_antitoneOn_Icc_of_deriv_nonpos (H : Section13HatLayers) (sign : ErrorSign) (D d ε a b : ℝ) (hcont : ContinuousOn (lambda H sign D d ε) (Set.Icc a b)) (hdiff : ∀ t ∈ Set.Ioo a b, DifferentiableAt ℝ (fun (x : ℝ) => lambda H sign D d ε x) t) (hderiv : ∀ t ∈ Set.Ioo a b, deriv (lambda H sign D d ε) t ≤ 0) : AntitoneOn (lambda H sign D d ε) (Set.Icc a b)

A finite-interval product criterion isolating exactly the local estimate needed in Claim 14.6(i). This is the rigorous content of the step from (14.16)+(T3) to a decreasing Λ: once the displayed derivative is nonpositive, ordinary one-variable calculus supplies antitonicity.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.AntitoneOn.mul_nonneg_on {f g : ℝ → ℝ} {S : Set ℝ} (hf : AntitoneOn f S) (hg : AntitoneOn g S) (hf0 : ∀ x ∈ S, 0 ≤ f x) (hg0 : ∀ x ∈ S, 0 ≤ g x) : AntitoneOn (fun (x : ℝ) => f x * g x) S

Multiplying two nonnegative antitone functions preserves antitonicity on a fixed set. This is the algebraic engine in the high-range part of Claim 14.6(ii), after (14.15).

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.ratio_rpow_antitoneOn_Ioi {Δ : ℝ} (hΔ : -1 ≤ Δ) : AntitoneOn (fun (t : ℝ) => (t / (t - 1)) ^ (1 + Δ)) (Set.Ioi 1)

The elementary ratio factor in (14.15) is antitone on (1,∞) whenever 1+Δ ≥ 0.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.qD_mul_antitoneOn_of_factors (H : Section13HatLayers) (sign : ErrorSign) (D d Δ : ℝ) {S : Set ℝ} (hLambda : AntitoneOn (fun (t : ℝ) => lambda H sign.opposite D d 1 (t - 1)) S) (hRatio : AntitoneOn (fun (t : ℝ) => (t / (t - 1)) ^ (1 + Δ)) S) (hLambda0 : ∀ t ∈ S, 0 ≤ lambda H sign.opposite D d 1 (t - 1)) (hRatio0 : ∀ t ∈ S, 0 ≤ (t / (t - 1)) ^ (1 + Δ)) (hgt1 : ∀ t ∈ S, 1 < t) : AntitoneOn (fun (t : ℝ) => qD H sign.opposite D d Δ t * t) S

A source-neutral high-range form of Claim 14.6(ii). It makes explicit that (14.15) reduces the claim to antitonicity of the shifted Λ₁ factor and of the ratio power. Suzuki treats the short remaining interval separately using (T4); it is not a consequence of Claim 14.6(i) alone.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.qD_mul_antitoneOn_of_shifted_lambda (H : Section13HatLayers) (sign : ErrorSign) (D d Δ : ℝ) {S : Set ℝ} (hΔ : -1 ≤ Δ) (hS : S ⊆ Set.Ioi 1) (hLambda : AntitoneOn (fun (t : ℝ) => lambda H sign.opposite D d 1 (t - 1)) S) (hLambda0 : ∀ t ∈ S, 0 ≤ lambda H sign.opposite D d 1 (t - 1)) : AntitoneOn (fun (t : ℝ) => qD H sign.opposite D d Δ t * t) S

High-range Claim 14.6(ii) with the ratio monotonicity discharged. The only remaining analytic input is decrease of the shifted Λ₁ factor.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.antitoneOn_of_pointwise_limit {u : ℕ → ℝ → ℝ} {f : ℝ → ℝ} {S : Set ℝ} (hu : ∀ (n : ℕ), AntitoneOn (u n) S) (hlim : ∀ x ∈ S, Filter.Tendsto (fun (n : ℕ) => u n x) Filter.atTop (nhds (f x))) : AntitoneOn f S

Pointwise convergence preserves antitonicity. Thus any genuine finite construction of the Section 13 solutions needs only pointwise convergence to pass weighted monotonicity to the limit; uniform convergence is required only for continuity/differentiation, not for this order statement.

structure MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Claim14_6FiniteApproximation (H : Section13HatLayers) (sign : ErrorSign) (D d ε a b : ℝ) : Type

Exact separation of finite and limiting obligations for Claim 14.6(i).

• approx : ℕ → ℝ → ℝ
• antitone (n : ℕ) : AntitoneOn (self.approx n) (Set.Icc a b)
• pointwise (x : ℝ) : x ∈ Set.Icc a b → Filter.Tendsto (fun (n : ℕ) => self.approx n x) Filter.atTop (nhds (lambda H sign D d ε x))

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.claim14_6_i_of_finiteApproximation {H : Section13HatLayers} {sign : ErrorSign} {D d ε a b : ℝ} (h : Claim14_6FiniteApproximation H sign D d ε a b) : AntitoneOn (lambda H sign D d ε) (Set.Icc a b)

Once a source construction supplies finite antitone approximants and their pointwise limit, Claim 14.6(i) on that compact interval is automatic.

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

The delayed positive integrand in the κ=1 Section 13 DDE.

Equations

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

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.integral_hatTailIntegrand {H : Section13HatLayers} {β a b : ℝ} (hH : Section13HatContract H β) (sign : ErrorSign) (ha : β + sign.epsilon < a) (hab : a ≤ b) : ∫ (t : ℝ) in a..b, hatTailIntegrand H sign t = weightedHat H sign a - weightedHat H sign b

The DDE integrated on a finite interval.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.integrableOn_hatTailIntegrand_Ioi {H : Section13HatLayers} {β a : ℝ} (hH : Section13HatContract H β) (sign : ErrorSign) (ha : β + sign.epsilon < a) : MeasureTheory.IntegrableOn (hatTailIntegrand H sign) (Set.Ioi a) MeasureTheory.volume

The delayed DDE integrand is integrable on every tail beyond the threshold.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.integral_Ioi_hatTailIntegrand {H : Section13HatLayers} {β a : ℝ} (hH : Section13HatContract H β) (sign : ErrorSign) (ha : β + sign.epsilon < a) : ∫ (t : ℝ) in Set.Ioi a, hatTailIntegrand H sign t = weightedHat H sign a

κ=1 tail identity obtained by integrating the Section 13 DDE to infinity.