Uniform prime-sum replacement, including the Buchstab corner

For primeErrorStart ≤ y, y² ≤ x, and log x / log y ≤ 100, the actual prime sum over y ≤ p < sqrt x differs from x / log x * ((log x / log y) * buchstab (log x / log y) - 1) by at most 106 * (primeErrorEnvelope y + 1 / log y) * (x / log y). For (y, sqrt x], the constant is 104. Both include x = y².

The proof constructs an integrable derivative representative, splits FTC at the sole possible interior corner exp (log x / 3), and keeps the extra f / log² integral from the comparator t / log t.

The finite summation argument below follows Mathlib's AbelSummation (Xavier Roblot, Apache 2.0), replacing its everywhere differentiability assumption by the fundamental theorem on subintervals.

theorem LiLiuPrereqBuchstab.integral_eq_sub_of_hasDerivAt_off_one {a b c : ℝ} {f g : ℝ → ℝ} (hab : a ≤ b) (hf : ContinuousOn f (Set.Icc a b)) (hd : ∀ t ∈ Set.Ioo a b, t ≠ c → HasDerivAt f (g t) t) (hg : IntervalIntegrable g MeasureTheory.volume a b) : ∫ (t : ℝ) in a..b, g t = f b - f a

FTC with one exceptional interior point. No derivative at the corner or at either endpoint is assumed.

theorem LiLiuPrereqBuchstab.sum_mul_abel_of_ftc {a b : ℝ} {f g : ℝ → ℝ} (c : ℕ → ℝ) (ha : 0 ≤ a) (hab : a ≤ b) (hg : MeasureTheory.IntegrableOn g (Set.Icc a b) MeasureTheory.volume) (hftc : ∀ (s t : ℝ), a ≤ s → s ≤ t → t ≤ b → ∫ (v : ℝ) in s..t, g v = f t - f s) : ∑ k ∈ Finset.Ioc ⌊a⌋₊ ⌊b⌋₊, f ↑k * c k = f b * ∑ k ∈ Finset.Icc 0 ⌊b⌋₊, c k - f a * ∑ k ∈ Finset.Icc 0 ⌊a⌋₊, c k - ∫ (t : ℝ) in a..b, g t * ∑ k ∈ Finset.Icc 0 ⌊t⌋₊, c k

Abel summation for an integrable derivative representative with FTC on every subinterval. This also applies to continuous piecewise-C¹ weights.

theorem LiLiuPrereqBuchstab.prime_abel_off_one {a b c : ℝ} {f g : ℝ → ℝ} (ha : 0 ≤ a) (hab : a ≤ b) (hf : ContinuousOn f (Set.Icc a b)) (hd : ∀ t ∈ Set.Ioo a b, t ≠ c → HasDerivAt f (g t) t) (hg : MeasureTheory.IntegrableOn g (Set.Icc a b) MeasureTheory.volume) : ∑ p ∈ primesIoc a b, f ↑p = f b * primePi b - f a * primePi a - ∫ (t : ℝ) in a..b, g t * primePi t

Actual prime Abel summation with a single corner. The derivative representative need not equal deriv f at the corner or the endpoints.

noncomputable def LiLiuPrereqBuchstab.buchstabSlope (u : ℝ) : ℝ

A derivative representative; the chosen value at 2 is immaterial.

Equations

• LiLiuPrereqBuchstab.buchstabSlope u = if u ≤ 2 then -(1 / u ^ 2) else (LiLiuPrereqBuchstab.buchstab (u - 1) - LiLiuPrereqBuchstab.buchstab u) / u

theorem LiLiuPrereqBuchstab.measurable_buchstabSlope : Measurable buchstabSlope

theorem LiLiuPrereqBuchstab.hasDerivAt_buchstab_off_two {u : ℝ} (hu : 1 < u) (hu2 : u ≠ 2) : HasDerivAt buchstab (buchstabSlope u) u

theorem LiLiuPrereqBuchstab.abs_buchstabSlope_le_one {u : ℝ} (hu : 1 ≤ u) : |buchstabSlope u| ≤ 1

noncomputable def LiLiuPrereqBuchstab.buchstabPrimeKernel (x t : ℝ) : ℝ

The actual weight occurring in the rough-count recursion.

Equations

• LiLiuPrereqBuchstab.buchstabPrimeKernel x t = x / (t * Real.log t) * LiLiuPrereqBuchstab.buchstab (Real.log x / Real.log t - 1)

noncomputable def LiLiuPrereqBuchstab.buchstabPrimeKernelSlope (x t : ℝ) : ℝ

Factored derivative representative, including an arbitrary corner value.

Equations

• LiLiuPrereqBuchstab.buchstabPrimeKernelSlope x t = -(x / (t ^ 2 * Real.log t)) * ((1 + 1 / Real.log t) * LiLiuPrereqBuchstab.buchstab (Real.log x / Real.log t - 1) + Real.log x / Real.log t / Real.log t * LiLiuPrereqBuchstab.buchstabSlope (Real.log x / Real.log t - 1))

theorem LiLiuPrereqBuchstab.measurable_buchstabPrimeKernelSlope (x : ℝ) : Measurable (buchstabPrimeKernelSlope x)

theorem LiLiuPrereqBuchstab.continuousOn_buchstabPrimeKernel {a b : ℝ} (x : ℝ) (ha : 1 < a) : ContinuousOn (buchstabPrimeKernel x) (Set.Icc a b)

theorem LiLiuPrereqBuchstab.hasDerivAt_buchstabPrimeKernel {x t : ℝ} (ht : 1 < t) (hu : 1 < Real.log x / Real.log t - 1) (hu2 : Real.log x / Real.log t - 1 ≠ 2) : HasDerivAt (buchstabPrimeKernel x) (buchstabPrimeKernelSlope x t) t

theorem LiLiuPrereqBuchstab.abs_buchstabPrimeKernel_le {x t : ℝ} (hx : 0 ≤ x) (ht : 1 < t) (hu : 1 ≤ Real.log x / Real.log t - 1) : |buchstabPrimeKernel x t| ≤ x / (t * Real.log t)

theorem LiLiuPrereqBuchstab.abs_buchstabPrimeKernelSlope_le {x t : ℝ} (hx : 0 ≤ x) (ht : 0 < t) (hl : 1 ≤ Real.log t) (hu : 1 ≤ Real.log x / Real.log t - 1) (hU : Real.log x / Real.log t ≤ 100) : |buchstabPrimeKernelSlope x t| ≤ 102 * (x / (t ^ 2 * Real.log t))

Uniform differential bound on the entire compact parameter band.

theorem LiLiuPrereqBuchstab.integrableOn_buchstabPrimeKernelSlope {x y : ℝ} (hy : primeErrorStart ≤ y) (hxy : y ^ 2 ≤ x) (hU : Real.log x / Real.log y ≤ 100) : MeasureTheory.IntegrableOn (buchstabPrimeKernelSlope x) (Set.Icc y √x) MeasureTheory.volume

theorem LiLiuPrereqBuchstab.buchstabPrimeKernel_abel {x y : ℝ} (hy : primeErrorStart ≤ y) (hxy : y ^ 2 ≤ x) (hU : Real.log x / Real.log y ≤ 100) : ∑ p ∈ primesIoc y √x, buchstabPrimeKernel x ↑p = buchstabPrimeKernel x √x * primePi √x - buchstabPrimeKernel x y * primePi y - ∫ (t : ℝ) in y..√x, buchstabPrimeKernelSlope x t * primePi t

The actual prime kernel satisfies Abel summation, even when exp (log x / 3) lies in the interval.

theorem LiLiuPrereqBuchstab.prime_abel_log_error_identity {a b c : ℝ} {f g : ℝ → ℝ} (ha : 1 < a) (hab : a ≤ b) (hf : ContinuousOn f (Set.Icc a b)) (hd : ∀ t ∈ Set.Ioo a b, t ≠ c → HasDerivAt f (g t) t) (hg : MeasureTheory.IntegrableOn g (Set.Icc a b) MeasureTheory.volume) : ∑ p ∈ primesIoc a b, f ↑p - ∫ (t : ℝ) in a..b, f t / Real.log t = (f b * (primePi b - b / Real.log b) - f a * (primePi a - a / Real.log a) - ∫ (t : ℝ) in a..b, g t * (primePi t - t / Real.log t)) - ∫ (t : ℝ) in a..b, f t / Real.log t ^ 2

Subtracting t / log t, not Li(t), leaves an explicit extra f(t) / log² t integral.

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

theorem LiLiuPrereqBuchstab.prime_abel_log_error_le {a b c X A : ℝ} {f g : ℝ → ℝ} (ha : primeErrorStart ≤ a) (hab : a ≤ b) (hX : 0 ≤ X) (hA : 0 ≤ A) (hf : ContinuousOn f (Set.Icc a b)) (hd : ∀ t ∈ Set.Ioo a b, t ≠ c → HasDerivAt f (g t) t) (hg : MeasureTheory.IntegrableOn g (Set.Icc a b) MeasureTheory.volume) (hfBound : ∀ t ∈ Set.Icc a b, |f t| ≤ X / (t * Real.log t)) (hgBound : ∀ t ∈ Set.Icc a b, |g t| ≤ A * (X / (t ^ 2 * Real.log t))) : |∑ p ∈ primesIoc a b, f ↑p - ∫ (t : ℝ) in a..b, f t / Real.log t| ≤ (A + 2) * primeErrorEnvelope a * (X / Real.log a) + X / Real.log a ^ 2

A quantitative, parameter-independent Abel estimate from the actual PNT. The only weight assumptions are continuity, an integrable piecewise derivative, and explicit pointwise bounds.

theorem LiLiuPrereqBuchstab.buchstabPrimeKernel_sum_Ioc_error_le {x y : ℝ} (hy : primeErrorStart ≤ y) (hxy : y ^ 2 ≤ x) (hU : Real.log x / Real.log y ≤ 100) : |∑ p ∈ primesIoc y √x, buchstabPrimeKernel x ↑p - x / Real.log x * (Real.log x / Real.log y * buchstab (Real.log x / Real.log y) - 1)| ≤ 104 * (primeErrorEnvelope y + 1 / Real.log y) * (x / Real.log y)

Uniform prime-sum replacement on (y, sqrt x], with a numerical constant independent of both real parameters, including x = y².

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

The lower prime cutoff is included, the upper cutoff is excluded.

Equations

• LiLiuPrereqBuchstab.primesIco a b = {p ∈ LiLiuPrereqBuchstab.primesIcc a b | ↑p < b}

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

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

Exact upper-endpoint correction, also valid on a degenerate interval.

theorem LiLiuPrereqBuchstab.buchstabPrimeKernel_sum_Ico_error_le {x y : ℝ} (hy : primeErrorStart ≤ y) (hxy : y ^ 2 ≤ x) (hU : Real.log x / Real.log y ≤ 100) : |∑ p ∈ primesIco y √x, buchstabPrimeKernel x ↑p - x / Real.log x * (Real.log x / Real.log y * buchstab (Real.log x / Real.log y) - 1)| ≤ 106 * (primeErrorEnvelope y + 1 / Real.log y) * (x / Real.log y)

Uniform replacement (H) with the actual strict-upper prime cutoff y ≤ p < sqrt x. The explicit constant 106 works for every admissible x,y; no differentiability is asserted at the Buchstab corner.

theorem LiLiuPrereqBuchstab.buchstab_prime_sum_replacement_uniform : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (x y : ℝ), primeErrorStart ≤ y → y ^ 2 ≤ x → Real.log x / Real.log y ≤ 100 → |∑ p ∈ primesIco y √x, x / (↑p * Real.log ↑p) * buchstab (Real.log x / Real.log ↑p - 1) - x / Real.log x * (Real.log x / Real.log y * buchstab (Real.log x / Real.log y) - 1)| ≤ C * (primeErrorEnvelope y + 1 / Real.log y) * (x / Real.log y)

The constant is quantified before both parameters. The summand and main term are the actual Buchstab kernel, not abstract replacement interfaces.