Harmonic remainder in Liu's Selberg denominator

This file isolates the elementary harmonic error in the exact denominator convolution. All estimates are pointwise in the fixed even integer N.

theorem MathlibNt.SieveTheory.LiuWeight.liuHarmonic_eq_harmonic (m : ℕ) : liuHarmonic m = ↑(harmonic m)

theorem MathlibNt.SieveTheory.LiuWeight.log_add_one_le_liuHarmonic (m : ℕ) : Real.log (↑m + 1) ≤ liuHarmonic m

theorem MathlibNt.SieveTheory.LiuWeight.liuHarmonic_le_one_add_log (m : ℕ) : liuHarmonic m ≤ 1 + Real.log ↑m

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

The error left after replacing H_{⌊x/d⌋} by log x - log d.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuHarmonicResidual x d = MathlibNt.SieveTheory.LiuWeight.liuHarmonic (x / d) - (Real.log ↑x - Real.log ↑d)

theorem MathlibNt.SieveTheory.LiuWeight.liuHarmonicResidual_nonneg_le_one {x d : ℕ} (hd : d ∈ Finset.Icc 1 x) : 0 ≤ liuHarmonicResidual x d ∧ liuHarmonicResidual x d ≤ 1

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuSelbergCorrectionTail (N x : ℕ) : ℕ → ℝ

The signed correction tail beyond x, written as an actual indicator family.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuSelbergCorrectionTail N x = {d : ℕ | x < d}.indicator fun (d : ℕ) => (MathlibNt.SieveTheory.LiuWeight.liuSelbergCorrection N) d

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuSelbergCorrectionAbsTail (N x : ℕ) : ℕ → ℝ

The absolute correction tail beyond x, written as an actual indicator family.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuSelbergCorrectionAbsTail N x = {d : ℕ | x < d}.indicator fun (d : ℕ) => |(MathlibNt.SieveTheory.LiuWeight.liuSelbergCorrection N) d|

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

theorem MathlibNt.SieveTheory.LiuWeight.summable_liuSelbergCorrectionTail {N x : ℕ} (hNeven : Even N) (hN : 0 < N) : Summable (liuSelbergCorrectionTail N x)

theorem MathlibNt.SieveTheory.LiuWeight.summable_liuSelbergCorrectionAbsTail {N x : ℕ} (hNeven : Even N) (hN : 0 < N) : Summable (liuSelbergCorrectionAbsTail N x)

theorem MathlibNt.SieveTheory.LiuWeight.liuSelbergCorrection_sum_Icc_add_tail {N x : ℕ} (hNeven : Even N) (hN : 0 < N) : ∑ d ∈ Finset.Icc 1 x, (liuSelbergCorrection N) d + ∑' (d : ℕ), liuSelbergCorrectionTail N x d = ∑' (d : ℕ), (liuSelbergCorrection N) d

theorem MathlibNt.SieveTheory.LiuWeight.liuSelbergArithmetic_sum_Icc_eq_log_main_add_remainders {N x : ℕ} (hNeven : Even N) (hN : 0 < N) : ∑ n ∈ Finset.Icc 1 x, liuSelbergArithmetic N n = Real.log ↑x * ∑' (d : ℕ), (liuSelbergCorrection N) d - Real.log ↑x * ∑' (d : ℕ), liuSelbergCorrectionTail N x d - ∑ d ∈ Finset.Icc 1 x, (liuSelbergCorrection N) d * Real.log ↑d + ∑ d ∈ Finset.Icc 1 x, (liuSelbergCorrection N) d * liuHarmonicResidual x d

Exact separation of the logarithmic main term, the signed correction tail, the logarithmic moment, and the elementary harmonic residual.

theorem MathlibNt.SieveTheory.LiuWeight.abs_liuSelbergArithmetic_sum_Icc_sub_log_main_le {N x : ℕ} (hNeven : Even N) (hN : 0 < N) (_hx : 1 ≤ x) : |∑ n ∈ Finset.Icc 1 x, liuSelbergArithmetic N n - Real.log ↑x / (2 * SingularSeries.liuSingularSeries N)| ≤ Real.log ↑x * ∑' (d : ℕ), liuSelbergCorrectionAbsTail N x d + ∑' (d : ℕ), |(liuSelbergCorrection N) d| * Real.log ↑d + ∑' (d : ℕ), |(liuSelbergCorrection N) d|

A transparent fixed-N reduction of the finite Selberg denominator to three explicit absolutely summable errors. No uniformity in N is asserted.