Suzuki Lemmas 14.1--14.3: explicit uniform exponential tail

This file closes the dimension-one local-product hypothesis into the pointwise Lemma 14.1 source estimate and then combines the natural-ceiling support theorem with Lemma 14.2. The resulting bound is uniform in N.

noncomputable def MathlibNt.SieveTheory.suzukiSourceL (z K : ℝ) : ℝ

The explicit source parameter supplied by the dimension-one local-product bound.

Equations

• MathlibNt.SieveTheory.suzukiSourceL z K = Real.log (Real.log z / Real.log 2) + Real.log (1 + K / Real.log 2)

theorem MathlibNt.SieveTheory.suzukiPrimeMassBelow_natCast (S : BoundingSieve) (z : ℕ) : ∑ p ∈ SwitchingPrinciple.suzukiSupportedBelow S z, S.nu p = SwitchingPrinciple.suzukiPrimeMassBelow S ↑z

The natural and real presentations of the supported prime mass agree at a natural cutoff.

theorem MathlibNt.SieveTheory.suzukiLemma14_1_pointwise_of_localProduct (S : BoundingSieve) {K : ℝ} (n D z : ℕ) (hlocal : SwitchingPrinciple.HasDimensionOneLocalProductBound S K) (hz : 2 ≤ z) : suzukiSourceV S n D z ≤ suzukiSourceL (↑z) K ^ n / ↑n.factorial

Pointwise Lemma 14.1, with its source parameter discharged directly from Suzuki's dimension-one local-product hypothesis.

theorem MathlibNt.SieveTheory.suzukiLemma14_3_natCeil_uniform_explicit (S : BoundingSieve) {N D z : ℕ} {s K : ℝ} (hlocal : SwitchingPrinciple.HasDimensionOneLocalProductBound S K) (hD : 1 < D) (hs : 2 ≤ s) (hz : z = ⌈↑D ^ (1 / s)⌉₊) : suzukiActualT S N D z ≤ suzukiSourceL (↑z) K ^ (⌊s - 2⌋₊ + 1) / ↑(⌊s - 2⌋₊ + 1).factorial * Real.exp (suzukiSourceL (↑z) K)

The explicit form of Lemma 14.3 at the natural-ceiling cutoff. Here M = ⌊s - 2⌋₊ + 1; all former majorant, power, and mass premises have been eliminated, and the right-hand side is independent of N.