Growth of Liu's prime-divisor Euler factors

We split the prime divisors of N at the transparent cutoff ⌈log N⌉₊. Mertens' product theorem controls the small primes, while the elementary estimate log (1 + 1 / p) ≤ 1 / p and the radical of N control the large primes.

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPrimeDivisorCutoff (N : ℕ) : ℕ

The natural cutoff used to split the prime divisors of N.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPrimeDivisorCutoff N = ⌈Real.log ↑N⌉₊

theorem MathlibNt.SieveTheory.LiuWeight.exists_liuPrimeDivisorProduct_le_log_log : ∃ (C_L : ℝ), 0 < C_L ∧ ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → liuPrimeDivisorProduct N ≤ C_L * (1 + Real.log (Real.log ↑N))

Liu's finite prime-divisor Euler product has at most log-log growth. The constants and threshold are independent of N.

theorem MathlibNt.SieveTheory.LiuWeight.exists_liuPrimeDivisorLogSum_le_log_log_sq : ∃ (C_D : ℝ), 0 < C_D ∧ ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → liuPrimeDivisorLogSum N ≤ C_D * (1 + Real.log (Real.log ↑N) ^ 2)

The logarithmic prime-divisor moment has at most squared log-log growth.

theorem MathlibNt.SieveTheory.LiuWeight.exists_liuSelbergEulerErrorNumerator_le_log_log_pow : ∃ (C : ℝ), 0 < C ∧ ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → Even N → (2 * liuSelbergAbsoluteLogMoment N + liuSelbergAbsoluteMass N) * SingularSeries.liuSingularSeries N ≤ C * (1 + Real.log (Real.log ↑N)) ^ 6

Along even integers, the numerator in the uniform Selberg Euler error is bounded by a fixed sixth power of 1 + log log N.

theorem MathlibNt.SieveTheory.LiuWeight.tendsto_liuSelbergEulerError_even : Filter.Tendsto (fun (N : ℕ) => (2 * liuSelbergAbsoluteLogMoment N + liuSelbergAbsoluteMass N) * SingularSeries.liuSingularSeries N / Real.log ↑N) (Filter.atTop ⊓ Filter.principal {N : ℕ | Even N}) (nhds 0)

The uniform Selberg Euler error tends to zero as N tends to infinity through the even integers.