From 09a053e649888befa819426d00878d7f3aaca830 Mon Sep 17 00:00:00 2001 From: Michael Stoll Date: Sat, 23 Nov 2024 13:04:00 +0000 Subject: [PATCH] feat(NumberTheory/LSeries/PrimesInAP): von Mangoldt restricted to a residue class (#19368) This is the next step on the way to **Dirichlet's Theorem**. It defines `ArithmeticFunction.vonMangoldt.residueClass` as the function that is the von Mangoldt function on a given residue class and zero outside and proves some facts about it (in particular that it is a linear combination of twists of the von Mangoldt function by Dirichlet characters). See [here](https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/Prerequisites.20for.20PNT.20and.20Dirichlet's.20Thm/near/483785853) on Zulip. The large import increase is caused by the need for more material to be able to state and prove the new things. --- Mathlib/NumberTheory/LSeries/PrimesInAP.lean | 94 ++++++++++++++++++-- 1 file changed, 89 insertions(+), 5 deletions(-) diff --git a/Mathlib/NumberTheory/LSeries/PrimesInAP.lean b/Mathlib/NumberTheory/LSeries/PrimesInAP.lean index 0c1fc1a1ebf26..0740c4659750a 100644 --- a/Mathlib/NumberTheory/LSeries/PrimesInAP.lean +++ b/Mathlib/NumberTheory/LSeries/PrimesInAP.lean @@ -3,9 +3,10 @@ Copyright (c) 2024 Michael Stoll. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Michael Stoll -/ -import Mathlib.Data.Nat.Factorization.PrimePow -import Mathlib.Topology.Algebra.InfiniteSum.Constructions -import Mathlib.Topology.Algebra.InfiniteSum.NatInt +import Mathlib.NumberTheory.DirichletCharacter.Orthogonality +import Mathlib.NumberTheory.LSeries.DirichletContinuation +import Mathlib.NumberTheory.LSeries.Linearity +import Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed /-! # Dirichlet's Theorem on primes in arithmetic progression @@ -17,8 +18,8 @@ and `a : ZMod q` is invertible, then there are infinitely many prime numbers `p` This will be done in the following steps: 1. Some auxiliary lemmas on infinite products and sums -2. (TODO) Results on the von Mangoldt function restricted to a residue class -3. (TODO) Results on its L-series +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 -/ @@ -65,3 +66,86 @@ lemma tprod_eq_tprod_primes_mul_tprod_primes_of_mulSupport_subset_prime_powers { Function.Injective.prodMap (fun ⦃_ _⦄ a ↦ a) <| add_left_injective 1 end auxiliary + +/-! +### The L-series of the von Mangoldt function restricted to a residue class +-/ + +section arith_prog + +namespace ArithmeticFunction.vonMangoldt + +open Complex LSeries DirichletCharacter + +open scoped LSeries.notation + +variable {q : ℕ} (a : ZMod q) + +/-- The von Mangoldt function restricted to the residue class `a` mod `q`. -/ +noncomputable abbrev residueClass : ℕ → ℝ := + {n : ℕ | (n : ZMod q) = a}.indicator (vonMangoldt ·) + +lemma residueClass_nonneg (n : ℕ) : 0 ≤ residueClass a n := + Set.indicator_apply_nonneg fun _ ↦ vonMangoldt_nonneg + +lemma residueClass_le (n : ℕ) : residueClass a n ≤ vonMangoldt n := + Set.indicator_apply_le' (fun _ ↦ le_rfl) (fun _ ↦ vonMangoldt_nonneg) + +@[simp] +lemma residueClass_apply_zero : residueClass a 0 = 0 := by + simp only [Set.indicator_apply_eq_zero, Set.mem_setOf_eq, Nat.cast_zero, map_zero, ofReal_zero, + implies_true] + +lemma abscissaOfAbsConv_residueClass_le_one : + abscissaOfAbsConv ↗(residueClass a) ≤ 1 := by + refine abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable fun y hy ↦ ?_ + unfold LSeriesSummable + have := LSeriesSummable_vonMangoldt <| show 1 < (y : ℂ).re by simp only [ofReal_re, hy] + convert this.indicator {n : ℕ | (n : ZMod q) = a} + ext1 n + by_cases hn : (n : ZMod q) = a + · simp +contextual only [term, Set.indicator, Set.mem_setOf_eq, hn, ↓reduceIte, apply_ite, + ite_self] + · simp +contextual only [term, Set.mem_setOf_eq, hn, not_false_eq_true, Set.indicator_of_not_mem, + ofReal_zero, zero_div, ite_self] + +variable [NeZero q] {a} + +/-- We can express `ArithmeticFunction.vonMangoldt.residueClass` as a linear combination +of twists of the von Mangoldt function with Dirichlet charaters. -/ +lemma residueClass_apply (ha : IsUnit a) (n : ℕ) : + residueClass a n = + (q.totient : ℂ)⁻¹ * ∑ χ : DirichletCharacter ℂ q, χ a⁻¹ * χ n * vonMangoldt n := by + rw [eq_inv_mul_iff_mul_eq₀ <| mod_cast (Nat.totient_pos.mpr q.pos_of_neZero).ne'] + simp +contextual only [residueClass, Set.indicator_apply, Set.mem_setOf_eq, apply_ite, + ofReal_zero, mul_zero, ← Finset.sum_mul, sum_char_inv_mul_char_eq ℂ ha n, eq_comm (a := a), + ite_mul, zero_mul, ↓reduceIte, ite_self] + +/-- We can express `ArithmeticFunction.vonMangoldt.residueClass` as a linear combination +of twists of the von Mangoldt function with Dirichlet charaters. -/ +lemma residueClass_eq (ha : IsUnit a) : + ↗(residueClass a) = (q.totient : ℂ)⁻¹ • + ∑ χ : DirichletCharacter ℂ q, χ a⁻¹ • (fun n : ℕ ↦ χ n * vonMangoldt n) := by + ext1 n + simpa only [Pi.smul_apply, Finset.sum_apply, smul_eq_mul, ← mul_assoc] + using residueClass_apply ha n + +/-- 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`). -/ +lemma LSeries_residueClass_eq (ha : IsUnit a) {s : ℂ} (hs : 1 < s.re) : + LSeries ↗(residueClass a) s = + -(q.totient : ℂ)⁻¹ * ∑ χ : DirichletCharacter ℂ q, χ a⁻¹ * + (deriv (LFunction χ) s / LFunction χ s) := by + simp only [deriv_LFunction_eq_deriv_LSeries _ hs, LFunction_eq_LSeries _ hs, neg_mul, ← mul_neg, + ← Finset.sum_neg_distrib, ← neg_div, ← LSeries_twist_vonMangoldt_eq _ hs] + rw [eq_inv_mul_iff_mul_eq₀ <| mod_cast (Nat.totient_pos.mpr q.pos_of_neZero).ne'] + simp_rw [← LSeries_smul, + ← LSeries_sum <| fun χ _ ↦ (LSeriesSummable_twist_vonMangoldt χ hs).smul _] + refine LSeries_congr s fun {n} _ ↦ ?_ + simp only [Pi.smul_apply, residueClass_apply ha, smul_eq_mul, ← mul_assoc, + mul_inv_cancel_of_invertible, one_mul, Finset.sum_apply, Pi.mul_apply] + +end ArithmeticFunction.vonMangoldt + +end arith_prog