Documentation

AnalyticNumberTheory.Mertens.Basic

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.

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

The finite set of prime natural numbers at most x.

Equations
Instances For
    source
    @[simp]
    theorem AnalyticNumberTheory.Mertens.mem_primesUpTo {p x : ℕ} :
    p ∈ primesUpTo x ↔ Nat.Prime p ∧ p ≤ x
    source
    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.

    source
    theorem AnalyticNumberTheory.Mertens.primesUpTo_eq_empty_of_le_one {x : ℕ} (hx : x ≤ 1) :
    primesUpTo x = ∅
    source
    noncomputable def AnalyticNumberTheory.Mertens.primeReciprocalSum (x : ℕ) :
    ℝ

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

    Equations
    Instances For
      source
      noncomputable def AnalyticNumberTheory.Mertens.primeProduct (x : ℕ) :
      ℝ

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

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

        There are no reciprocal-prime terms below 2.

        source
        @[simp]
        theorem AnalyticNumberTheory.Mertens.primeReciprocalSum_zero :
        primeReciprocalSum 0 = 0
        source
        @[simp]
        theorem AnalyticNumberTheory.Mertens.primeReciprocalSum_one :
        primeReciprocalSum 1 = 0
        source
        theorem AnalyticNumberTheory.Mertens.primeReciprocalSum_nonneg (x : ℕ) :
        0 ≤ primeReciprocalSum x
        source
        theorem AnalyticNumberTheory.Mertens.primeReciprocalSum_mono :
        Monotone primeReciprocalSum

        The reciprocal-prime sum is monotone in its cutoff.

        source
        @[simp]
        theorem AnalyticNumberTheory.Mertens.primeProduct_zero :
        primeProduct 0 = 1
        source
        @[simp]
        theorem AnalyticNumberTheory.Mertens.primeProduct_one :
        primeProduct 1 = 1
        source
        theorem AnalyticNumberTheory.Mertens.primeFactor_pos {p : ℕ} (hp : Nat.Prime p) :
        0 < 1 - 1 / ↑p

        Every Euler factor indexed by a prime is strictly positive.

        source
        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.

        source
        theorem AnalyticNumberTheory.Mertens.primeProduct_pos (x : ℕ) :
        0 < primeProduct x
        source
        theorem AnalyticNumberTheory.Mertens.primeProduct_nonneg (x : ℕ) :
        0 ≤ primeProduct x
        source
        theorem AnalyticNumberTheory.Mertens.primeProduct_le_one (x : ℕ) :
        primeProduct x ≤ 1
        source
        theorem AnalyticNumberTheory.Mertens.primeProduct_antitone :
        Antitone primeProduct

        The finite Euler product is antitone in its cutoff.

        source
        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.

        source
        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².

        source
        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.