Documentation

MathlibNt.SieveTheory.Selberg.Liu.LiuSelbergDenominatorHarmonic

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.

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

MathlibNt.SieveTheory.LiuWeight.liuHarmonic_eq_harmonic · compiled type and proof/definition references.

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

MathlibNt.SieveTheory.LiuWeight.log_add_one_le_liuHarmonic · compiled type and proof/definition references.

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

MathlibNt.SieveTheory.LiuWeight.liuHarmonic_le_one_add_log · compiled type and proof/definition references.

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

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

Equations
Instances For
    Inspect dependencies

    MathlibNt.SieveTheory.LiuWeight.liuHarmonicResidual · compiled type and proof/definition references.

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

    MathlibNt.SieveTheory.LiuWeight.liuHarmonicResidual_nonneg_le_one · compiled type and proof/definition references.

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

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

    Equations
    Instances For
      Inspect dependencies

      MathlibNt.SieveTheory.LiuWeight.liuSelbergCorrectionTail · compiled type and proof/definition references.

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

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

      Equations
      Instances For
        Inspect dependencies

        MathlibNt.SieveTheory.LiuWeight.liuSelbergCorrectionAbsTail · compiled type and proof/definition references.

        source
        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
        Inspect dependencies

        MathlibNt.SieveTheory.LiuWeight.summable_abs_liuSelbergCorrection_mul_log_nat · compiled type and proof/definition references.

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

        MathlibNt.SieveTheory.LiuWeight.summable_liuSelbergCorrectionTail · compiled type and proof/definition references.

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

        MathlibNt.SieveTheory.LiuWeight.summable_liuSelbergCorrectionAbsTail · compiled type and proof/definition references.

        source
        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
        Inspect dependencies

        MathlibNt.SieveTheory.LiuWeight.liuSelbergCorrection_sum_Icc_add_tail · compiled type and proof/definition references.

        source
        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.

        Inspect dependencies

        MathlibNt.SieveTheory.LiuWeight.liuSelbergArithmetic_sum_Icc_eq_log_main_add_remainders · compiled type and proof/definition references.

        source
        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.

        Inspect dependencies

        MathlibNt.SieveTheory.LiuWeight.abs_liuSelbergArithmetic_sum_Icc_sub_log_main_le · compiled type and proof/definition references.