Dirichlet's Theorem on primes in arithmetic progression

The goal of this file is to prove Dirichlet's Theorem: If q is a positive natural number and a : ZMod q is invertible, then there are infinitely many prime numbers p such that (p : ZMod q) = a.

The main steps of the proof are as follows.

1. Define ArithmeticFunction.vonMangoldt.residueClass a for a : ZMod q, which is a function ℕ → ℝ taking the value zero when (n : ℤMod q) ≠ a and Λ n else (where Λ is the von Mangoldt function ArithmeticFunction.vonMangoldt; we have Λ (p^k) = log p for prime powers and Λ n = 0 otherwise.)
2. Show that this function can be written as a linear combination of functions of the form χ * Λ (pointwise product) with Dirichlet characters χ mod q. See ArithmeticFunction.vonMangoldt.residueClass_eq.
3. This implies that the L-series of ArithmeticFunction.vonMangoldt.residueClass a agrees (on re s > 1) with the corresponding linear combination of negative logarithmic derivatives of Dirichlet L-functions. See ArithmeticFunction.vonMangoldt.LSeries_residueClass_eq.
4. Define an auxiliary function ArithmeticFunction.vonMangoldt.LFunctionResidueClassAux a that is this linear combination of negative logarithmic derivatives of L-functions minus (q.totient)⁻¹/(s-1), which cancels the pole at s = 1. See ArithmeticFunction.vonMangoldt.eqOn_LFunctionResidueClassAux for the statement that the auxiliary function agrees with the L-series of ArithmeticFunction.vonMangoldt.residueClass up to the term (q.totient)⁻¹/(s-1).
5. Show that the auxiliary function is continuous on re s ≥ 1; see ArithmeticFunction.vonMangoldt.continuousOn_LFunctionResidueClassAux. This relies heavily on the non-vanishing of Dirichlet L-functions on the closed half-plane re s ≥ 1 (DirichletCharacter.LFunction_ne_zero_of_one_le_re), which in turn can only be stated since we know that the L-series of a Dirichlet character extends to an entire function (unless the character is trivial; then there is a simple pole at s = 1); see DirichletCharacter.LFunction_eq_LSeries (contributed by David Loeffler).
6. Show that the sum of Λ n / n over any residue class, but excluding the primes, converges. See ArithmeticFunction.vonMangoldt.summable_residueClass_non_primes_div.
7. Combining these ingredients, we can deduce that the sum of Λ n / n over the primes in a residue class must diverge. See ArithmeticFunction.vonMangoldt.not_summable_residueClass_prime_div.
8. This finally easily implies that there must be infinitely many primes in the residue class.

Definitions

• ArithmeticFunction.vonMangoldt.residueClass a (see above).
• ArithmeticFunction.vonMangoldt.continuousOn_LFunctionResidueClassAux (see above).

Main Result

We give two versions of Dirichlet's Theorem:

• Nat.setOf_prime_and_eq_mod_infinite states that the set of primes p such that (p : ZMod q) = a is infinite (when a is invertible in ZMod q).
• Nat.forall_exists_prime_gt_and_eq_mod states that for any natural number n there is a prime p > n such that (p : ZMod q) = a.

Tags

prime number, arithmetic progression, residue class, Dirichlet's Theorem

Auxiliary statements

An infinite product or sum over a function supported in prime powers can be written as an iterated product or sum over primes and natural numbers.

theorem tprod_eq_tprod_primes_of_mulSupport_subset_prime_powers {α : Type u_1} [CommGroup α] [UniformSpace α] [IsUniformGroup α] [CompleteSpace α] [T0Space α] {f : ℕ → α} (hfm : Multipliable f) (hf : Function.mulSupport f ⊆ {n : ℕ | IsPrimePow n}) : ∏' (n : ℕ), f n = ∏' (p : Nat.Primes) (k : ℕ), f (↑p ^ (k + 1))

theorem tsum_eq_tsum_primes_of_support_subset_prime_powers {α : Type u_1} [AddCommGroup α] [UniformSpace α] [IsUniformAddGroup α] [CompleteSpace α] [T0Space α] {f : ℕ → α} (hfm : Summable f) (hf : Function.support f ⊆ {n : ℕ | IsPrimePow n}) : ∑' (n : ℕ), f n = ∑' (p : Nat.Primes) (k : ℕ), f (↑p ^ (k + 1))

theorem tprod_eq_tprod_primes_mul_tprod_primes_of_mulSupport_subset_prime_powers {α : Type u_1} [CommGroup α] [UniformSpace α] [IsUniformGroup α] [CompleteSpace α] [T0Space α] {f : ℕ → α} (hfm : Multipliable f) (hf : Function.mulSupport f ⊆ {n : ℕ | IsPrimePow n}) : ∏' (n : ℕ), f n = (∏' (p : Nat.Primes), f ↑p) * ∏' (p : Nat.Primes) (k : ℕ), f (↑p ^ (k + 2))

theorem tsum_eq_tsum_primes_add_tsum_primes_of_support_subset_prime_powers {α : Type u_1} [AddCommGroup α] [UniformSpace α] [IsUniformAddGroup α] [CompleteSpace α] [T0Space α] {f : ℕ → α} (hfm : Summable f) (hf : Function.support f ⊆ {n : ℕ | IsPrimePow n}) : ∑' (n : ℕ), f n = ∑' (p : Nat.Primes), f ↑p + ∑' (p : Nat.Primes) (k : ℕ), f (↑p ^ (k + 2))

The L-series of the von Mangoldt function restricted to a residue class

@[reducible, inline]

noncomputable abbrev ArithmeticFunction.vonMangoldt.residueClass {q : ℕ} (a : ZMod q) : ℕ → ℝ

The von Mangoldt function restricted to the residue class a mod q.

Equations

• ArithmeticFunction.vonMangoldt.residueClass a = {n : ℕ | ↑n = a}.indicator fun (x : ℕ) => ArithmeticFunction.vonMangoldt x

theorem ArithmeticFunction.vonMangoldt.residueClass_nonneg {q : ℕ} (a : ZMod q) (n : ℕ) : 0 ≤ residueClass a n

theorem ArithmeticFunction.vonMangoldt.residueClass_le {q : ℕ} (a : ZMod q) (n : ℕ) : residueClass a n ≤ vonMangoldt n

@[simp]

theorem ArithmeticFunction.vonMangoldt.residueClass_apply_zero {q : ℕ} (a : ZMod q) : residueClass a 0 = 0

theorem ArithmeticFunction.vonMangoldt.abscissaOfAbsConv_residueClass_le_one {q : ℕ} (a : ZMod q) : (LSeries.abscissaOfAbsConv fun (n : ℕ) => ↑(residueClass a n)) ≤ 1

theorem ArithmeticFunction.vonMangoldt.support_residueClass_prime_div {q : ℕ} (a : ZMod q) : (Function.support fun (n : ℕ) => (if Nat.Prime n then residueClass a n else 0) / ↑n) = {p : ℕ | Nat.Prime p ∧ ↑p = a}

The set we are interested in (prime numbers in the residue class a) is the same as the support of ArithmeticFunction.vonMangoldt.residueClass restricted to primes (and divided by n; this is how this result is used later).

theorem ArithmeticFunction.vonMangoldt.summable_residueClass_non_primes_div {q : ℕ} (a : ZMod q) : Summable fun (n : ℕ) => (if Nat.Prime n then 0 else residueClass a n) / ↑n

The function n ↦ Λ n / n, restricted to non-primes in a residue class, is summable. This is used to convert results on ArithmeticFunction.vonMangoldt.residueClass to results on primes in an arithmetic progression.

theorem ArithmeticFunction.vonMangoldt.residueClass_apply {q : ℕ} {a : ZMod q} [NeZero q] (ha : IsUnit a) (n : ℕ) : ↑(residueClass a n) = (↑q.totient)⁻¹ * ∑ χ : DirichletCharacter ℂ q, χ a⁻¹ * χ ↑n * ↑(vonMangoldt n)

We can express ArithmeticFunction.vonMangoldt.residueClass as a linear combination of twists of the von Mangoldt function by Dirichlet characters.

theorem ArithmeticFunction.vonMangoldt.residueClass_eq {q : ℕ} {a : ZMod q} [NeZero q] (ha : IsUnit a) : (fun (n : ℕ) => ↑(residueClass a n)) = (↑q.totient)⁻¹ • ∑ χ : DirichletCharacter ℂ q, χ a⁻¹ • fun (n : ℕ) => χ ↑n * ↑(vonMangoldt n)

We can express ArithmeticFunction.vonMangoldt.residueClass as a linear combination of twists of the von Mangoldt function by Dirichlet characters.

theorem ArithmeticFunction.vonMangoldt.LSeries_residueClass_eq {q : ℕ} {a : ZMod q} [NeZero q] (ha : IsUnit a) {s : ℂ} (hs : 1 < s.re) : LSeries (fun (n : ℕ) => ↑(residueClass a n)) s = -(↑q.totient)⁻¹ * ∑ χ : DirichletCharacter ℂ q, χ a⁻¹ * (deriv (DirichletCharacter.LFunction χ) s / DirichletCharacter.LFunction χ s)

The L-series of the von Mangoldt function restricted to the residue class a mod q with a invertible in ZMod q is a linear combination of logarithmic derivatives of L-functions of the Dirichlet characters mod q (on re s > 1).

@[reducible, inline]

noncomputable abbrev ArithmeticFunction.vonMangoldt.LFunctionResidueClassAux {q : ℕ} (a : ZMod q) [NeZero q] (s : ℂ) : ℂ

The auxiliary function used, e.g., with the Wiener-Ikehara Theorem to prove Dirichlet's Theorem. On re s > 1, it agrees with the L-series of the von Mangoldt function restricted to the residue class a : ZMod q minus the principal part (q.totient)⁻¹/(s-1) of the pole at s = 1; see ArithmeticFunction.vonMangoldt.eqOn_LFunctionResidueClassAux.

Equations

• One or more equations did not get rendered due to their size.

theorem ArithmeticFunction.vonMangoldt.continuousOn_LFunctionResidueClassAux' {q : ℕ} (a : ZMod q) [NeZero q] : ContinuousOn (LFunctionResidueClassAux a) {s : ℂ | s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), DirichletCharacter.LFunction χ s ≠ 0}

The auxiliary function is continuous away from the zeros of the L-functions of the Dirichlet characters mod q (including at s = 1).

theorem ArithmeticFunction.vonMangoldt.continuousOn_LFunctionResidueClassAux {q : ℕ} (a : ZMod q) [NeZero q] : ContinuousOn (LFunctionResidueClassAux a) {s : ℂ | 1 ≤ s.re}

The L-series of the von Mangoldt function restricted to the prime residue class a mod q is continuous on re s ≥ 1 except for a simple pole at s = 1 with residue (q.totient)⁻¹. The statement as given here in terms of ArithmeticFunction.vonMangoldt.LFunctionResidueClassAux is equivalent.

theorem ArithmeticFunction.vonMangoldt.eqOn_LFunctionResidueClassAux {q : ℕ} {a : ZMod q} [NeZero q] (ha : IsUnit a) : Set.EqOn (LFunctionResidueClassAux a) (fun (s : ℂ) => LSeries (fun (n : ℕ) => ↑(residueClass a n)) s - (↑q.totient)⁻¹ / (s - 1)) {s : ℂ | 1 < s.re}

The auxiliary function agrees on re s > 1 with the L-series of the von Mangoldt function restricted to the residue class a : ZMod q minus the principal part (q.totient)⁻¹/(s-1) of its pole at s = 1.

theorem ArithmeticFunction.vonMangoldt.LFunctionResidueClassAux_real {q : ℕ} {a : ZMod q} [NeZero q] (ha : IsUnit a) {x : ℝ} (hx : 1 < x) : LFunctionResidueClassAux a ↑x = ↑(LFunctionResidueClassAux a ↑x).re

The auxiliary function takes real values for real arguments x > 1.

theorem ArithmeticFunction.vonMangoldt.LSeries_residueClass_lower_bound {q : ℕ} [NeZero q] {a : ZMod q} (ha : IsUnit a) : ∃ (C : ℝ), ∀ {x : ℝ}, x ∈ Set.Ioc 1 2 → (↑q.totient)⁻¹ / (x - 1) - C ≤ ∑' (n : ℕ), residueClass a n / ↑n ^ x

As x approaches 1 from the right along the real axis, the L-series of ArithmeticFunction.vonMangoldt.residueClass is bounded below by (q.totient)⁻¹/(x-1) - C.

theorem ArithmeticFunction.vonMangoldt.not_summable_residueClass_prime_div {q : ℕ} [NeZero q] {a : ZMod q} (ha : IsUnit a) : ¬Summable fun (n : ℕ) => (if Nat.Prime n then residueClass a n else 0) / ↑n

The function n ↦ Λ n / n restricted to primes in an invertible residue class is not summable. This then implies that there must be infinitely many such primes.

Dirichlet's Theorem

theorem Nat.setOf_prime_and_eq_mod_infinite {q : ℕ} [NeZero q] {a : ZMod q} (ha : IsUnit a) : {p : ℕ | Prime p ∧ ↑p = a}.Infinite

Dirichlet's Theorem on primes in arithmetic progression: if q is a positive integer and a : ZMod q is a unit, then there are infinitely many prime numbers p such that (p : ZMod q) = a.

theorem Nat.forall_exists_prime_gt_and_eq_mod {q : ℕ} [NeZero q] {a : ZMod q} (ha : IsUnit a) (n : ℕ) : ∃ p > n, Prime p ∧ ↑p = a

Dirichlet's Theorem on primes in arithmetic progression: if q is a positive integer and a : ZMod q is a unit, then there are infinitely many prime numbers p such that (p : ZMod q) = a.