Euler total of Liu's Selberg correction

This file proves absolute summability of the correction in the exact denominator convolution and identifies its signed Euler total.

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuSelbergAbsPrimeDeviation (N : ℕ) (p : Nat.Primes) : ℝ

Equations

• MathlibNt.SieveTheory.LiuWeight.liuSelbergAbsPrimeDeviation N p = ∑' (e : ℕ), |(MathlibNt.SieveTheory.LiuWeight.liuSelbergCorrection N) (↑p ^ e)| - 1

theorem MathlibNt.SieveTheory.LiuWeight.summable_abs_liuSelbergCorrection_prime_pow (N : ℕ) {p : ℕ} (hp : Nat.Prime p) : Summable fun (e : ℕ) => |(liuSelbergCorrection N) (p ^ e)|

theorem MathlibNt.SieveTheory.LiuWeight.tsum_abs_liuSelbergCorrection_prime_pow {N p : ℕ} (hNeven : Even N) (hp : Nat.Prime p) : ∑' (e : ℕ), |(liuSelbergCorrection N) (p ^ e)| = if p ∣ N then 1 + (↑p)⁻¹ else 1 + 3 / (↑p * (↑p - 2))

theorem MathlibNt.SieveTheory.LiuWeight.tsum_liuSelbergCorrection_prime_pow_eq_localFactor_inv {N p : ℕ} (hNeven : Even N) (hp : Nat.Prime p) : ∑' (e : ℕ), (liuSelbergCorrection N) (p ^ e) = (SingularSeries.localFactor p N)⁻¹

theorem MathlibNt.SieveTheory.LiuWeight.liuSelbergAbsPrimeDeviation_nonneg_core {N : ℕ} (hNeven : Even N) (p : Nat.Primes) : 0 ≤ liuSelbergAbsPrimeDeviation N p

The absolute local Euler total contains the unit term.

theorem MathlibNt.SieveTheory.LiuWeight.summable_liuSelbergAbsPrimeDeviation {N : ℕ} (hNeven : Even N) (hN : 0 < N) : Summable (liuSelbergAbsPrimeDeviation N)

theorem MathlibNt.SieveTheory.LiuWeight.summable_norm_liuSelbergCorrection {N : ℕ} (hNeven : Even N) (hN : 0 < N) : Summable fun (d : ℕ) => ‖(liuSelbergCorrection N) d‖

theorem MathlibNt.SieveTheory.LiuWeight.summable_abs_liuSelbergCorrection {N : ℕ} (hNeven : Even N) (hN : 0 < N) : Summable fun (d : ℕ) => |(liuSelbergCorrection N) d|

theorem MathlibNt.SieveTheory.LiuWeight.summable_abs_liuSelbergCorrection_mul_log {N : ℕ} (hNeven : Even N) (hN : 0 < N) : Summable fun (d : ℕ) => |(liuSelbergCorrection N) d| * Real.log (2 * ↑d)

theorem MathlibNt.SieveTheory.LiuWeight.liuSelbergCorrection_finiteEulerProduct {N z : ℕ} (hNeven : Even N) (hz : 2 ≤ z) : ∏ p ∈ (z + 1).primesBelow, ∑' (e : ℕ), (liuSelbergCorrection N) (p ^ e) = 1 / (2 * SingularSeries.liuSingularSeriesTruncated N z)

theorem MathlibNt.SieveTheory.LiuWeight.tsum_liuSelbergCorrection {N : ℕ} (hNeven : Even N) (hN : 0 < N) : ∑' (d : ℕ), (liuSelbergCorrection N) d = 1 / (2 * SingularSeries.liuSingularSeries N)

theorem MathlibNt.SieveTheory.LiuWeight.tendsto_liuSelbergCorrection_partialSums {N : ℕ} (hNeven : Even N) (hN : 0 < N) : Filter.Tendsto (fun (x : ℕ) => ∑ d ∈ Finset.Icc 1 x, (liuSelbergCorrection N) d) Filter.atTop (nhds (1 / (2 * SingularSeries.liuSingularSeries N)))