Abel summation and elementary weighted sums over actual primes

All endpoints are real. primesIoc a b excludes the lower endpoint and includes the upper endpoint; primesIcc a b includes both.

The finite tails of 1 / (p log p) are bounded by 4 / log a or 5 / log a, respectively. The sum of p / log p is at most 2 b² / log² b. These estimates use the imported actual PNT, not prime-distribution hypotheses supplied to the sum theorems.

noncomputable def LiLiuPrereqBuchstab.primesIoc (a b : ℝ) : Finset ℕ

Equations

• LiLiuPrereqBuchstab.primesIoc a b = {p ∈ ⌊b⌋₊.primesLE | a < ↑p}

noncomputable def LiLiuPrereqBuchstab.primesIcc (a b : ℝ) : Finset ℕ

Equations

• LiLiuPrereqBuchstab.primesIcc a b = {p ∈ ⌊b⌋₊.primesLE | a ≤ ↑p}

theorem LiLiuPrereqBuchstab.mem_primesIoc {a b : ℝ} (hb : 0 ≤ b) {p : ℕ} : p ∈ primesIoc a b ↔ Nat.Prime p ∧ a < ↑p ∧ ↑p ≤ b

theorem LiLiuPrereqBuchstab.mem_primesIcc {a b : ℝ} (hb : 0 ≤ b) {p : ℕ} : p ∈ primesIcc a b ↔ Nat.Prime p ∧ a ≤ ↑p ∧ ↑p ≤ b

theorem LiLiuPrereqBuchstab.primePi_eq_sum_indicator (t : ℝ) : primePi t = ∑ k ∈ Finset.Icc 0 ⌊t⌋₊, if Nat.Prime k then 1 else 0

theorem LiLiuPrereqBuchstab.prime_abel {a b : ℝ} {f : ℝ → ℝ} (ha : 0 ≤ a) (hab : a ≤ b) (hf : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t) (hi : MeasureTheory.IntegrableOn (deriv f) (Set.Icc a b) MeasureTheory.volume) : ∑ p ∈ primesIoc a b, f ↑p = f b * primePi b - f a * primePi a - ∫ (t : ℝ) in a..b, deriv f t * primePi t

Exact prime Abel summation, with the endpoint at a excluded.

theorem LiLiuPrereqBuchstab.integrableOn_mul_primePi {a b : ℝ} {g : ℝ → ℝ} (ha : 0 ≤ a) (hg : MeasureTheory.IntegrableOn g (Set.Icc a b) MeasureTheory.volume) : MeasureTheory.IntegrableOn (fun (t : ℝ) => g t * primePi t) (Set.Icc a b) MeasureTheory.volume

The step-function factor pi(t) preserves integrability on finite intervals.

theorem LiLiuPrereqBuchstab.one_le_log_of_start_le {t : ℝ} (ht : primeErrorStart ≤ t) : 1 ≤ Real.log t

theorem LiLiuPrereqBuchstab.integral_logTailKernel {a b : ℝ} (ha : primeErrorStart ≤ a) (hab : a ≤ b) : ∫ (t : ℝ) in a..b, 4 / (t * Real.log t ^ 2) = 4 / Real.log a - 4 / Real.log b

The elementary logarithmic integral used to bound every finite prime tail.

theorem LiLiuPrereqBuchstab.sum_primesIoc_inv_mul_log_le {y b : ℝ} (hy : primeErrorStart ≤ y) (hyb : y ≤ b) : ∑ p ∈ primesIoc y b, 1 / (↑p * Real.log ↑p) ≤ 4 / Real.log y

(E), excluding the lower endpoint: the constant is independent of both endpoints.

theorem LiLiuPrereqBuchstab.sum_primesIcc_eq_sum_primesIoc_add {y b : ℝ} (hb : 0 ≤ b) (f : ℝ → ℝ) : ∑ p ∈ primesIcc y b, f ↑p = ∑ p ∈ primesIoc y b, f ↑p + if ∃ p ∈ primesIcc y b, ↑p = y then f y else 0

Exact lower-endpoint correction; it is present only when the real endpoint is a prime.

theorem LiLiuPrereqBuchstab.sum_primesIcc_inv_mul_log_le {y b : ℝ} (hy : primeErrorStart ≤ y) (hyb : y ≤ b) : ∑ p ∈ primesIcc y b, 1 / (↑p * Real.log ↑p) ≤ 5 / Real.log y

(E), with both endpoints included and an explicit absolute constant.

theorem LiLiuPrereqBuchstab.sum_primesIcc_div_log_le {y b : ℝ} (hy : primeErrorStart ≤ y) (hb : primeErrorStart ≤ b) : ∑ p ∈ primesIcc y b, ↑p / Real.log ↑p ≤ 2 * b ^ 2 / Real.log b ^ 2

(F), with real endpoints and the fixed constant from the actual PNT bound.