Uniform Euler controls for Liu's Selberg correction

The finite factors below isolate the dependence on the prime divisors of the even integer N; the infinite factor is fixed once and for all at N = 2.

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPrimeDivisorProduct (N : ℕ) : ℝ

The finite Euler factor which records the prime divisors of N.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPrimeDivisorProduct N = ∏ p ∈ N.primeFactors, (1 + (↑p)⁻¹)

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuUniversalAbsEulerFactor (p : Nat.Primes) : ℝ

The absolute local Euler factor at the fixed even integer 2.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuUniversalAbsEulerFactor p = 1 + MathlibNt.SieveTheory.LiuWeight.liuSelbergAbsPrimeDeviation 2 p

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuUniversalAbsEuler : ℝ

The universal absolute Euler product, independent of N.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuUniversalAbsEuler = ∏' (p : Nat.Primes), MathlibNt.SieveTheory.LiuWeight.liuUniversalAbsEulerFactor p

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuUniversalAbsLogMoment : ℝ

A fixed logarithmic absolute moment. It is independent of the variable integer N in the uniform estimates below.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuUniversalAbsLogMoment = ∑' (d : ℕ), |(MathlibNt.SieveTheory.LiuWeight.liuSelbergCorrection 2) d| * Real.log ↑d

theorem MathlibNt.SieveTheory.LiuWeight.summable_liuUniversalAbsEulerDeviation : Summable (liuSelbergAbsPrimeDeviation 2)

theorem MathlibNt.SieveTheory.LiuWeight.liuSelbergAbsPrimeDeviation_two_nonneg (p : Nat.Primes) : 0 ≤ liuSelbergAbsPrimeDeviation 2 p

theorem MathlibNt.SieveTheory.LiuWeight.liuUniversalAbsEulerFactor_nonneg (p : Nat.Primes) : 0 ≤ liuUniversalAbsEulerFactor p

theorem MathlibNt.SieveTheory.LiuWeight.liuUniversalAbsEulerFactor_pos (p : Nat.Primes) : 0 < liuUniversalAbsEulerFactor p

theorem MathlibNt.SieveTheory.LiuWeight.multipliable_liuUniversalAbsEulerFactor : Multipliable liuUniversalAbsEulerFactor

theorem MathlibNt.SieveTheory.LiuWeight.liuUniversalAbsEuler_nonneg : 0 ≤ liuUniversalAbsEuler

theorem MathlibNt.SieveTheory.LiuWeight.liuUniversalAbsEuler_ne_zero : liuUniversalAbsEuler ≠ 0

theorem MathlibNt.SieveTheory.LiuWeight.liuUniversalAbsEuler_pos : 0 < liuUniversalAbsEuler

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

Equations

• MathlibNt.SieveTheory.LiuWeight.liuAbsoluteEulerFactor N p = 1 + MathlibNt.SieveTheory.LiuWeight.liuSelbergAbsPrimeDeviation N p

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

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPrimeDivisorKernel N p = if ↑p ∣ N then 1 + (↑↑p)⁻¹ else 1

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

theorem MathlibNt.SieveTheory.LiuWeight.liuAbsoluteEulerFactor_one_le {N : ℕ} (hNeven : Even N) (p : Nat.Primes) : 1 ≤ liuAbsoluteEulerFactor N p

theorem MathlibNt.SieveTheory.LiuWeight.multipliable_liuAbsoluteEulerFactor {N : ℕ} (hNeven : Even N) (hN : 0 < N) : Multipliable (liuAbsoluteEulerFactor N)

theorem MathlibNt.SieveTheory.LiuWeight.liuAbsoluteEulerFactor_le_universal_mul_kernel {N : ℕ} (hNeven : Even N) (p : Nat.Primes) : liuAbsoluteEulerFactor N p ≤ liuUniversalAbsEulerFactor p * liuPrimeDivisorKernel N p

theorem MathlibNt.SieveTheory.LiuWeight.hasProd_liuPrimeDivisorKernel {N : ℕ} (hN : 0 < N) : HasProd (liuPrimeDivisorKernel N) (liuPrimeDivisorProduct N)

theorem MathlibNt.SieveTheory.LiuWeight.tprod_universal_mul_liuPrimeDivisorKernel {N : ℕ} (hN : 0 < N) : ∏' (p : Nat.Primes), liuUniversalAbsEulerFactor p * liuPrimeDivisorKernel N p = liuUniversalAbsEuler * liuPrimeDivisorProduct N

theorem MathlibNt.SieveTheory.LiuWeight.tprod_liuAbsoluteEulerFactor_le_uniform {N : ℕ} (hNeven : Even N) (hN : 0 < N) : ∏' (p : Nat.Primes), liuAbsoluteEulerFactor N p ≤ liuUniversalAbsEuler * liuPrimeDivisorProduct N

theorem MathlibNt.SieveTheory.LiuWeight.tsum_abs_liuSelbergCorrection_le_tprod_liuAbsoluteEulerFactor {N : ℕ} (hNeven : Even N) (hN : 0 < N) : ∑' (d : ℕ), |(liuSelbergCorrection N) d| ≤ ∏' (p : Nat.Primes), liuAbsoluteEulerFactor N p

theorem MathlibNt.SieveTheory.LiuWeight.tsum_abs_liuSelbergCorrection_le_uniform {N : ℕ} (hNeven : Even N) (hN : 0 < N) : ∑' (d : ℕ), |(liuSelbergCorrection N) d| ≤ liuUniversalAbsEuler * liuPrimeDivisorProduct N

theorem MathlibNt.SieveTheory.LiuWeight.summable_liuUniversalAbsLogMoment : Summable fun (d : ℕ) => |(liuSelbergCorrection 2) d| * Real.log ↑d

theorem MathlibNt.SieveTheory.LiuWeight.liuUniversalAbsLogMoment_nonneg : 0 ≤ liuUniversalAbsLogMoment

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuUniversalAbsLogRatio : ℝ

The normalized universal logarithmic moment.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuUniversalAbsLogRatio = MathlibNt.SieveTheory.LiuWeight.liuUniversalAbsLogMoment / MathlibNt.SieveTheory.LiuWeight.liuUniversalAbsEuler

theorem MathlibNt.SieveTheory.LiuWeight.liuUniversalAbsLogRatio_nonneg : 0 ≤ liuUniversalAbsLogRatio

theorem MathlibNt.SieveTheory.LiuWeight.liuPrimeDivisorProduct_pos (N : ℕ) : 0 < liuPrimeDivisorProduct N

theorem MathlibNt.SieveTheory.LiuWeight.one_add_liuBaseDeviation_le_one (p : ℕ) : 1 + SingularSeries.liuBaseDeviation p ≤ 1

theorem MathlibNt.SieveTheory.LiuWeight.liuUniversalProduct_le_one : SingularSeries.liuUniversalProduct ≤ 1

theorem MathlibNt.SieveTheory.LiuWeight.liuCorrectionFactor_le_primeCube {p : ℕ} (hp : 2 < p) : SingularSeries.liuCorrectionFactor p ≤ (1 + (↑p)⁻¹) ^ 3

theorem MathlibNt.SieveTheory.LiuWeight.liuCorrection_le_liuPrimeDivisorProduct_cube (N : ℕ) : SingularSeries.liuCorrection N ≤ liuPrimeDivisorProduct N ^ 3

theorem MathlibNt.SieveTheory.LiuWeight.liuSingularSeries_le_liuPrimeDivisorProduct_cube (N : ℕ) : SingularSeries.liuSingularSeries N ≤ liuPrimeDivisorProduct N ^ 3

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPrimeDivisorLogSum (N : ℕ) : ℝ

The logarithmic first moment of the finite prime-divisor kernel.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPrimeDivisorLogSum N = ∑ p ∈ N.primeFactors, Real.log ↑p / ↑p

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuSquarefreeDivisorKernel (N d : ℕ) : ℝ

The squarefree kernel supported on divisors of N. At a prime divisor of N its local coefficient is 1 / p.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuSquarefreeDivisorKernel N d = if d ∈ N.divisors ∧ Squarefree d then (↑d)⁻¹ else 0

theorem MathlibNt.SieveTheory.LiuWeight.summable_liuSquarefreeDivisorKernel {N : ℕ} (hN : 0 < N) : Summable (liuSquarefreeDivisorKernel N)

theorem MathlibNt.SieveTheory.LiuWeight.summable_liuSquarefreeDivisorKernel_mul_log {N : ℕ} (hN : 0 < N) : Summable fun (d : ℕ) => liuSquarefreeDivisorKernel N d * Real.log ↑d

theorem MathlibNt.SieveTheory.LiuWeight.tsum_liuSquarefreeDivisorKernel {N : ℕ} (hN : 0 < N) : ∑' (d : ℕ), liuSquarefreeDivisorKernel N d = liuPrimeDivisorProduct N

theorem MathlibNt.SieveTheory.LiuWeight.liuSquarefreeDivisorKernel_nonneg (N d : ℕ) : 0 ≤ liuSquarefreeDivisorKernel N d

theorem MathlibNt.SieveTheory.LiuWeight.liuPrimeDivisorLogSum_nonneg (N : ℕ) : 0 ≤ liuPrimeDivisorLogSum N

theorem MathlibNt.SieveTheory.LiuWeight.tsum_liuSquarefreeDivisorKernel_mul_log_le {N : ℕ} (hN : 0 < N) : ∑' (d : ℕ), liuSquarefreeDivisorKernel N d * Real.log ↑d ≤ liuPrimeDivisorProduct N * liuPrimeDivisorLogSum N

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuSelbergCorrectionAbsFunction (N : ℕ) : ArithmeticFunction ℝ

The absolute Selberg correction as an arithmetic function.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuSelbergCorrectionAbsFunction N = { toFun := fun (n : ℕ) => |(MathlibNt.SieveTheory.LiuWeight.liuSelbergCorrection N) n|, map_zero' := ⋯ }

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuSelbergCorrectionAbsFunction_apply (N n : ℕ) : (liuSelbergCorrectionAbsFunction N) n = |(liuSelbergCorrection N) n|

theorem MathlibNt.SieveTheory.LiuWeight.liuSelbergCorrectionAbsFunction_isMultiplicative (N : ℕ) : (liuSelbergCorrectionAbsFunction N).IsMultiplicative

theorem MathlibNt.SieveTheory.LiuWeight.tsum_abs_liuSelbergCorrection_two_eq_liuUniversalAbsEuler : ∑' (d : ℕ), |(liuSelbergCorrection 2) d| = liuUniversalAbsEuler

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuSquarefreeDivisorKernelFunction (N : ℕ) : ArithmeticFunction ℝ

The finite squarefree divisor kernel as an arithmetic function.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuSquarefreeDivisorKernelFunction N = { toFun := MathlibNt.SieveTheory.LiuWeight.liuSquarefreeDivisorKernel N, map_zero' := ⋯ }

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuSquarefreeDivisorKernelFunction_apply (N n : ℕ) : (liuSquarefreeDivisorKernelFunction N) n = liuSquarefreeDivisorKernel N n

theorem MathlibNt.SieveTheory.LiuWeight.liuSquarefreeDivisorKernelFunction_isMultiplicative {N : ℕ} (hN : 0 < N) : (liuSquarefreeDivisorKernelFunction N).IsMultiplicative

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuSelbergAbsKernelConvolution (N : ℕ) : ArithmeticFunction ℝ

The universal absolute correction convolved with the finite divisor kernel.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuSelbergAbsKernelConvolution N = MathlibNt.SieveTheory.LiuWeight.liuSelbergCorrectionAbsFunction 2 * MathlibNt.SieveTheory.LiuWeight.liuSquarefreeDivisorKernelFunction N

theorem MathlibNt.SieveTheory.LiuWeight.liuSelbergAbsKernelConvolution_isMultiplicative {N : ℕ} (hN : 0 < N) : (liuSelbergAbsKernelConvolution N).IsMultiplicative

theorem MathlibNt.SieveTheory.LiuWeight.liuSelbergAbsKernelConvolution_nonneg (N n : ℕ) : 0 ≤ (liuSelbergAbsKernelConvolution N) n

theorem MathlibNt.SieveTheory.LiuWeight.liuSelbergCorrectionAbsFunction_two_le_convolution {N n : ℕ} (hN : 0 < N) : (liuSelbergCorrectionAbsFunction 2) n ≤ (liuSelbergAbsKernelConvolution N) n

theorem MathlibNt.SieveTheory.LiuWeight.liuSquarefreeDivisorKernelFunction_le_convolution {N n : ℕ} (_hN : 0 < N) : (liuSquarefreeDivisorKernelFunction N) n ≤ (liuSelbergAbsKernelConvolution N) n

theorem MathlibNt.SieveTheory.LiuWeight.abs_liuSelbergCorrection_prime_pow_eq_two_of_not_dvd {N p e : ℕ} (hNeven : Even N) (hp : Nat.Prime p) (hpn : ¬p ∣ N) : |(liuSelbergCorrection N) (p ^ e)| = |(liuSelbergCorrection 2) (p ^ e)|

theorem MathlibNt.SieveTheory.LiuWeight.liuSelbergCorrectionAbsFunction_prime_pow_le_convolution {N p e : ℕ} (hNeven : Even N) (hN : 0 < N) (hp : Nat.Prime p) : (liuSelbergCorrectionAbsFunction N) (p ^ e) ≤ (liuSelbergAbsKernelConvolution N) (p ^ e)

theorem MathlibNt.SieveTheory.LiuWeight.liuSelbergCorrectionAbsFunction_le_convolution {N : ℕ} (hNeven : Even N) (hN : 0 < N) (n : ℕ) : (liuSelbergCorrectionAbsFunction N) n ≤ (liuSelbergAbsKernelConvolution N) n

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuSelbergAbsoluteLogMoment (N : ℕ) : ℝ

The nonnegative logarithmic moment in the exact denominator correction.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuSelbergAbsoluteLogMoment N = ∑' (d : ℕ), |(MathlibNt.SieveTheory.LiuWeight.liuSelbergCorrection N) d| * Real.log ↑d

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuSelbergAbsoluteMass (N : ℕ) : ℝ

The nonnegative absolute mass in the exact denominator correction.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuSelbergAbsoluteMass N = ∑' (d : ℕ), |(MathlibNt.SieveTheory.LiuWeight.liuSelbergCorrection N) d|

theorem MathlibNt.SieveTheory.LiuWeight.tsum_liuSelbergAbsKernelConvolution_mul_log {N : ℕ} (hN : 0 < N) : ∑' (n : ℕ), (liuSelbergAbsKernelConvolution N) n * Real.log ↑n = liuUniversalAbsLogMoment * liuPrimeDivisorProduct N + (∑' (n : ℕ), |(liuSelbergCorrection 2) n|) * ∑' (n : ℕ), liuSquarefreeDivisorKernel N n * Real.log ↑n

theorem MathlibNt.SieveTheory.LiuWeight.liuSelbergAbsoluteLogMoment_le_uniform {N : ℕ} (hNeven : Even N) (hN : 0 < N) : liuSelbergAbsoluteLogMoment N ≤ liuPrimeDivisorProduct N * (liuUniversalAbsLogMoment + liuUniversalAbsEuler * liuPrimeDivisorLogSum N)

theorem MathlibNt.SieveTheory.LiuWeight.liuSelbergAbsoluteLogMoment_le_uniform_normalized {N : ℕ} (hNeven : Even N) (hN : 0 < N) : liuSelbergAbsoluteLogMoment N ≤ liuUniversalAbsEuler * liuPrimeDivisorProduct N * (liuUniversalAbsLogRatio + liuPrimeDivisorLogSum N)

theorem MathlibNt.SieveTheory.LiuWeight.liuSelbergCorrectionAbsTail_markov {N x : ℕ} (hNeven : Even N) (hN : 0 < N) (hx : 2 ≤ x) : Real.log ↑x * ∑' (d : ℕ), liuSelbergCorrectionAbsTail N x d ≤ liuSelbergAbsoluteLogMoment N

theorem MathlibNt.SieveTheory.LiuWeight.abs_liuSelbergArithmetic_sum_Icc_sub_log_main_le_uniform_reduction {N x : ℕ} (hNeven : Even N) (hN : 0 < N) (hx : 2 ≤ x) : |∑ n ∈ Finset.Icc 1 x, liuSelbergArithmetic N n - Real.log ↑x / (2 * SingularSeries.liuSingularSeries N)| ≤ 2 * liuSelbergAbsoluteLogMoment N + liuSelbergAbsoluteMass N