The deterministic term in Liu's aggregate Abel reduction

The discrete Abel main term is an ordinary right Riemann sum for 1 / log. Above 2 monotonicity gives a uniform error. Below 2 the integral is kept explicit, so the singular contribution is not silently treated as an ordinary Riemann sum. Liu's product-cube support gives the exact O(N^(2/3)) indicator mass needed for a subsequent modulus average.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanDiscreteInverseLogMain_succ (m : ℕ) (hm : 2 ≤ m) : liuPanDiscreteInverseLogMain (m + 1) = liuPanDiscreteInverseLogMain m + 1 / Real.log ↑(m + 1)

theorem MathlibNt.SieveTheory.LiuWeight.liuPanDiscreteInverseLogMain_eq_sum (m : ℕ) : liuPanDiscreteInverseLogMain m = if 2 ≤ m then 2 / Real.log 2 + ∑ n ∈ Finset.Ico 3 (m + 1), 1 / Real.log ↑n else 0

Exact telescoping formula for the discrete Abel main term.

theorem MathlibNt.SieveTheory.LiuWeight.abs_liuPanDiscreteInverseLogMain_floor_sub_liuLogarithmicIntegral_le_of_two_le (kappa x : ℝ) (hx : 2 ≤ x) : |liuPanDiscreteInverseLogMain ⌊x⌋₊ - liuLogarithmicIntegral kappa x| ≤ |kappa| + 3 / Real.log 2

Above the logarithmic singularity, the discrete Abel main term differs from the normalized logarithmic integral by a constant independent of x.

theorem MathlibNt.SieveTheory.LiuWeight.floor_natCast_div_natCast_eq_div (y a : ℕ) : ⌊↑y / ↑a⌋₊ = y / a

The rational source arguments use the same integer endpoint as Euclidean division. This keeps the singular x < 2 regime visibly separate from the ordinary Riemann-sum comparison above.

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

Mathlib's interval integral is zero when the interval crosses the non-integrable logarithmic singularity at 1.

theorem MathlibNt.SieveTheory.LiuWeight.abs_integral_inverseLogDensity_le_log_inv_sub_one {x : ℝ} (hx : 1 < x) (hx2 : x ≤ 2) : |∫ (t : ℝ) in 2..x, 1 / Real.log t| ≤ 2 * Real.log (1 / (x - 1))

On the integrable side of the singularity, the short integral grows at most logarithmically in the reciprocal distance from 1.

theorem MathlibNt.SieveTheory.LiuWeight.abs_liuPanDiscreteInverseLogMain_floor_sub_liuLogarithmicIntegral_le_of_nonneg_lt_two (kappa x : ℝ) (hx : 0 ≤ x) (hx2 : x < 2) : |liuPanDiscreteInverseLogMain ⌊x⌋₊ - liuLogarithmicIntegral kappa x| ≤ |kappa| + |∫ (t : ℝ) in 2..x, 1 / Real.log t|

Below the endpoint 2, the discrete part is zero. The displayed integral is the only possible logarithmic singular contribution; no assertion of interval-integrability through 1 is being made.

theorem MathlibNt.SieveTheory.LiuWeight.abs_liuPanDiscreteInverseLogMain_floor_sub_liuLogarithmicIntegral_le (kappa x : ℝ) (hx : 0 ≤ x) : |liuPanDiscreteInverseLogMain ⌊x⌋₊ - liuLogarithmicIntegral kappa x| ≤ |kappa| + 3 / Real.log 2 + if 1 < x ∧ x < 2 then 2 * Real.log (1 / (x - 1)) else 0

A uniform formula for the error on x ≥ 0. The only growing term is the explicit logarithm of the reciprocal distance to the integrable side of the singularity at 1; on the non-integrable side Mathlib's integral is zero.

theorem MathlibNt.SieveTheory.LiuWeight.abs_liuPanDiscreteInverseLogMain_div_sub_liuLogarithmicIntegral_le (kappa : ℝ) (y a : ℕ) : |liuPanDiscreteInverseLogMain (y / a) - liuLogarithmicIntegral kappa (↑y / ↑a)| ≤ |kappa| + 3 / Real.log 2 + 2 * Real.log ↑(a + 1)

At rational source arguments the distance from the singularity is either zero/non-integrable or at least 1/a, giving a uniform logarithmic bound.

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

The uniform scalar error used for every source index a ≤ N.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanInverseLogDeterministicErrorBound kappa N = |kappa| + 3 / Real.log 2 + 2 * Real.log ↑(N + 1)

theorem MathlibNt.SieveTheory.LiuWeight.liuPanInverseLogDeterministicErrorBound_nonneg (kappa : ℝ) (N : ℕ) : 0 ≤ liuPanInverseLogDeterministicErrorBound kappa N

theorem MathlibNt.SieveTheory.LiuWeight.abs_liuPanAggregateInverseLogDeterministicTerm_source_le (kappa : ℝ) (N y q : ℕ) (hN : 1 ≤ N) : |liuPanAggregateInverseLogDeterministicTerm kappa y N q (liuWeight N (liuSourceZ10 N) (liuSourceY3 N))| ≤ 3 * ↑N ^ (2 / 3) * liuPanInverseLogDeterministicErrorBound kappa N

Product-cube support turns the deterministic source sum into N^(2/3) times one logarithmic error factor.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateInverseLogDeterministicMaxY_source_le (kappa : ℝ) (N q : ℕ) (hN : 1 ≤ N) : liuPanAggregateInverseLogDeterministicMaxY kappa N q N (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) ≤ 3 * ↑N ^ (2 / 3) * liuPanInverseLogDeterministicErrorBound kappa N

The bound is independent of both maximized variables.

theorem MathlibNt.SieveTheory.LiuWeight.liuMainPanAggregateInverseLogDeterministicAverage_source_le (kappa : ℝ) (N : ℕ) (B : ℝ) (hN : 1 ≤ N) : liuMainPanAggregateInverseLogDeterministicAverage kappa N (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) B ≤ 3 * ↑N ^ (2 / 3) * liuPanInverseLogDeterministicErrorBound kappa N * liuPanPrimePowerH3Mass (panModulusCutoff N B)

The normalized modulus mass is exactly the finite H₃ mass.

theorem MathlibNt.SieveTheory.LiuWeight.liuMainPanAggregateInverseLogDeterministicAverage_source_le_rpow_polylog (kappa : ℝ) : ∃ (C : ℝ), 0 < C ∧ ∀ (N : ℕ) (B : ℝ), 3 ≤ N → 0 ≤ B → liuMainPanAggregateInverseLogDeterministicAverage kappa N (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) B ≤ C * ↑N ^ (2 / 3) * Real.log ↑N ^ 7

Uniformly in the Pan parameter B ≥ 0, the deterministic average has the sublinear scale N^(2/3) log(N)^7.

theorem MathlibNt.SieveTheory.LiuWeight.eventually_liuMainPanAggregateInverseLogDeterministicBoundAt_source (kappa A : ℝ) (_hA : 0 < A) : ∃ (C : ℝ), 0 < C ∧ ∃ (N0 : ℕ), ∀ (N : ℕ), N0 ≤ N → ∀ (B : ℝ), 0 ≤ B → LiuMainPanAggregateInverseLogDeterministicBoundAt kappa N (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) A B C

Every fixed logarithmic saving eventually dominates the deterministic N^(2/3) log(N)^7 scale, uniformly for all B ≥ 0.

def MathlibNt.SieveTheory.LiuWeight.LiuMainPanAggregateInverseLogPsiSourceFamilyBound : Prop

The only remaining source-family hypothesis is the aggregate psi estimate.

Equations

• MathlibNt.SieveTheory.LiuWeight.LiuMainPanAggregateInverseLogPsiSourceFamilyBound = ∀ (A : ℝ), 0 < A → ∃ (Cpsi : ℝ), 0 < Cpsi ∧ ∃ (B : ℝ), 0 ≤ B ∧ ∃ (N0 : ℕ), ∀ (N : ℕ), N0 ≤ N → MathlibNt.SieveTheory.LiuWeight.LiuMainPanAggregateInverseLogPsiBoundAt N (MathlibNt.SieveTheory.LiuWeight.liuWeight N (MathlibNt.SieveTheory.LiuWeight.liuSourceZ10 N) (MathlibNt.SieveTheory.LiuWeight.liuSourceY3 N)) A B Cpsi

theorem MathlibNt.SieveTheory.LiuWeight.LiuMainPanAggregateInverseLogPsiSourceFamilyBound.to_sourceFamilyBound {kappa : ℝ} (hpsi : LiuMainPanAggregateInverseLogPsiSourceFamilyBound) : LiuMainPanAggregateInverseLogSourceFamilyBound kappa

The unconditional deterministic estimate packages any aggregate psi source-family bound into the corrected two-component contract.