Adapted from PrimeNumberTheoremAnd/IEANTN/Mertens.lean, AlexKontorovich/PrimeNumberTheoremAnd revision c39a751132c88b6e8080b74c74023fd95b3d8be0 (Apache-2.0). The first Mertens theorem only; blueprint metadata and unused results omitted. The explicit error constant is relaxed to avoid unrelated integral estimates.

First Mertens theorem with a coefficient-independent bounded error. Adapted proofs retain the upstream theorem names inside a project namespace.

theorem CCDN.Mertens.sum_Ioc_one_eq_sum_Ioc_zero {f : ℕ → ℝ} {x : ℕ} (hx : 1 ≤ x) (hf : f 1 = 0) : ∑ n ∈ Finset.Ioc 1 x, f n = ∑ n ∈ Finset.Ioc 0 x, f n

theorem CCDN.Mertens.sum_log_le {x : ℝ} (hx : 1 ≤ x) : ∑ n ∈ Finset.Ioc 0 ⌊x⌋₊, Real.log ↑n ≤ x * Real.log x

theorem CCDN.Mertens.integral_log_le {a b : ℝ} (ha : 1 ≤ a) (hab : a ≤ b) : ∫ (t : ℝ) in a..b, Real.log t ≤ Real.log b * (b - a)

theorem CCDN.Mertens.sum_log_ge {x : ℝ} (hx : 1 ≤ x) : ∑ n ∈ Finset.Ioc 0 ⌊x⌋₊, Real.log ↑n ≥ x * Real.log x - 2 * x

theorem CCDN.Mertens.sum_log_eq_log_factorial (x : ℝ) : ∑ n ∈ Finset.Ioc 0 ⌊x⌋₊, Real.log ↑n = Real.log ↑⌊x⌋₊.factorial

theorem CCDN.Mertens.sum_log_eq_sum_mangoldt {x : ℝ} : ∑ n ∈ Finset.Ioc 0 ⌊x⌋₊, Real.log ↑n = ∑ d ∈ Finset.Ioc 0 ⌊x⌋₊, ArithmeticFunction.vonMangoldt d * ↑⌊x / ↑d⌋₊

@[reducible, inline]

noncomputable abbrev CCDN.Mertens.E₁Λ (x : ℝ) : ℝ

The error in the logarithmically weighted von Mangoldt sum.

Equations

• CCDN.Mertens.E₁Λ x = ∑ d ∈ Finset.Ioc 0 ⌊x⌋₊, ArithmeticFunction.vonMangoldt d / ↑d - Real.log x

theorem CCDN.Mertens.sum_mangoldt_div_eq (x : ℝ) : ∑ d ∈ Finset.Ioc 0 ⌊x⌋₊, ArithmeticFunction.vonMangoldt d / ↑d = Real.log x + E₁Λ x

theorem CCDN.Mertens.E₁Λ.ge {x : ℝ} (hx : 1 ≤ x) : E₁Λ x ≥ -2

theorem CCDN.Mertens.E₁Λ.le {x : ℝ} (hx : 1 ≤ x) : E₁Λ x ≤ Real.log 4 + 4

theorem CCDN.Mertens.sum_mangoldt_div_eq_log {x : ℝ} (hx : 1 ≤ x) : |∑ d ∈ Finset.Ioc 0 ⌊x⌋₊, ArithmeticFunction.vonMangoldt d / ↑d - Real.log x| ≤ Real.log 4 + 4

theorem CCDN.Mertens.E₁Λ.bounded' : ∃ c > 0, ∀ x ≥ 1, |E₁Λ x| ≤ c

theorem CCDN.Mertens.E₁Λ.bounded : E₁Λ =O[Filter.atTop] fun (x : ℝ) => 1

theorem CCDN.Mertens.one_eq_o_log : (fun (x : ℝ) => 1) =o[Filter.atTop] fun (x : ℝ) => Real.log x

theorem CCDN.Mertens.sum_mangoldt_div_eq_log' : Asymptotics.IsEquivalent Filter.atTop (fun (x : ℝ) => ∑ d ∈ Finset.Ioc 0 ⌊x⌋₊, ArithmeticFunction.vonMangoldt d / ↑d) fun (x : ℝ) => Real.log x

@[reducible, inline]

noncomputable abbrev CCDN.Mertens.E₁p (x : ℝ) : ℝ

The error in the prime sum of log p / p.

Equations

• CCDN.Mertens.E₁p x = ∑ p ∈ Finset.Ioc 0 ⌊x⌋₊ with Nat.Prime p, Real.log ↑p / ↑p - Real.log x

theorem CCDN.Mertens.sum_log_prime_div_eq (x : ℝ) : ∑ p ∈ Finset.Ioc 0 ⌊x⌋₊ with Nat.Prime p, Real.log ↑p / ↑p = Real.log x + E₁p x

theorem CCDN.Mertens.E₁p.le_E₁Λ (x : ℝ) : E₁p x ≤ E₁Λ x

theorem CCDN.Mertens.E₁p.le {x : ℝ} (hx : 1 ≤ x) : E₁p x ≤ Real.log 4 + 4

@[reducible, inline]

noncomputable abbrev CCDN.Mertens.E₁ : ℝ

The convergent prime-power correction between the prime and von Mangoldt sums.

Equations

• CCDN.Mertens.E₁ = ∑' (p : ℕ), if Nat.Prime p then Real.log ↑p / (↑p * (↑p - 1)) else 0

theorem CCDN.Mertens.E₁.summand_nonneg (p : ℕ) : 0 ≤ if Nat.Prime p then Real.log ↑p / (↑p * (↑p - 1)) else 0

theorem CCDN.Mertens.E₁.summable : Summable fun (p : ℕ) => if Nat.Prime p then Real.log ↑p / (↑p * (↑p - 1)) else 0

theorem CCDN.Mertens.E₁Λ.le_E₁p_add_E₁ {x : ℝ} (hx : 1 ≤ x) : E₁Λ x ≤ E₁p x + E₁

theorem CCDN.Mertens.E₁p.ge {x : ℝ} (hx : 1 ≤ x) : E₁p x ≥ -2 - E₁

theorem CCDN.Mertens.prime_sum_bounded_error {x : ℝ} (hx : 1 ≤ x) : |∑ p ∈ Finset.Ioc 0 ⌊x⌋₊ with Nat.Prime p, Real.log ↑p / ↑p - Real.log x| ≤ Real.log 4 + 6 + E₁