Documentation

AnalyticNumberTheory.Sieve.GoldbachDensity

Goldbach local density #

The Goldbach-type local density ν(d) = ∏_{p | d} 1/(p-1) used by additive sieve problems such as Chen's theorem and the Goldbach conjecture. On squarefree moduli it is the reciprocal totient, which is the main term of the Bombieri--Vinogradov distribution estimates.

source
noncomputable def AnalyticNumberTheory.Sieve.goldbachNu :
ArithmeticFunction ℝ

Goldbach local density: ν(d) = ∏_{p | d} 1/(p-1).

Equations
Instances For
    source
    theorem AnalyticNumberTheory.Sieve.goldbachNu_apply_prime {p : ℕ} (hp : Nat.Prime p) :
    goldbachNu p = 1 / (↑p - 1)

    The Goldbach density has the expected value on a prime.

    source
    theorem AnalyticNumberTheory.Sieve.goldbachNu_isMultiplicative :
    goldbachNu.IsMultiplicative

    The Goldbach density is multiplicative.

    source
    theorem AnalyticNumberTheory.Sieve.goldbachNu_pos_of_prime {p : ℕ} (hp : Nat.Prime p) :
    0 < goldbachNu p

    The Goldbach density is positive at every prime.

    source
    theorem AnalyticNumberTheory.Sieve.goldbachNu_lt_one_of_prime {p : ℕ} (hp : Nat.Prime p) (hp2 : 2 < p) :
    goldbachNu p < 1

    The Goldbach density is bounded by one at every prime larger than two.

    source
    theorem AnalyticNumberTheory.Sieve.totient_eq_prod_primeFactors_of_squarefree {n : ℕ} (hn : Squarefree n) :
    n.totient = ∏ p ∈ n.primeFactors, (p - 1)

    The totient of a squarefree natural is the product of p - 1 over its prime factors.

    source
    theorem AnalyticNumberTheory.Sieve.goldbachNu_squarefree_eq_inv_totient {d : ℕ} (hd : Squarefree d) :
    goldbachNu d = 1 / ↑d.totient

    The Goldbach density of a squarefree modulus is exactly the reciprocal totient: ν(d) = 1/φ(d). This identifies the distribution main term ν(d) · x/log x with the standard Bombieri--Vinogradov main term li(x)/φ(d).