Suzuki Lemma 14.3: explicit logarithmic exponent

This file converts a bound of the form

T ≤ L^M / M! * exp L

into a completely explicit exponential bound. The final theorem takes M = ⌊s - 2⌋₊ + 1; the hypothesis exp 1 * L ≤ s - 2 is an explicit (non-asymptotic) large-cutoff condition ensuring that the floor error has the favourable sign.

theorem MathlibNt.SieveTheory.exp_nat_mul_log_sub_nat_le_factorial (m : ℕ) (hm : 0 < m) : Real.exp (↑m * Real.log ↑m - ↑m) ≤ ↑m.factorial

The elementary lower bound m! ≥ exp (m log m - m). We retain only the main two terms of Mathlib's global Stirling lower bound.

theorem MathlibNt.SieveTheory.pow_div_factorial_mul_exp_le_logExponent {L T : ℝ} {M : ℕ} (hL : 0 < L) (hM : 0 < M) (hT : T ≤ L ^ M / ↑M.factorial * Real.exp L) : T ≤ Real.exp (L + ↑M * (1 + Real.log L - Real.log ↑M))

Exact log-exponent conversion at a positive integer cutoff. This is the form to use immediately after obtaining the standard exponential-tail bound L^M / M! * exp L.

theorem MathlibNt.SieveTheory.floorTail_le_claim145_logExponent {s L T : ℝ} (hL : 0 < L) (hlarge : Real.exp 1 * L ≤ s - 2) (hT : T ≤ L ^ (⌊s - 2⌋₊ + 1) / ↑(⌊s - 2⌋₊ + 1).factorial * Real.exp L) : T ≤ Real.exp (L + (s - 2) * (1 + Real.log L - Real.log (s - 2)))

Floor-error conversion in the exact cutoff used by Suzuki Lemma 14.3.

The explicit condition exp 1 * L ≤ s - 2 implies both positivity and that x ↦ x (1 + log L - log x) is already decreasing in the only comparison needed here. Since

s - 2 < ⌊s - 2⌋₊ + 1,

the integer exponent can therefore be replaced by the real endpoint s - 2 without any hidden asymptotic predicate or Big-O constant.

theorem MathlibNt.SieveTheory.suzukiExponentialTail_le_claim145_logExponent {s L : ℝ} (hL : 0 < L) (hlarge : Real.exp 1 * L ≤ s - 2) (htail : suzukiExponentialTail L (⌊s - 2⌋₊ + 1) ≤ L ^ (⌊s - 2⌋₊ + 1) / ↑(⌊s - 2⌋₊ + 1).factorial * Real.exp L) : suzukiExponentialTail L (⌊s - 2⌋₊ + 1) ≤ Real.exp (L + (s - 2) * (1 + Real.log L - Real.log (s - 2)))

Direct consumer for the tail object occurring in Lemma 14.3. The standard L^M/M! * exp L estimate is kept as an explicit premise, so this theorem can be composed with any proof of that estimate without changing constants.

theorem MathlibNt.SieveTheory.suzukiLemma14_3_uniform_logExponent (S : BoundingSieve) {N D z : ℕ} {s L : ℝ} (hz : 0 < z) (hL : 0 < L) (hpow : z ^ (⌊s - 2⌋₊ + 2) ≤ D) (h141 : SuzukiLemma141Majorant S D z L) (hlarge : Real.exp 1 * L ≤ s - 2) (htail : suzukiExponentialTail L (⌊s - 2⌋₊ + 1) ≤ L ^ (⌊s - 2⌋₊ + 1) / ↑(⌊s - 2⌋₊ + 1).factorial * Real.exp L) : suzukiActualT S N D z ≤ Real.exp (L + (s - 2) * (1 + Real.log L - Real.log (s - 2)))

Suzuki Lemma 14.3 with the exponential tail converted all the way to the logarithmic exponent consumed in subsequent Claim-14.5 comparisons. Every constant and threshold condition is explicit.