A genuine logarithmic-integral model for Liu's main term

For every additive normalization κ, this module defines κ + ∫ t in 2..x, 1 / log t. A standard paper logarithmic integral restricted to x ≥ 2 has this form for a particular value of κ. Liu's source notation does not identify that normalization, so it remains a parameter here.

This function is not identified with the analytic-number-theory compatibility function called logarithmicIntegral, which is the historical proxy x / log x.

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegral (κ x : ℝ) : ℝ

The logarithmic integral above 2, with an explicit additive normalization.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegral κ x = κ + ∫ (t : ℝ) in 2..x, 1 / Real.log t

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegral_sub_normalization (κ₂ κ₁ x : ℝ) : liuLogarithmicIntegral κ₂ x - liuLogarithmicIntegral κ₁ x = κ₂ - κ₁

Changing the additive normalization changes the logarithmic integral by exactly the same constant.

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegralRemainder (κ x : ℝ) : ℝ

Difference between Liu's genuine logarithmic integral and the x / log x proxy used in the source main-term calculation.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegralRemainder κ x = MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegral κ x - x / Real.log x

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegralUpperConstant (κ : ℝ) : ℝ

A global upper-model constant for liuLogarithmicIntegral κ on x ≥ 2.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegralUpperConstant κ = |κ| + 2 / Real.log 2 + 2

theorem MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegrand_nonneg {t : ℝ} (ht : 2 ≤ t) : 0 ≤ 1 / Real.log t

The logarithmic-integral density is nonnegative above 2.

theorem MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegrand_intervalIntegrable_of_two_le {a b : ℝ} (ha : 2 ≤ a) (hab : a ≤ b) : IntervalIntegrable (fun (t : ℝ) => 1 / Real.log t) MeasureTheory.volume a b

The logarithmic-integral density is interval integrable on every interval whose left endpoint is at least 2.

theorem MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegrand_intervalIntegrable {x : ℝ} (hx : 2 ≤ x) : IntervalIntegrable (fun (t : ℝ) => 1 / Real.log t) MeasureTheory.volume 2 x

The density is integrable from 2 to every x ≥ 2.

theorem MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegral_integral_nonneg {x : ℝ} (hx : 2 ≤ x) : 0 ≤ ∫ (t : ℝ) in 2..x, 1 / Real.log t

The logarithmic integral from 2 to x ≥ 2 is nonnegative.

theorem MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegral_nonneg (κ : ℝ) (hκ : 0 ≤ κ) {x : ℝ} (hx : 2 ≤ x) : 0 ≤ liuLogarithmicIntegral κ x

A nonnegative additive normalization makes the genuine logarithmic integral nonnegative throughout its source range.

theorem MathlibNt.SieveTheory.LiuWeight.liuLogarithmicSquaredIntegrand_intervalIntegrable {x : ℝ} (hx : 2 ≤ x) : IntervalIntegrable (fun (t : ℝ) => 1 / Real.log t ^ 2) MeasureTheory.volume 2 x

The squared logarithmic density is interval integrable above 2.

theorem MathlibNt.SieveTheory.LiuWeight.hasDerivAt_div_log {t : ℝ} (ht : 2 ≤ t) : HasDerivAt (fun (u : ℝ) => u / Real.log u) (1 / Real.log t - 1 / Real.log t ^ 2) t

Derivative identity behind integration by parts for x / log x.

theorem MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegralRemainder_eq (κ : ℝ) {x : ℝ} (hx : 2 ≤ x) : liuLogarithmicIntegralRemainder κ x = κ - 2 / Real.log 2 + ∫ (t : ℝ) in 2..x, 1 / Real.log t ^ 2

Exact integration-by-parts expansion of the genuine-minus-proxy remainder.

theorem MathlibNt.SieveTheory.LiuWeight.div_log_le_liuLogarithmicIntegral {x : ℝ} (hx : 2 ≤ x) : x / Real.log x ≤ liuLogarithmicIntegral (2 / Real.log 2) x

The normalization 2 / log 2 makes the genuine logarithmic integral dominate the elementary proxy on the full source range.

theorem MathlibNt.SieveTheory.LiuWeight.log_le_two_mul_sqrt {x : ℝ} (hx : 2 ≤ x) : Real.log x ≤ 2 * √x

A simple global inequality used to absorb the short part of the integral.

theorem MathlibNt.SieveTheory.LiuWeight.one_le_div_log {x : ℝ} (hx : 2 ≤ x) : 1 ≤ x / Real.log x

Above 2, the ratio x / log x is at least one.

theorem MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegral_integral_le {x : ℝ} (hx : 2 ≤ x) : ∫ (t : ℝ) in 2..x, 1 / Real.log t ≤ (2 / Real.log 2 + 2) * (x / Real.log x)

Explicit global bound for the integral part. For x ≥ 4, split at √x: the first interval is bounded by √x / log 2, and on the second interval log t ≥ log x / 2. The range 2 ≤ x < 4 is handled directly.

theorem MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegralUpperConstant_nonneg (κ : ℝ) : 0 ≤ liuLogarithmicIntegralUpperConstant κ

The explicit upper-model constant is nonnegative.

theorem MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegral_abs_le (κ : ℝ) {x : ℝ} (hx : 2 ≤ x) : |liuLogarithmicIntegral κ x| ≤ liuLogarithmicIntegralUpperConstant κ * x / Real.log x

The normalized logarithmic integral has a global x / log x upper bound.

theorem MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegral_paperLiUpperModel (κ : ℝ) : PaperLiUpperModel (liuLogarithmicIntegral κ) (liuLogarithmicIntegralUpperConstant κ)

Every additive normalization of the genuine integral family supplies the upper model required by the finite Liu R₁ argument.

theorem MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegral_paperQStyleSourceR1Majorant_le_log_square_cutoff (κ : ℝ) (N : ℕ) (ε : ℝ) (hN : 8 ≤ N) (hε : 0 ≤ ε) : paperQStyleSourceR1Majorant (liuLogarithmicIntegral κ) N (liuSourceZ10 N) (paperQSourceCutoff N ε) (liuSourceY3 N) (liuSourceD2 N) ≤ 15 * liuLogarithmicIntegralUpperConstant κ * liuSourceR1P₂ReciprocalBound * paperQStyleDivisorWeightLogConstant * ↑N ^ (9 / 10) * Real.log ↑N ^ 2

The source-cutoff R₁ endpoint instantiated with the genuine normalized logarithmic-integral family.

theorem MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegral_liuPaperQSourceR1Majorant_le_log_square (κ : ℝ) (N : ℕ) (ε : ℝ) (hN : 8 ≤ N) (hε : 0 ≤ ε) : liuPaperQSourceR1Majorant (liuLogarithmicIntegral κ) N ε ≤ 15 * liuLogarithmicIntegralUpperConstant κ * liuSourceR1P₂ReciprocalBound * paperQStyleDivisorWeightLogConstant * ↑N ^ (9 / 10) * Real.log ↑N ^ 2

Liu's R₁ log-square endpoint with the outer divisor sum defined using the source-facing real-cutoff modulus liuPaperQModulus. The weight lower cutoff is separately fixed by liuSourceZ10.