Elementary finite objects for Mertens' theorems

This file defines the finite set of primes at most x, its reciprocal sum, and the corresponding Euler product. It contains only elementary finite-sum, finite-product, positivity, and local logarithm estimates; analytic asymptotic results belong in later modules.

def AnalyticNumberTheory.Mertens.primesUpTo (x : ℕ) : Finset ℕ

The finite set of prime natural numbers at most x.

Equations

• AnalyticNumberTheory.Mertens.primesUpTo x = Finset.filter Nat.Prime (Finset.range (x + 1))

@[simp]

theorem AnalyticNumberTheory.Mertens.mem_primesUpTo {p x : ℕ} : p ∈ primesUpTo x ↔ Nat.Prime p ∧ p ≤ x

theorem AnalyticNumberTheory.Mertens.primesUpTo_mono {x y : ℕ} (hxy : x ≤ y) : primesUpTo x ⊆ primesUpTo y

The sets of primes up to x are nested as x increases.

theorem AnalyticNumberTheory.Mertens.primesUpTo_eq_empty_of_le_one {x : ℕ} (hx : x ≤ 1) : primesUpTo x = ∅

noncomputable def AnalyticNumberTheory.Mertens.primeReciprocalSum (x : ℕ) : ℝ

The finite reciprocal-prime sum ∑ p ≤ x, 1 / p.

Equations

• AnalyticNumberTheory.Mertens.primeReciprocalSum x = ∑ p ∈ AnalyticNumberTheory.Mertens.primesUpTo x, 1 / ↑p

noncomputable def AnalyticNumberTheory.Mertens.primeProduct (x : ℕ) : ℝ

The finite Euler product ∏ p ≤ x, (1 - 1 / p).

Equations

• AnalyticNumberTheory.Mertens.primeProduct x = ∏ p ∈ AnalyticNumberTheory.Mertens.primesUpTo x, (1 - 1 / ↑p)

theorem AnalyticNumberTheory.Mertens.primeReciprocalSum_eq_zero_of_le_one {x : ℕ} (hx : x ≤ 1) : primeReciprocalSum x = 0

There are no reciprocal-prime terms below 2.

@[simp]

theorem AnalyticNumberTheory.Mertens.primeReciprocalSum_zero : primeReciprocalSum 0 = 0

@[simp]

theorem AnalyticNumberTheory.Mertens.primeReciprocalSum_one : primeReciprocalSum 1 = 0

theorem AnalyticNumberTheory.Mertens.primeReciprocalSum_nonneg (x : ℕ) : 0 ≤ primeReciprocalSum x

theorem AnalyticNumberTheory.Mertens.primeReciprocalSum_mono : Monotone primeReciprocalSum

The reciprocal-prime sum is monotone in its cutoff.

@[simp]

theorem AnalyticNumberTheory.Mertens.primeProduct_zero : primeProduct 0 = 1

@[simp]

theorem AnalyticNumberTheory.Mertens.primeProduct_one : primeProduct 1 = 1

theorem AnalyticNumberTheory.Mertens.primeFactor_pos {p : ℕ} (hp : Nat.Prime p) : 0 < 1 - 1 / ↑p

Every Euler factor indexed by a prime is strictly positive.

theorem AnalyticNumberTheory.Mertens.primeFactor_le_one {p : ℕ} (_hp : Nat.Prime p) : 1 - 1 / ↑p ≤ 1

Every Euler factor indexed by a prime is at most one.

theorem AnalyticNumberTheory.Mertens.primeProduct_pos (x : ℕ) : 0 < primeProduct x

theorem AnalyticNumberTheory.Mertens.primeProduct_nonneg (x : ℕ) : 0 ≤ primeProduct x

theorem AnalyticNumberTheory.Mertens.primeProduct_le_one (x : ℕ) : primeProduct x ≤ 1

theorem AnalyticNumberTheory.Mertens.primeProduct_antitone : Antitone primeProduct

The finite Euler product is antitone in its cutoff.

theorem AnalyticNumberTheory.Mertens.log_primeProduct (x : ℕ) : Real.log (primeProduct x) = ∑ p ∈ primesUpTo x, Real.log (1 - 1 / ↑p)

Taking logarithms converts the finite Euler product into a finite sum.

theorem AnalyticNumberTheory.Mertens.abs_log_one_sub_add_le {t : ℝ} (ht0 : 0 < t) (htle : t ≤ 1 / 2) : |Real.log (1 - t) + t| ≤ 2 * t ^ 2

For 0 < t ≤ 1/2, the error after linearizing log (1 - t) is at most 2 t².

theorem AnalyticNumberTheory.Mertens.abs_log_primeFactor_add_le {p : ℕ} (hp : Nat.Prime p) : |Real.log (1 - 1 / ↑p) + 1 / ↑p| ≤ 2 / ↑p ^ 2

The local logarithmic correction for a prime Euler factor.