Abel summation for prime reciprocal sums

This finite identity is the bridge from effective Chebyshev-theta estimates to Mertens' second theorem. It deliberately contains no asymptotic claim.

noncomputable def AnalyticNumberTheory.Mertens.thetaErrorKernel (t : ℝ) : ℝ

The theta-error contribution to the positive-kernel Abel formula.

Equations

• AnalyticNumberTheory.Mertens.thetaErrorKernel t = (Chebyshev.theta t - t) * (Real.log t + 1) / (t * Real.log t) ^ 2

theorem AnalyticNumberTheory.Mertens.thetaErrorKernel_eq (t : ℝ) : thetaErrorKernel t = Chebyshev.theta t * (Real.log t + 1) / (t * Real.log t) ^ 2 - t * (Real.log t + 1) / (t * Real.log t) ^ 2

theorem AnalyticNumberTheory.Mertens.norm_integral_Ioi_le_div_log {f : ℝ → ℝ} {x C : ℝ} (hx : 1 < x) (hbound : ∀ t ∈ Set.Ioi x, ‖f t‖ ≤ C * (t⁻¹ / Real.log t ^ 2)) : ‖∫ (t : ℝ) in Set.Ioi x, f t‖ ≤ C / Real.log x

A reusable improper-integral tail estimate for the kernel that occurs in the Mertens error term.

theorem AnalyticNumberTheory.Mertens.locallyIntegrableOn_theta : MeasureTheory.LocallyIntegrableOn Chebyshev.theta (Set.Ici 2) MeasureTheory.volume

The Chebyshev theta function is locally integrable away from zero.

theorem AnalyticNumberTheory.Mertens.locallyIntegrableOn_thetaErrorKernel : MeasureTheory.LocallyIntegrableOn thetaErrorKernel (Set.Ici 2) MeasureTheory.volume

The theta-error kernel is locally integrable away from the logarithmic singularity.

theorem AnalyticNumberTheory.Mertens.thetaErrorKernel_isBigO : thetaErrorKernel =O[Filter.atTop] fun (t : ℝ) => t⁻¹ / Real.log t ^ 2

The theta-error kernel has the integrable decay required for the Mertens tail estimate.

theorem AnalyticNumberTheory.Mertens.integrableOn_thetaErrorKernel : MeasureTheory.IntegrableOn thetaErrorKernel (Set.Ioi 2) MeasureTheory.volume

The theta-error kernel is integrable on the improper tail.

noncomputable def AnalyticNumberTheory.Mertens.mertensSecondConstant : ℝ

The constant in the Mertens reciprocal-prime asymptotic, expressed through the theta-error kernel.

Equations

• AnalyticNumberTheory.Mertens.mertensSecondConstant = -Real.log (Real.log 2) + 1 / Real.log 2 + ∫ (t : ℝ) in Set.Ioi 2, AnalyticNumberTheory.Mertens.thetaErrorKernel t

theorem AnalyticNumberTheory.Mertens.thetaErrorKernel_interval_sub_total_eq_neg_tail {x : ℝ} (hx : 2 ≤ x) : (∫ (t : ℝ) in 2..x, thetaErrorKernel t) - ∫ (t : ℝ) in Set.Ioi 2, thetaErrorKernel t = -∫ (t : ℝ) in Set.Ioi x, thetaErrorKernel t

The finite error integral differs from its limiting value by the negative improper tail.

theorem AnalyticNumberTheory.Mertens.intervalIntegrable_thetaErrorKernel {x : ℝ} (hx : 2 ≤ x) : IntervalIntegrable thetaErrorKernel MeasureTheory.volume 2 x

The theta-error kernel is integrable on every finite interval beginning at two.

theorem AnalyticNumberTheory.Mertens.theta_weighted_integral_decomposition {x : ℝ} (hx : 2 ≤ x) : ∫ (t : ℝ) in 2..x, Chebyshev.theta t * (Real.log t + 1) / (t * Real.log t) ^ 2 = (∫ (t : ℝ) in 2..x, t * (Real.log t + 1) / (t * Real.log t) ^ 2) + ∫ (t : ℝ) in 2..x, thetaErrorKernel t

Splitting the theta term in the Abel integral into its identity main term and its theta-error term.

theorem AnalyticNumberTheory.Mertens.thetaErrorKernel_tail_eventually : ∃ C > 0, ∀ᶠ (x : ℝ) in Filter.atTop, ‖∫ (t : ℝ) in Set.Ioi x, thetaErrorKernel t‖ ≤ C / Real.log x

The improper theta-error tail has the Mertens O(1 / log x) rate.

theorem AnalyticNumberTheory.Mertens.primeReciprocalSum_eq_theta_abel {x : ℝ} (hx : 2 ≤ x) : primeReciprocalSum ⌊x⌋₊ = (x * Real.log x)⁻¹ * Chebyshev.theta x - ∫ (t : ℝ) in 2..x, deriv (fun (u : ℝ) => (u * Real.log u)⁻¹) t * Chebyshev.theta t

Abel summation expresses the finite reciprocal-prime sum through the Chebyshev theta function.

theorem AnalyticNumberTheory.Mertens.primeReciprocalSum_eq_theta_div_mul_log_add_integral {x : ℝ} (hx : 2 ≤ x) : primeReciprocalSum ⌊x⌋₊ = Chebyshev.theta x / (x * Real.log x) + ∫ (t : ℝ) in 2..x, Chebyshev.theta t * (Real.log t + 1) / (t * Real.log t) ^ 2

The positive-kernel form of the Abel bridge.

theorem AnalyticNumberTheory.Mertens.theta_abel_main_term {x : ℝ} (hx : 2 ≤ x) : x / (x * Real.log x) + ∫ (t : ℝ) in 2..x, t * (Real.log t + 1) / (t * Real.log t) ^ 2 = Real.log (Real.log x) + (-Real.log (Real.log 2) + 1 / Real.log 2)

The contribution of replacing theta by the identity in the positive-kernel Abel formula.

theorem AnalyticNumberTheory.Mertens.mertensSecond_error_decomposition {x : ℝ} (hx : 2 ≤ x) : primeReciprocalSum ⌊x⌋₊ - (Real.log (Real.log x) + mertensSecondConstant) = (Chebyshev.theta x - x) / (x * Real.log x) - ∫ (t : ℝ) in Set.Ioi x, thetaErrorKernel t

Exact real-variable decomposition underlying Mertens' second theorem.

theorem AnalyticNumberTheory.Mertens.mertensSecond_eventually : ∃ C > 0, ∀ᶠ (x : ℝ) in Filter.atTop, |primeReciprocalSum ⌊x⌋₊ - (Real.log (Real.log x) + mertensSecondConstant)| ≤ C / Real.log x

Mertens' second theorem with an explicit O(1 / log x) error, on the real-variable bridge used by downstream arithmetic applications.

theorem AnalyticNumberTheory.Mertens.mertensSecond_isBigO : (fun (n : ℕ) => primeReciprocalSum n - (Real.log (Real.log ↑n) + mertensSecondConstant)) =O[Filter.atTop] fun (n : ℕ) => 1 / Real.log ↑n

Natural-number Big-O interface for Mertens' second theorem.

theorem AnalyticNumberTheory.Mertens.mertensSecond_nat : ∃ C > 0, ∀ (n : ℕ), 2 ≤ n → |primeReciprocalSum n - (Real.log (Real.log ↑n) + mertensSecondConstant)| ≤ C / Real.log ↑n

Natural-number form of Mertens' second theorem, with the finite initial range absorbed into the uniform constant.

theorem AnalyticNumberTheory.Mertens.primeReciprocalSum_range_le : ∃ (E : ℝ), 0 < E ∧ ∀ (a b : ℕ), 3 ≤ a → a ≤ b → primeReciprocalSum b - primeReciprocalSum (a - 1) ≤ Real.log (Real.log ↑b / Real.log ↑a) + E

Prime reciprocal sum over an interval: for 3 ≤ a ≤ b, Σ_{a ≤ p ≤ b} 1/p ≤ log(log b/log a) + E, with an explicit error from Mertens' second theorem. Subtracting the endpoint log log terms yields the ratio log b/log a.

theorem AnalyticNumberTheory.Mertens.primeReciprocalSum_range_eq (a b : ℕ) (ha : 1 ≤ a) (hab : a ≤ b) : ∑ p ∈ Finset.range (b + 1) with Nat.Prime p ∧ a ≤ p, 1 / ↑p = primeReciprocalSum b - primeReciprocalSum (a - 1)

Interval sum as a difference: Σ_{a ≤ p ≤ b} 1/p = primeReciprocalSum b - primeReciprocalSum (a-1).

theorem AnalyticNumberTheory.Mertens.primeReciprocal_doubleSum_eq (A B : Finset ℕ) : ∑ p ∈ A, ∑ q ∈ B, 1 / (↑p * ↑q) = (∑ p ∈ A, 1 / ↑p) * ∑ q ∈ B, 1 / ↑q

Double reciprocal sum factorization (Fubini): Σ_{p,q} 1/(pq) = (Σ_p 1/p)(Σ_q 1/q).

theorem AnalyticNumberTheory.Mertens.primeReciprocal_doubleSum_le : ∃ (E : ℝ), 0 < E ∧ ∀ (a b c : ℕ), 3 ≤ a → a ≤ b → b ≤ c → ∑ p₁ ∈ Finset.range (b + 1) with Nat.Prime p₁ ∧ a ≤ p₁, ∑ p₂ ∈ Finset.range (c + 1) with Nat.Prime p₂ ∧ b ≤ p₂, 1 / (↑p₁ * ↑p₂) ≤ (Real.log (Real.log ↑b / Real.log ↑a) + E) * (Real.log (Real.log ↑c / Real.log ↑b) + E)

Double reciprocal sum bound: for 3 ≤ a ≤ b ≤ c, Σ_{a ≤ p₁ ≤ b} Σ_{b ≤ p₂ ≤ c} 1/(p₁p₂) ≤ (log(log b/log a) + E)·(log(log c/log b) + E), where E comes from the explicit error in Mertens' second theorem.