Arithmetic convolution for Liu's Selberg denominator

This file isolates the exact multiplicative arithmetic underlying the finite Selberg denominator.

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

The squarefree source arithmetic factor, extended by zero at zero and away from the source primes.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuSelbergArithmetic N n = if n = 0 then 0 else if Squarefree n ∧ n.Coprime N then ∏ p ∈ n.primeFactors, (↑p - 2)⁻¹ else 0

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuSelbergArithmetic_zero (N : ℕ) : liuSelbergArithmetic N 0 = 0

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuSelbergArithmetic_one (N : ℕ) : liuSelbergArithmetic N 1 = 1

theorem MathlibNt.SieveTheory.LiuWeight.liuSelbergArithmetic_eq_zero_of_not_squarefree_or_not_coprime {N n : ℕ} (h : ¬(Squarefree n ∧ n.Coprime N)) : liuSelbergArithmetic N n = 0

theorem MathlibNt.SieveTheory.LiuWeight.liuSelbergArithmetic_eq_prod {N n : ℕ} (hn : n ≠ 0) (hs : Squarefree n) (hc : n.Coprime N) : liuSelbergArithmetic N n = ∏ p ∈ n.primeFactors, (↑p - 2)⁻¹

theorem MathlibNt.SieveTheory.LiuWeight.dvd_liuPaperQModulus_iff_squarefree_coprime {ε : ℝ} {N n : ℕ} (hn : n ≤ paperQSourceCutoff N ε) : n ∣ liuPaperQModulus N ε ↔ Squarefree n ∧ n.Coprime N

A divisor of Liu's squarefree source modulus is exactly a squarefree integer coprime to N (with the cutoff made explicit for the reverse direction).

theorem MathlibNt.SieveTheory.LiuWeight.liuSelbergDenominator_eq_sum_Icc {N : ℕ} {epsilon : ℝ} (_hNeven : Even N) (_hR : 1 ≤ paperQSourceCutoff N epsilon) : liuSelbergDenominator N epsilon = ∑ n ∈ Finset.Icc 1 (paperQSourceCutoff N epsilon), liuSelbergArithmetic N n

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuReciprocal : ArithmeticFunction ℝ

Equations

• MathlibNt.SieveTheory.LiuWeight.liuReciprocal = { toFun := fun (n : ℕ) => if n = 0 then 0 else (↑n)⁻¹, map_zero' := MathlibNt.SieveTheory.LiuWeight.liuReciprocal._proof_1 }

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuReciprocal_apply (n : ℕ) : liuReciprocal n = if n = 0 then 0 else (↑n)⁻¹

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

Equations

• MathlibNt.SieveTheory.LiuWeight.liuSelbergArithmeticFunction N = { toFun := MathlibNt.SieveTheory.LiuWeight.liuSelbergArithmetic N, map_zero' := ⋯ }

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuSelbergArithmeticFunction_apply (N n : ℕ) : (liuSelbergArithmeticFunction N) n = liuSelbergArithmetic N n

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuMoebiusReciprocal : ArithmeticFunction ℝ

Equations

• MathlibNt.SieveTheory.LiuWeight.liuMoebiusReciprocal = { toFun := fun (n : ℕ) => if n = 0 then 0 else ↑(ArithmeticFunction.moebius n) / ↑n, map_zero' := MathlibNt.SieveTheory.LiuWeight.liuMoebiusReciprocal._proof_1 }

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

Equations

• MathlibNt.SieveTheory.LiuWeight.liuSelbergCorrection N = MathlibNt.SieveTheory.LiuWeight.liuMoebiusReciprocal * MathlibNt.SieveTheory.LiuWeight.liuSelbergArithmeticFunction N

theorem MathlibNt.SieveTheory.LiuWeight.liuSelbergCorrection_apply (N n : ℕ) : (liuSelbergCorrection N) n = ∑ d ∈ n.divisors, liuMoebiusReciprocal (n / d) * (liuSelbergArithmeticFunction N) d

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuReciprocal_zero : liuReciprocal 0 = 0

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuMoebiusReciprocal_zero : liuMoebiusReciprocal 0 = 0

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuSelbergCorrection_zero (N : ℕ) : (liuSelbergCorrection N) 0 = 0

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuSelbergCorrection_one (N : ℕ) : (liuSelbergCorrection N) 1 = 1

theorem MathlibNt.SieveTheory.LiuWeight.liuSelbergArithmeticFunction_isMultiplicative (N : ℕ) : (liuSelbergArithmeticFunction N).IsMultiplicative

theorem MathlibNt.SieveTheory.LiuWeight.liuReciprocal_isMultiplicative : liuReciprocal.IsMultiplicative

theorem MathlibNt.SieveTheory.LiuWeight.liuMoebiusReciprocal_isMultiplicative : liuMoebiusReciprocal.IsMultiplicative

theorem MathlibNt.SieveTheory.LiuWeight.liuSelbergCorrection_isMultiplicative (N : ℕ) : (liuSelbergCorrection N).IsMultiplicative

theorem MathlibNt.SieveTheory.LiuWeight.liuReciprocal_mul_liuMoebiusReciprocal : liuReciprocal * liuMoebiusReciprocal = 1

theorem MathlibNt.SieveTheory.LiuWeight.liuSelbergArithmeticFunction_eq_convolution (N : ℕ) : liuSelbergArithmeticFunction N = liuReciprocal * liuSelbergCorrection N

theorem MathlibNt.SieveTheory.LiuWeight.liuSelbergArithmetic_eq_convolution (N n : ℕ) : liuSelbergArithmetic N n = (liuReciprocal * liuSelbergCorrection N) n

theorem MathlibNt.SieveTheory.LiuWeight.liuSelbergCorrection_prime_pow_sum {N p k : ℕ} (hp : Nat.Prime p) : (liuSelbergCorrection N) (p ^ k) = ∑ j ∈ Finset.range (k + 1), liuMoebiusReciprocal (p ^ (k - j)) * (liuSelbergArithmeticFunction N) (p ^ j)

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuMoebiusReciprocal_one : liuMoebiusReciprocal 1 = 1

theorem MathlibNt.SieveTheory.LiuWeight.liuSelbergCorrection_prime_of_not_dvd {N p : ℕ} (hNeven : Even N) (hp : Nat.Prime p) (hpn : ¬p ∣ N) : (liuSelbergCorrection N) p = 2 / (↑p * (↑p - 2))

theorem MathlibNt.SieveTheory.LiuWeight.liuSelbergCorrection_prime_sq_of_not_dvd {N p : ℕ} (hp : Nat.Prime p) (hpn : ¬p ∣ N) : (liuSelbergCorrection N) (p ^ 2) = -1 / (↑p * (↑p - 2))

theorem MathlibNt.SieveTheory.LiuWeight.liuSelbergCorrection_prime_pow_eq_zero_of_not_dvd {N p k : ℕ} (hp : Nat.Prime p) (_hpn : ¬p ∣ N) (hk : 3 ≤ k) : (liuSelbergCorrection N) (p ^ k) = 0

theorem MathlibNt.SieveTheory.LiuWeight.liuSelbergCorrection_prime_of_dvd {N p : ℕ} (hp : Nat.Prime p) (hpn : p ∣ N) : (liuSelbergCorrection N) p = -(↑p)⁻¹

theorem MathlibNt.SieveTheory.LiuWeight.liuSelbergCorrection_prime_pow_eq_zero_of_dvd {N p k : ℕ} (hp : Nat.Prime p) (hpn : p ∣ N) (hk : 2 ≤ k) : (liuSelbergCorrection N) (p ^ k) = 0

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuHarmonic (x : ℕ) : ℝ

The finite harmonic sum, with the empty sum giving its value at zero.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuHarmonic x = ∑ m ∈ Finset.Icc 1 x, (↑m)⁻¹

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuHarmonic_zero : liuHarmonic 0 = 0

theorem MathlibNt.SieveTheory.LiuWeight.liuReciprocal_sum_Ioc (x : ℕ) : ∑ m ∈ Finset.Ioc 0 x, liuReciprocal m = liuHarmonic x

theorem MathlibNt.SieveTheory.LiuWeight.liuSelbergArithmetic_sum_Icc (N x : ℕ) : ∑ n ∈ Finset.Icc 1 x, liuSelbergArithmetic N n = ∑ d ∈ Finset.Icc 1 x, (liuSelbergCorrection N) d * liuHarmonic (x / d)