Suzuki Lemma 14.3: an N-uniform exponential-tail domination

This file proves the non-asymptotic core of Lemma 14.3 for the actual discrete parity sum suzukiActualT. It does not use eventual emptiness of the finite prime support and it does not scan over depths. The only analytic input is the pointwise Lemma 14.1 majorant; the lower cutoff is obtained from the actual support-vanishing theorem.

The production source objects specialize Suzuki's parameter to β = 2. Thus ⌊s - 2⌋₊ + 1 is the first possibly nonzero layer. The hypothesis z ^ (⌊s - 2⌋₊ + 2) ≤ D is the exact natural-number support condition needed below (and is the form consumed from the real logarithmic coordinate bridge).

noncomputable def MathlibNt.SieveTheory.suzukiExponentialTail (L : ℝ) (M : ℕ) : ℝ

The exponential series restricted to indices n ≥ M.

Equations

• MathlibNt.SieveTheory.suzukiExponentialTail L M = ∑' (n : ℕ), if M ≤ n then L ^ n / ↑n.factorial else 0

def MathlibNt.SieveTheory.SuzukiLemma141Majorant (S : BoundingSieve) (D z : ℕ) (L : ℝ) : Prop

The expected pointwise interface of Suzuki Lemma 14.1. It is deliberately pointwise, rather than an assumption of the desired tail estimate.

Equations

• MathlibNt.SieveTheory.SuzukiLemma141Majorant S D z L = ∀ (n : ℕ), MathlibNt.SieveTheory.suzukiSourceV S n D z ≤ L ^ n / ↑n.factorial

def MathlibNt.SieveTheory.SuzukiActualSupportVanishing (S : BoundingSieve) (D z : ℕ) (β s : ℝ) : Prop

The support statement used in Suzuki's proof: layers at or below s - β vanish. This names the expected support interface without assuming any tail estimate.

Equations

• MathlibNt.SieveTheory.SuzukiActualSupportVanishing S D z β s = ∀ (n : ℕ), ↑n ≤ s - β → MathlibNt.SieveTheory.suzukiSourceV S n D z = 0

theorem MathlibNt.SieveTheory.suzukiSourceV_eq_zero_below_cutoff (S : BoundingSieve) {M n D z : ℕ} (hz : 0 < z) (hpow : z ^ (M + 2) ≤ D) (hn : n ≤ M) : suzukiSourceV S n D z = 0

Actual source support vanishing below a natural cutoff. This is a direct consumer of the source-faithful support theorem, not finite-support emptiness.

theorem MathlibNt.SieveTheory.suzukiActualT_le_exponentialTail_of_support (S : BoundingSieve) {N D z M : ℕ} {L : ℝ} (hL : 0 ≤ L) (hzero : ∀ n < M, suzukiSourceV S n D z = 0) (h141 : SuzukiLemma141Majorant S D z L) : suzukiActualT S N D z ≤ suzukiExponentialTail L M

Abstract finite-to-infinite step in Suzuki Lemma 14.3. The finite carrier may depend on N; the right side does not.

theorem MathlibNt.SieveTheory.suzukiActualT_le_uniform_tsum (S : BoundingSieve) {N D z : ℕ} {β s L : ℝ} (hβs : β ≤ s) (hL : 0 ≤ L) (hsupport : SuzukiActualSupportVanishing S D z β s) (h141 : SuzukiLemma141Majorant S D z L) : suzukiActualT S N D z ≤ ∑' (n : ℕ), if ⌊s - β⌋₊ + 1 ≤ n then L ^ n / ↑n.factorial else 0

Generic-β formulation of the exact tail stage. It combines the actual support cutoff and the Lemma 14.1 pointwise estimate, and removes both the parity restriction and the upper endpoint N.

theorem MathlibNt.SieveTheory.suzukiLemma14_3_uniform_exponentialTail (S : BoundingSieve) {N D z : ℕ} {s L : ℝ} (hz : 0 < z) (_hs : 2 ≤ s) (hL : 0 ≤ L) (hpow : z ^ (⌊s - 2⌋₊ + 2) ≤ D) (h141 : SuzukiLemma141Majorant S D z L) : suzukiActualT S N D z ≤ suzukiExponentialTail L (⌊s - 2⌋₊ + 1)

Suzuki Lemma 14.3 at the exact exponential-tail stage (β = 2). This is uniform in N: no term on the right depends on N.

theorem MathlibNt.SieveTheory.suzukiLemma14_3_uniform_tsum (S : BoundingSieve) {N D z : ℕ} {s L : ℝ} (hz : 0 < z) (hs : 2 ≤ s) (hL : 0 ≤ L) (hpow : z ^ (⌊s - 2⌋₊ + 2) ≤ D) (h141 : SuzukiLemma141Majorant S D z L) : suzukiActualT S N D z ≤ ∑' (n : ℕ), if ⌊s - 2⌋₊ + 1 ≤ n then L ^ n / ↑n.factorial else 0

Spelling out the tail makes the floor endpoint and the absence of N on its right-hand side explicit.