refactor(NumberTheory/LSeries): merge QuadraticNonvanishing into `N…

…onvanishing` (#19185)

The proof of non-vanishing of Dirichlet L-functions on `re s = 1` was written in two chunks, since the case of quadratic characters at `s = 1` needs to be handled separately. This PR merges together the two files, and makes one more theorem private since it is superseded by more general results proved later on, rendering the case split in the proof invisible to end-users.

Mathlib.lean

@@ -3754,7 +3754,6 @@ import Mathlib.NumberTheory.LSeries.Linearity
 import Mathlib.NumberTheory.LSeries.MellinEqDirichlet
 import Mathlib.NumberTheory.LSeries.Nonvanishing
 import Mathlib.NumberTheory.LSeries.Positivity
-import Mathlib.NumberTheory.LSeries.QuadraticNonvanishing
 import Mathlib.NumberTheory.LSeries.RiemannZeta
 import Mathlib.NumberTheory.LSeries.ZMod
 import Mathlib.NumberTheory.LegendreSymbol.AddCharacter

Mathlib/NumberTheory/LSeries/Nonvanishing.lean

@@ -1,33 +1,219 @@
 /-
 Copyright (c) 2024 Michael Stoll. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Michael Stoll
+Authors: Michael Stoll, David Loeffler
 -/
 import Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
 import Mathlib.NumberTheory.Harmonic.ZetaAsymp
-import Mathlib.NumberTheory.LSeries.QuadraticNonvanishing
+import Mathlib.NumberTheory.LSeries.Dirichlet
+import Mathlib.NumberTheory.LSeries.DirichletContinuation
+import Mathlib.NumberTheory.LSeries.Positivity
 
 /-!
 # The L-function of a Dirichlet character does not vanish on Re(s) ≥ 1
 
 The main result in this file is `DirichletCharacter.Lfunction_ne_zero_of_one_le_re`:
-if `χ` is a Dirichlet character and `s.re ≥ 1` and either `χ` is nontrivial or `s ≠ 1`,
+if `χ` is a Dirichlet character, `s ∈ ℂ` with `1 ≤ s.re`, and either `χ` is nontrivial or `s ≠ 1`,
 then the L-function of `χ` does not vanish at `s`.
 
 As a consequence, we have the corresponding statement for the Riemann ζ function:
-`riemannZeta_ne_zero_of_one_le_re`.
+`riemannZeta_ne_zero_of_one_le_re` (which does not require `s ≠ 1`, since the junk value at `s = 1`
+happens to be non-zero).
 
 These results are prerequisites for the **Prime Number Theorem** and
 **Dirichlet's Theorem** on primes in arithmetic progressions.
+
+## Outline of proofs
+
+We split into two cases: first, the special case of (non-trivial) quadratic characters at `s = 1`;
+then the remaining case when either `s ≠ 1` or `χ ^ 2 ≠ 1`.
+
+The first case is handled using a positivity argument applied to the series `L χ s * ζ s`: we show
+that this function has non-negative Dirichlet coefficients, is strictly positive for `s ≫ 0`, but
+vanishes at `s = -2`, so it must have a pole somewhere in between.
+
+The second case is dealt with using the product
+`L(χ^0, 1 + x)^3 L(χ, 1 + x + I * y)^4 L(χ^2, 1 + x + 2 * I * y)`, which
+we show has absolute value `≥ 1` for all positive `x` and real `y`; if `L(χ, 1 + I * y) = 0` then
+this product would have to tend to 0 as `x → 0`, which is a contradiction.
+-/
+
+/- NB: Many lemmas (and some defs) in this file are private, since they concern properties of
+hypothetical objects which we eventually deduce cannot exist. We have only made public the lemmas
+whose hypotheses do not turn out to be contradictory.
+-/
+
+open Complex Asymptotics Topology Filter
+open ArithmeticFunction hiding log
+
+-- We use the ordering on `ℂ` given by comparing real parts for fixed imaginary part
+open scoped ComplexOrder
+
+variable {N : ℕ}
+
+namespace DirichletCharacter
+
+section quadratic
+
+/-!
+### Convolution of a Dirichlet character with ζ
+
+We define `DirichletCharacter.zetaMul χ` to be the arithmetic function obtained by
+taking the product (as arithmetic functions = Dirichlet convolution) of the
+arithmetic function `ζ` with `χ`.
+
+We then show that for a quadratic character `χ`, this arithmetic function is multiplicative
+and takes nonnegative real values.
 -/
 
+/-- The complex-valued arithmetic function that is the convolution of the constant
+function `1` with `χ`. -/
+def zetaMul (χ : DirichletCharacter ℂ N) : ArithmeticFunction ℂ :=
+  .zeta * toArithmeticFunction (χ ·)
+
+/-- The arithmetic function `zetaMul χ` is multiplicative. -/
+lemma isMultiplicative_zetaMul (χ : DirichletCharacter ℂ N) : χ.zetaMul.IsMultiplicative :=
+  isMultiplicative_zeta.natCast.mul <| isMultiplicative_toArithmeticFunction χ
+
+lemma LSeriesSummable_zetaMul (χ : DirichletCharacter ℂ N) {s : ℂ} (hs : 1 < s.re) :
+    LSeriesSummable χ.zetaMul s := by
+  refine ArithmeticFunction.LSeriesSummable_mul (LSeriesSummable_zeta_iff.mpr hs) <|
+    LSeriesSummable_of_bounded_of_one_lt_re (m := 1) (fun n hn ↦ ?_) hs
+  simpa only [toArithmeticFunction, coe_mk, hn, ↓reduceIte, ← Complex.norm_eq_abs]
+  using norm_le_one χ _
+
+lemma zetaMul_prime_pow_nonneg {χ : DirichletCharacter ℂ N} (hχ : χ ^ 2 = 1) {p : ℕ}
+    (hp : p.Prime) (k : ℕ) :
+    0 ≤ zetaMul χ (p ^ k) := by
+  simp only [zetaMul, toArithmeticFunction, coe_zeta_mul_apply, coe_mk,
+    Nat.sum_divisors_prime_pow hp, pow_eq_zero_iff', hp.ne_zero, ne_eq, false_and, ↓reduceIte,
+    Nat.cast_pow, map_pow]
+  rcases MulChar.isQuadratic_iff_sq_eq_one.mpr hχ p with h | h | h
+  · refine Finset.sum_nonneg fun i _ ↦ ?_
+    simp only [h, le_refl, pow_nonneg]
+  · refine Finset.sum_nonneg fun i _ ↦ ?_
+    simp only [h, one_pow, zero_le_one]
+  · simp only [h, neg_one_geom_sum]
+    split_ifs
+    exacts [le_rfl, zero_le_one]
+
+/-- `zetaMul χ` takes nonnegative real values when `χ` is a quadratic character. -/
+lemma zetaMul_nonneg {χ : DirichletCharacter ℂ N} (hχ : χ ^ 2 = 1) (n : ℕ) :
+    0 ≤ zetaMul χ n := by
+  rcases eq_or_ne n 0 with rfl | hn
+  · simp only [ArithmeticFunction.map_zero, le_refl]
+  · simpa only [χ.isMultiplicative_zetaMul.multiplicative_factorization _ hn] using
+      Finset.prod_nonneg
+        fun p hp ↦ zetaMul_prime_pow_nonneg hχ (Nat.prime_of_mem_primeFactors hp) _
+
+/-
+### "Bad" Dirichlet characters
+
+Our goal is to show that `L(χ, 1) ≠ 0` when `χ` is a (nontrivial) quadratic Dirichlet character.
+To do that, we package the contradictory properties in a (private) structure
+`DirichletCharacter.BadChar` and derive further statements eventually leading to a contradiction.
+
+This entire section is private.
+-/
+
+/-- The object we're trying to show doesn't exist: A nontrivial quadratic Dirichlet character
+whose L-function vanishes at `s = 1`. -/
+private structure BadChar (N : ℕ) [NeZero N] where
+  /-- The character we want to show cannot exist. -/
+  χ : DirichletCharacter ℂ N
+  χ_ne : χ ≠ 1
+  χ_sq : χ ^ 2 = 1
+  hχ : χ.LFunction 1 = 0
+
+variable [NeZero N]
+
+namespace BadChar
+
+/-- The product of the Riemann zeta function with the L-function of `B.χ`.
+We will show that `B.F (-2) = 0` but also that `B.F (-2)` must be positive,
+giving the desired contradiction. -/
+private noncomputable
+def F (B : BadChar N) : ℂ → ℂ :=
+  Function.update (fun s : ℂ ↦ riemannZeta s * LFunction B.χ s) 1 (deriv (LFunction B.χ) 1)
+
+private lemma F_differentiableAt_of_ne (B : BadChar N) {s : ℂ} (hs : s ≠ 1) :
+    DifferentiableAt ℂ B.F s := by
+  apply DifferentiableAt.congr_of_eventuallyEq
+  · exact (differentiableAt_riemannZeta hs).mul <| differentiableAt_LFunction B.χ s (.inl hs)
+  · filter_upwards [eventually_ne_nhds hs] with t ht using Function.update_noteq ht ..
+
+/-- `B.F` agrees with the L-series of `zetaMul χ` on `1 < s.re`. -/
+private lemma F_eq_LSeries (B : BadChar N) {s : ℂ} (hs : 1 < s.re) :
+    B.F s = LSeries B.χ.zetaMul s := by
+  rw [F, zetaMul, ← coe_mul, LSeries_convolution']
+  · have hs' : s ≠ 1 := fun h ↦ by simp only [h, one_re, lt_self_iff_false] at hs
+    simp only [ne_eq, hs', not_false_eq_true, Function.update_noteq, B.χ.LFunction_eq_LSeries hs]
+    congr 1
+    · simp_rw [← LSeries_zeta_eq_riemannZeta hs, ← natCoe_apply]
+    · exact LSeries_congr s B.χ.apply_eq_toArithmeticFunction_apply
+  -- summability side goals from `LSeries_convolution'`
+  · exact LSeriesSummable_zeta_iff.mpr hs
+  · exact (LSeriesSummable_congr _ fun h ↦ (B.χ.apply_eq_toArithmeticFunction_apply h).symm).mpr <|
+      ZMod.LSeriesSummable_of_one_lt_re B.χ hs
+
+/-- If `χ` is a bad character, then `F` is an entire function. -/
+private lemma F_differentiable (B : BadChar N) : Differentiable ℂ B.F := by
+  intro s
+  rcases ne_or_eq s 1 with hs | rfl
+  · exact B.F_differentiableAt_of_ne hs
+  -- now need to deal with `s = 1`
+  refine (analyticAt_of_differentiable_on_punctured_nhds_of_continuousAt ?_ ?_).differentiableAt
+  · filter_upwards [self_mem_nhdsWithin] with t ht
+    exact B.F_differentiableAt_of_ne ht
+  -- now reduced to showing *continuity* at s = 1
+  let G := Function.update (fun s ↦ (s - 1) * riemannZeta s) 1 1
+  let H := Function.update (fun s ↦ (B.χ.LFunction s - B.χ.LFunction 1) / (s - 1)) 1
+    (deriv B.χ.LFunction 1)
+  have : B.F = G * H := by
+    ext1 t
+    rcases eq_or_ne t 1 with rfl | ht
+    · simp only [F, G, H, Pi.mul_apply, one_mul, Function.update_same]
+    · simp only [F, G, H, Function.update_noteq ht, mul_comm _ (riemannZeta _), B.hχ, sub_zero,
+      Pi.mul_apply, mul_assoc, mul_div_cancel₀ _ (sub_ne_zero.mpr ht)]
+  rw [this]
+  apply ContinuousAt.mul
+  · simpa only [G, continuousAt_update_same] using riemannZeta_residue_one
+  · exact (B.χ.differentiableAt_LFunction 1 (.inr B.χ_ne)).hasDerivAt.continuousAt_div
+
+/-- The trivial zero at `s = -2` of the zeta function gives that `F (-2) = 0`.
+This is used later to obtain a contradction. -/
+private lemma F_neg_two (B : BadChar N) : B.F (-2 : ℝ) = 0 := by
+  have := riemannZeta_neg_two_mul_nat_add_one 0
+  rw [Nat.cast_zero, zero_add, mul_one] at this
+  rw [F, ofReal_neg, ofReal_ofNat, Function.update_noteq (mod_cast (by omega : (-2 : ℤ) ≠ 1)),
+    this, zero_mul]
+
+end BadChar
+
+/-- If `χ` is a nontrivial quadratic Dirichlet character, then `L(χ, 1) ≠ 0`. This is private
+since it is later superseded by `LFunction_apply_one_ne_zero`. -/
+private theorem LFunction_apply_one_ne_zero_of_quadratic {χ : DirichletCharacter ℂ N}
+    (hχ : χ ^ 2 = 1) (χ_ne : χ ≠ 1) :
+    χ.LFunction 1 ≠ 0 := by
+  intro hL
+  -- construct a "bad character" and put together a contradiction.
+  let B : BadChar N := {χ := χ, χ_sq := hχ, hχ := hL, χ_ne := χ_ne}
+  refine B.F_neg_two.not_gt ?_
+  refine ArithmeticFunction.LSeries_positive_of_differentiable_of_eqOn (zetaMul_nonneg hχ)
+    (χ.isMultiplicative_zetaMul.map_one ▸ zero_lt_one) B.F_differentiable ?_
+    (fun _ ↦ B.F_eq_LSeries) _
+  exact LSeries.abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable
+    fun _ a ↦ χ.LSeriesSummable_zetaMul a
+
+end quadratic
+
 section nonvanishing
 
-open Complex
+variable (χ : DirichletCharacter ℂ N)
 
 -- This is the key positivity lemma that is used to show that the L-function
 -- of a Dirichlet character `χ` does not vanish for `s.re ≥ 1` (unless `χ^2 = 1` and `s = 1`).
-private lemma re_log_comb_nonneg {a : ℝ} (ha₀ : 0 ≤ a) (ha₁ : a < 1) {z : ℂ} (hz : ‖z‖ = 1) :
+private lemma re_log_comb_nonneg' {a : ℝ} (ha₀ : 0 ≤ a) (ha₁ : a < 1) {z : ℂ} (hz : ‖z‖ = 1) :
       0 ≤ 3 * (-log (1 - a)).re + 4 * (-log (1 - a * z)).re + (-log (1 - a * z ^ 2)).re := by
   have hac₀ : ‖(a : ℂ)‖ < 1 := by
     simp only [norm_eq_abs, abs_ofReal, _root_.abs_of_nonneg ha₀, ha₁]
@@ -48,10 +234,6 @@ private lemma re_log_comb_nonneg {a : ℝ} (ha₀ : 0 ≤ a) (ha₁ : a < 1) {z
     convert (show 0 ≤ 2 * a ^ n * ((z ^ n).re + 1) ^ 2 by positivity) using 1
     ring
 
-namespace DirichletCharacter
-
-variable {N : ℕ} (χ : DirichletCharacter ℂ N)
-
 -- This is the version of the technical positivity lemma for logarithms of Euler factors.
 private lemma re_log_comb_nonneg {n : ℕ} (hn : 2 ≤ n) {x : ℝ} (hx : 1 < x) (y : ℝ) :
     0 ≤ 3 * (-log (1 - (1 : DirichletCharacter ℂ N) n * n ^ (-x : ℂ))).re +
@@ -68,7 +250,7 @@ private lemma re_log_comb_nonneg {n : ℕ} (hn : 2 ≤ n) {x : ℝ} (hx : 1 < x)
       simp only [neg_re, mul_re, I_re, ofReal_re, zero_mul, I_im, ofReal_im, mul_zero, sub_self,
         neg_zero, Real.rpow_zero, one_mul]
     rw [MulChar.one_apply hn', one_mul]
-    convert _root_.re_log_comb_nonneg ha₀ ha₁ hz using 6
+    convert re_log_comb_nonneg' ha₀ ha₁ hz using 6
     · simp only [ofReal_cpow n.cast_nonneg (-x), ofReal_natCast, ofReal_neg]
     · congr 2
       rw [neg_add, cpow_add _ _ <| mod_cast by omega, ← ofReal_neg, ofReal_cpow n.cast_nonneg (-x),
@@ -96,7 +278,7 @@ private lemma one_lt_re_one_add {x : ℝ} (hx : 0 < x) (y : ℝ) :
 
 open scoped LSeries.notation in
 /-- For positive `x` and nonzero `y` and a Dirichlet character `χ` we have that
-`|L(χ^0, x)^3 L(χ, x+iy)^4 L(χ^2, x+2iy)| ≥ 1. -/
+`|L(χ^0, 1 + x)^3 L(χ, 1 + x + I * y)^4 L(χ^2, 1 + x + 2 * I * y)| ≥ 1. -/
 lemma norm_LSeries_product_ge_one {x : ℝ} (hx : 0 < x) (y : ℝ) :
     ‖L ↗(1 : DirichletCharacter ℂ N) (1 + x) ^ 3 * L ↗χ (1 + x + I * y) ^ 4 *
       L ↗(χ ^ 2 :) (1 + x + 2 * I * y)‖ ≥ 1 := by
@@ -128,9 +310,6 @@ lemma norm_LFunction_product_ge_one {x : ℝ} (hx : 0 < x) (y : ℝ) :
     χ.LFunction_eq_LSeries h₁, (χ ^ 2).LFunction_eq_LSeries h₂]
   exact norm_LSeries_product_ge_one χ hx y
 
-open Asymptotics Topology Filter
-
-open Homeomorph in
 lemma LFunctionTrivChar_isBigO_near_one_horizontal :
     (fun x : ℝ ↦ LFunctionTrivChar N (1 + x)) =O[𝓝[>] 0] fun x ↦ (1 : ℂ) / x := by
   have : (fun w : ℂ ↦ LFunctionTrivChar N (1 + w)) =O[𝓝[≠] 0] (1 / ·) := by
@@ -203,7 +382,7 @@ except when `χ` is trivial and `s = 1` (then `L(χ, s)` has a simple pole at `s
 theorem LFunction_ne_zero_of_re_eq_one {s : ℂ} (hs : s.re = 1) (hχs : χ ≠ 1 ∨ s ≠ 1) :
     LFunction χ s ≠ 0 := by
   by_cases h : χ ^ 2 = 1 ∧ s = 1
-  · exact h.2 ▸ LFunction_at_one_ne_zero_of_quadratic h.1 <| hχs.neg_resolve_right h.2
+  · exact h.2 ▸ LFunction_apply_one_ne_zero_of_quadratic h.1 <| hχs.neg_resolve_right h.2
   · have hs' : s = 1 + I * s.im := by
       conv_lhs => rw [← re_add_im s, hs, ofReal_one, mul_comm]
     rw [not_and_or, ← ne_eq, ← ne_eq, hs', add_right_ne_self] at h
@@ -224,15 +403,14 @@ variable {χ} in
 theorem LFunction_apply_one_ne_zero (hχ : χ ≠ 1) : LFunction χ 1 ≠ 0 :=
   LFunction_ne_zero_of_one_le_re χ (.inl hχ) <| one_re ▸ le_rfl
 
-end DirichletCharacter
-
-open DirichletCharacter in
 /-- The Riemann Zeta Function does not vanish on the closed half-plane `re s ≥ 1`.
 (Note that the value at `s = 1` is a junk value, which happens to be nonzero.) -/
-lemma riemannZeta_ne_zero_of_one_le_re ⦃s : ℂ⦄ (hs : 1 ≤ s.re) :
+lemma _root_.riemannZeta_ne_zero_of_one_le_re ⦃s : ℂ⦄ (hs : 1 ≤ s.re) :
     riemannZeta s ≠ 0 := by
   rcases eq_or_ne s 1 with rfl | hs₀
   · exact riemannZeta_one_ne_zero
   · exact LFunction_modOne_eq (χ := 1) ▸ LFunction_ne_zero_of_one_le_re _ (.inr hs₀) hs
 
 end nonvanishing
+
+end DirichletCharacter