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.

noncomputable def AnalyticNumberTheory.Sieve.goldbachNu : ArithmeticFunction ℝ

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

Equations

• AnalyticNumberTheory.Sieve.goldbachNu = ArithmeticFunction.prodPrimeFactors fun (r : ℕ) => 1 / (↑r - 1)

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.

theorem AnalyticNumberTheory.Sieve.goldbachNu_isMultiplicative : goldbachNu.IsMultiplicative

The Goldbach density is multiplicative.

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

The Goldbach density is positive at every prime.

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.

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.

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