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.

This will be done in the following steps:

1. Some auxiliary lemmas on infinite products and sums
2. Results on the von Mangoldt function restricted to a residue class
3. (TODO) Results on its L-series and an auxiliary function related to it
4. (TODO) Derivation of 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 α] [UniformGroup α] [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 α] [UniformAddGroup α] [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 α] [UniformGroup α] [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 α] [UniformAddGroup α] [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 ≤ ArithmeticFunction.vonMangoldt.residueClass a n

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

@[simp]

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

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

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

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

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

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

theorem ArithmeticFunction.vonMangoldt.LSeries_residueClass_eq {q : ℕ} {a : ZMod q} [NeZero q] (ha : IsUnit a) {s : ℂ} (hs : 1 < s.re) : LSeries (fun (n : ℕ) => ↑(ArithmeticFunction.vonMangoldt.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).