Liu's genuine logarithmic-integral weight sum

This module reindexes the finite characteristic weight by its unique prime-pair representation and separates Liu's printed reciprocal-log estimate from the comparison between the genuine logarithmic integral and x / log x.

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuWeightMainSum (main : ℝ → ℝ) (N : ℕ) : ℝ

The weighted main-model sum in Liu's factored M₁.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuWeightMainSum main N = ∑ a ∈ Finset.range (N + 1), MathlibNt.SieveTheory.LiuWeight.liuWeight N (MathlibNt.SieveTheory.LiuWeight.liuSourceZ10 N) (MathlibNt.SieveTheory.LiuWeight.liuSourceY3 N) a * main (↑N / ↑a)

theorem MathlibNt.SieveTheory.LiuWeight.liuWeightMainSum_eq_sum_pairs (main : ℝ → ℝ) (N : ℕ) : liuWeightMainSum main N = ∑ p ∈ liuWeightPairs N (liuSourceZ10 N) (liuSourceY3 N), main (↑N / (↑p.1 * ↑p.2))

Exact finite reindexing of Liu's characteristic weight by its unique admissible ordered prime pair.

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

The reciprocal-log sum printed in Liu's lm-mt, with every quotient taken in ℝ.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuSourceReciprocalLogSum N = ∑ p ∈ MathlibNt.SieveTheory.LiuWeight.liuWeightPairs N (MathlibNt.SieveTheory.LiuWeight.liuSourceZ10 N) (MathlibNt.SieveTheory.LiuWeight.liuSourceY3 N), 1 / (↑p.1 * ↑p.2 * Real.log (↑N / (↑p.1 * ↑p.2)))

def MathlibNt.SieveTheory.LiuWeight.LiuSourceReciprocalLogBound (N : ℕ) : Prop

Transparent statement of the source estimate ∑ f(a)/(a log(N/a)) ≤ 0.49254/log N.

Equations

• MathlibNt.SieveTheory.LiuWeight.LiuSourceReciprocalLogBound N = (MathlibNt.SieveTheory.LiuWeight.liuSourceReciprocalLogSum N ≤ 0.49254 / Real.log ↑N)

theorem MathlibNt.SieveTheory.LiuWeight.liuWeightMainSum_div_log_eq (N : ℕ) (hN : 8 ≤ N) : liuWeightMainSum (fun (x : ℝ) => x / Real.log x) N = ↑N * liuSourceReciprocalLogSum N

The x / log x proxy weight sum is exactly N times Liu's reciprocal-log sum.

theorem MathlibNt.SieveTheory.LiuWeight.liuWeightMainSum_div_log_le (N : ℕ) (hN : 8 ≤ N) (hsource : LiuSourceReciprocalLogBound N) : liuWeightMainSum (fun (x : ℝ) => x / Real.log x) N ≤ 0.49254 * ↑N / Real.log ↑N

Liu's reciprocal-log estimate gives the printed proxy main-sum bound without any natural-number division.

def MathlibNt.SieveTheory.LiuWeight.LiuGenuineLiWeightMainSumBound (kappa K : ℝ) (N : ℕ) : Prop

The genuine-logarithmic-integral weighted-sum estimate needed for Liu's M₁.

Equations

• MathlibNt.SieveTheory.LiuWeight.LiuGenuineLiWeightMainSumBound kappa K N = (0 ≤ MathlibNt.SieveTheory.LiuWeight.liuWeightMainSum (MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegral kappa) N ∧ MathlibNt.SieveTheory.LiuWeight.liuWeightMainSum (MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegral kappa) N ≤ K * ↑N / Real.log ↑N)

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

The exact summed correction from replacing the source proxy by the genuine logarithmic integral.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuGenuineLiRemainderSum kappa N = ∑ p ∈ MathlibNt.SieveTheory.LiuWeight.liuWeightPairs N (MathlibNt.SieveTheory.LiuWeight.liuSourceZ10 N) (MathlibNt.SieveTheory.LiuWeight.liuSourceY3 N), MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegralRemainder kappa (↑N / (↑p.1 * ↑p.2))

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuWeightP₁ReciprocalBound : ℝ

A fixed Mertens bound for the first prime coordinate of Liu's pairs.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuWeightP₁ReciprocalBound = Classical.choose MathlibNt.SieveTheory.LiuWeight.liuWeightP₁ReciprocalBound._proof_2

theorem MathlibNt.SieveTheory.LiuWeight.liuWeightP₁ReciprocalBound_spec (N : ℕ) (hN : 2 ≤ N) : |liuSourceR1P₁DivisorReciprocalSum N 0| ≤ liuWeightP₁ReciprocalBound

The chosen constant uniformly bounds the first-coordinate reciprocal mass.

theorem MathlibNt.SieveTheory.LiuWeight.liuSourceR1P₁DivisorReciprocalSum_nonneg (N : ℕ) : 0 ≤ liuSourceR1P₁DivisorReciprocalSum N 0

The first-coordinate reciprocal mass is nonnegative.

theorem MathlibNt.SieveTheory.LiuWeight.liuWeightP₁ReciprocalBound_nonneg : 0 ≤ liuWeightP₁ReciprocalBound

The uniform first-coordinate Mertens bound is nonnegative.

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

The reciprocal mass of the exact Liu pair set.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuWeightPairReciprocalSum N = ∑ p ∈ MathlibNt.SieveTheory.LiuWeight.liuWeightPairs N (MathlibNt.SieveTheory.LiuWeight.liuSourceZ10 N) (MathlibNt.SieveTheory.LiuWeight.liuSourceY3 N), 1 / (↑p.1 * ↑p.2)

theorem MathlibNt.SieveTheory.LiuWeight.liuWeightPairReciprocalSum_le (N : ℕ) (hN : 8 ≤ N) : liuWeightPairReciprocalSum N ≤ liuWeightP₁ReciprocalBound * liuSourceR1P₂ReciprocalBound

The exact pair reciprocal mass is uniformly bounded by the two Mertens constants.

theorem MathlibNt.SieveTheory.LiuWeight.eventually_abs_liuLogarithmicIntegralRemainder_le (kappa : ℝ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ᶠ (x : ℝ) in Filter.atTop, 2 ≤ x → |liuLogarithmicIntegralRemainder kappa x| ≤ C * x / Real.log x ^ 2

The genuine-minus-proxy remainder is eventually bounded by x / log(x)^2. The additive normalization is absorbed using log(x)^2 = o(x).

theorem MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegralRemainder_pair_le (kappa C : ℝ) (hC : 0 ≤ C) (N : ℕ) (hN : 8 ≤ N) (p : ℕ × ℕ) (hp : p ∈ liuWeightPairs N (liuSourceZ10 N) (liuSourceY3 N)) (hpoint : |liuLogarithmicIntegralRemainder kappa (↑N / (↑p.1 * ↑p.2))| ≤ C * (↑N / (↑p.1 * ↑p.2)) / Real.log (↑N / (↑p.1 * ↑p.2)) ^ 2) : |liuLogarithmicIntegralRemainder kappa (↑N / (↑p.1 * ↑p.2))| ≤ 9 * C * ↑N / (↑p.1 * ↑p.2 * Real.log ↑N ^ 2)

The pair logarithm lower bound converts the pointwise remainder estimate to an N / (p₁ p₂ log(N)^2) estimate.

theorem MathlibNt.SieveTheory.LiuWeight.liuGenuineLiRemainderSum_factor (C : ℝ) (N : ℕ) : ∑ p ∈ liuWeightPairs N (liuSourceZ10 N) (liuSourceY3 N), 9 * C * ↑N / (↑p.1 * ↑p.2 * Real.log ↑N ^ 2) = 9 * C * ↑N / Real.log ↑N ^ 2 * liuWeightPairReciprocalSum N

The pointwise pair majorant factors through the exact reciprocal pair mass.

theorem MathlibNt.SieveTheory.LiuWeight.liuWeightMainSum_logarithmicIntegral_eq_proxy_add_remainder (kappa : ℝ) (N : ℕ) : liuWeightMainSum (liuLogarithmicIntegral kappa) N = liuWeightMainSum (fun (x : ℝ) => x / Real.log x) N + liuGenuineLiRemainderSum kappa N

Exact decomposition of the genuine weight sum into the source proxy and its summed logarithmic-integral correction.

def MathlibNt.SieveTheory.LiuWeight.LiuGenuineLiRemainderSumBound (kappa eta : ℝ) (N : ℕ) : Prop

The sole analytic correction estimate needed after exact reindexing.

Equations

• MathlibNt.SieveTheory.LiuWeight.LiuGenuineLiRemainderSumBound kappa eta N = (|MathlibNt.SieveTheory.LiuWeight.liuGenuineLiRemainderSum kappa N| ≤ eta * ↑N / Real.log ↑N)

def MathlibNt.SieveTheory.LiuWeight.LiuGenuineLiRemainderSumIsLittleO (kappa : ℝ) : Prop

Eventual o(N/log N) form of the sole remaining correction estimate.

Equations

• MathlibNt.SieveTheory.LiuWeight.LiuGenuineLiRemainderSumIsLittleO kappa = ∀ (eta : ℝ), 0 < eta → ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → MathlibNt.SieveTheory.LiuWeight.LiuGenuineLiRemainderSumBound kappa eta N

theorem MathlibNt.SieveTheory.LiuWeight.liuGenuineLiRemainderSum_isLittleO (kappa : ℝ) : LiuGenuineLiRemainderSumIsLittleO kappa

The summed genuine-logarithmic-integral correction is o(N / log N).

theorem MathlibNt.SieveTheory.LiuWeight.liuWeightMainSum_logarithmicIntegral_nonneg (kappa : ℝ) (hκ : 0 ≤ kappa) (N : ℕ) (hN : 8 ≤ N) : 0 ≤ liuWeightMainSum (liuLogarithmicIntegral kappa) N

Under kappa ≥ 0, every summand in the genuine weight sum is nonnegative.

theorem MathlibNt.SieveTheory.LiuWeight.liuGenuineLiWeightMainSumBound_of_source_of_remainder (kappa eta : ℝ) (hκ : 0 ≤ kappa) (_heta : 0 < eta) (N : ℕ) (hN : 8 ≤ N) (hsource : LiuSourceReciprocalLogBound N) (hremainder : LiuGenuineLiRemainderSumBound kappa eta N) : LiuGenuineLiWeightMainSumBound kappa (0.49254 + eta) N

The source 0.49254 estimate and one precise remainder-sum bound imply the genuine logarithmic-integral estimate.

theorem MathlibNt.SieveTheory.LiuWeight.eventually_liuGenuineLiWeightMainSumBound_of_source (kappa : ℝ) (hκ : 0 ≤ kappa) (eta : ℝ) : 0 < eta → ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → LiuSourceReciprocalLogBound N → LiuGenuineLiWeightMainSumBound kappa (0.49254 + eta) N

For a nonnegative normalization, Liu's printed reciprocal-log estimate eventually implies the genuine logarithmic-integral weight-sum bound.