From fe0e8bcc2ddc54118bbd2abdc474dd1d2e3076f3 Mon Sep 17 00:00:00 2001 From: Michael Stoll Date: Fri, 22 Nov 2024 04:40:29 +0000 Subject: [PATCH] feat(NumberTheory/LSeries/PrimesInAP): new file (#19344) This PR creates a new file `Mathlib.NumberTheory.LSeries.PrimesInAP` that will eventually contain a proof of **Dirichlet's Theorem on primes in arithmetic progression**. As a first step, we provide two lemmas on re-writing sums (or products) over a function supported in prime powers. (We also add an API lemma for `Multipliable`/`Summable` that seems to be missing.) See [here](https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/Prerequisites.20for.20PNT.20and.20Dirichlet's.20Thm/near/483714489) on Zulip. --- Mathlib.lean | 1 + Mathlib/NumberTheory/LSeries/PrimesInAP.lean | 67 +++++++++++++++++++ .../Algebra/InfiniteSum/Constructions.lean | 5 ++ 3 files changed, 73 insertions(+) create mode 100644 Mathlib/NumberTheory/LSeries/PrimesInAP.lean diff --git a/Mathlib.lean b/Mathlib.lean index e6b62736993a2..5e0aee1763797 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -3770,6 +3770,7 @@ import Mathlib.NumberTheory.LSeries.Linearity import Mathlib.NumberTheory.LSeries.MellinEqDirichlet import Mathlib.NumberTheory.LSeries.Nonvanishing import Mathlib.NumberTheory.LSeries.Positivity +import Mathlib.NumberTheory.LSeries.PrimesInAP import Mathlib.NumberTheory.LSeries.RiemannZeta import Mathlib.NumberTheory.LSeries.ZMod import Mathlib.NumberTheory.LegendreSymbol.AddCharacter diff --git a/Mathlib/NumberTheory/LSeries/PrimesInAP.lean b/Mathlib/NumberTheory/LSeries/PrimesInAP.lean new file mode 100644 index 0000000000000..0c1fc1a1ebf26 --- /dev/null +++ b/Mathlib/NumberTheory/LSeries/PrimesInAP.lean @@ -0,0 +1,67 @@ +/- +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 + +/-! +# 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. (TODO) Results on the von Mangoldt function restricted to a residue class +3. (TODO) Results on its L-series +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. +-/ + +section auxiliary + +variable {α β γ : Type*} [CommGroup α] [UniformSpace α] [UniformGroup α] [CompleteSpace α] + [T0Space α] + +open Nat.Primes in +@[to_additive tsum_eq_tsum_primes_of_support_subset_prime_powers] +lemma tprod_eq_tprod_primes_of_mulSupport_subset_prime_powers {f : ℕ → α} + (hfm : Multipliable f) (hf : Function.mulSupport f ⊆ {n | IsPrimePow n}) : + ∏' n : ℕ, f n = ∏' (p : Nat.Primes) (k : ℕ), f (p ^ (k + 1)) := by + have hfm' : Multipliable fun pk : Nat.Primes × ℕ ↦ f (pk.fst ^ (pk.snd + 1)) := + prodNatEquiv.symm.multipliable_iff.mp <| by + simpa only [← coe_prodNatEquiv_apply, Prod.eta, Function.comp_def, Equiv.apply_symm_apply] + using hfm.subtype _ + simp only [← tprod_subtype_eq_of_mulSupport_subset hf, Set.coe_setOf, ← prodNatEquiv.tprod_eq, + ← tprod_prod hfm'] + refine tprod_congr fun (p, k) ↦ congrArg f <| coe_prodNatEquiv_apply .. + +@[to_additive tsum_eq_tsum_primes_add_tsum_primes_of_support_subset_prime_powers] +lemma tprod_eq_tprod_primes_mul_tprod_primes_of_mulSupport_subset_prime_powers {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)) := by + rw [tprod_eq_tprod_primes_of_mulSupport_subset_prime_powers hfm hf] + have hfs' (p : Nat.Primes) : Multipliable fun k : ℕ ↦ f (p ^ (k + 1)) := + hfm.comp_injective <| (strictMono_nat_of_lt_succ + fun k ↦ pow_lt_pow_right₀ p.prop.one_lt <| lt_add_one (k + 1)).injective + conv_lhs => + enter [1, p]; rw [tprod_eq_zero_mul (hfs' p), zero_add, pow_one] + enter [2, 1, k]; rw [add_assoc, one_add_one_eq_two] + exact tprod_mul (Multipliable.subtype hfm _) <| + Multipliable.prod (f := fun (pk : Nat.Primes × ℕ) ↦ f (pk.1 ^ (pk.2 + 2))) <| + hfm.comp_injective <| Subtype.val_injective |>.comp + Nat.Primes.prodNatEquiv.injective |>.comp <| + Function.Injective.prodMap (fun ⦃_ _⦄ a ↦ a) <| add_left_injective 1 + +end auxiliary diff --git a/Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean b/Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean index 47d09ed95c689..8b1f1a092440e 100644 --- a/Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean +++ b/Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean @@ -192,6 +192,11 @@ theorem Multipliable.prod_factor {f : β × γ → α} (h : Multipliable f) (b : Multipliable fun c ↦ f (b, c) := h.comp_injective fun _ _ h ↦ (Prod.ext_iff.1 h).2 +@[to_additive Summable.prod] +lemma Multipliable.prod {f : β × γ → α} (h : Multipliable f) : + Multipliable fun b ↦ ∏' c, f (b, c) := + ((Equiv.sigmaEquivProd β γ).multipliable_iff.mpr h).sigma + @[to_additive] lemma HasProd.tprod_fiberwise [T2Space α] {f : β → α} {a : α} (hf : HasProd f a) (g : β → γ) : HasProd (fun c : γ ↦ ∏' b : g ⁻¹' {c}, f b) a :=