feat(NumberTheory/LSeries/Dirichlet): new file, material on specific …

…L-series (#11712)

This PR adds a new file `NumberTheory.LSeries.Dirichlet` that contains results on L-series of specific functions:
* the Möbius function
* Dirichlet characters, with the constant function `1` as a special case
* the arithmetic function `ζ` (which has the same L-series as the constant function `1`)
* the von Mangoldt function and its twists by Dirichlet characters

It also adds (L-series of zero and of the indicator function of `{1}`) and removes (convergence of the L-series of the constant function `1` / of  `ζ`; this is moved to the new file) some material to/from `NumberTheory.LSeries.Basic`.

See [this thread on Zulip](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/L-series/near/424858837).

Mathlib.lean

@@ -2976,6 +2976,7 @@ import Mathlib.NumberTheory.LSeries.Basic
 import Mathlib.NumberTheory.LSeries.Convergence
 import Mathlib.NumberTheory.LSeries.Convolution
 import Mathlib.NumberTheory.LSeries.Deriv
+import Mathlib.NumberTheory.LSeries.Dirichlet
 import Mathlib.NumberTheory.LSeries.Linearity
 import Mathlib.NumberTheory.LSeries.MellinEqDirichlet
 import Mathlib.NumberTheory.LegendreSymbol.AddCharacter

Mathlib/NumberTheory/Divisors.lean

@@ -132,6 +132,19 @@ theorem mem_divisorsAntidiagonal {x : ℕ × ℕ} :
         Nat.le_mul_of_pos_left _ (Nat.pos_of_ne_zero h.1)⟩
 #align nat.mem_divisors_antidiagonal Nat.mem_divisorsAntidiagonal
 
+lemma ne_zero_of_mem_divisorsAntidiagonal {p : ℕ × ℕ} (hp : p ∈ n.divisorsAntidiagonal) :
+    p.1 ≠ 0 ∧ p.2 ≠ 0 := by
+  obtain ⟨hp₁, hp₂⟩ := Nat.mem_divisorsAntidiagonal.mp hp
+  exact mul_ne_zero_iff.mp (hp₁.symm ▸ hp₂)
+
+lemma left_ne_zero_of_mem_divisorsAntidiagonal {p : ℕ × ℕ} (hp : p ∈ n.divisorsAntidiagonal) :
+    p.1 ≠ 0 :=
+  (ne_zero_of_mem_divisorsAntidiagonal hp).1
+
+lemma right_ne_zero_of_mem_divisorsAntidiagonal {p : ℕ × ℕ} (hp : p ∈ n.divisorsAntidiagonal) :
+    p.2 ≠ 0 :=
+  (ne_zero_of_mem_divisorsAntidiagonal hp).2
+
 -- Porting note: Redundant binder annotation update
 -- variable {n}
 

Mathlib/NumberTheory/LSeries/Basic.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aaron Anderson, Michael Stoll
 -/
 import Mathlib.Analysis.PSeries
-import Mathlib.NumberTheory.ArithmeticFunction
 import Mathlib.Analysis.NormedSpace.FiniteDimension
 
 #align_import number_theory.l_series from "leanprover-community/mathlib"@"32253a1a1071173b33dc7d6a218cf722c6feb514"
@@ -46,11 +45,6 @@ to `N` and `R` coerces to `ℂ`) as arguments to `LSeries` etc.
 ## Tags
 
 L-series
-
-## TODO
-
-* Move `LSeriesSummable.one_iff_one_lt_re` and `zeta_LSeriesSummable_iff_one_lt_r`
-  to a new file on L-series of specific functions
 -/
 
 open scoped BigOperators
@@ -86,7 +80,7 @@ lemma term_of_ne_zero {n : ℕ} (hn : n ≠ 0) (f : ℕ → ℂ) (s : ℂ) :
     term f s n = f n / n ^ s :=
   if_neg hn
 
-lemma term_congr {f g : ℕ → ℂ} (h : ∀ n ≠ 0, f n = g n) (s : ℂ) (n : ℕ) :
+lemma term_congr {f g : ℕ → ℂ} (h : ∀ {n}, n ≠ 0 → f n = g n) (s : ℂ) (n : ℕ) :
     term f s n = term g s n := by
   rcases eq_or_ne n 0 with hn | hn <;> simp [hn, h]
 
@@ -130,7 +124,7 @@ def LSeries (f : ℕ → ℂ) (s : ℂ) : ℂ :=
   ∑' n, term f s n
 #align nat.arithmetic_function.l_series LSeries
 
-lemma LSeries_congr {f g : ℕ → ℂ} (s : ℂ) (h : ∀ n ≠ 0, f n = g n) :
+lemma LSeries_congr {f g : ℕ → ℂ} (s : ℂ) (h : ∀ {n}, n ≠ 0 → f n = g n) :
     LSeries f s = LSeries g s :=
   tsum_congr <| term_congr h s
 
@@ -139,7 +133,7 @@ def LSeriesSummable (f : ℕ → ℂ) (s : ℂ) : Prop :=
   Summable (term f s)
 #align nat.arithmetic_function.l_series_summable LSeriesSummable
 
-lemma LSeriesSummable_congr {f g : ℕ → ℂ} (s : ℂ) (h : ∀ n ≠ 0, f n = g n) :
+lemma LSeriesSummable_congr {f g : ℕ → ℂ} (s : ℂ) (h : ∀ {n}, n ≠ 0 → f n = g n) :
     LSeriesSummable f s ↔ LSeriesSummable g s :=
   summable_congr <| term_congr h s
 
@@ -197,7 +191,7 @@ lemma LSeriesHasSum_iff {f : ℕ → ℂ} {s a : ℂ} :
     LSeriesHasSum f s a ↔ LSeriesSummable f s ∧ LSeries f s = a :=
   ⟨fun H ↦ ⟨H.LSeriesSummable, H.LSeries_eq⟩, fun ⟨H₁, H₂⟩ ↦ H₂ ▸ H₁.LSeriesHasSum⟩
 
-lemma LSeriesHasSum_congr {f g : ℕ → ℂ} (s a : ℂ) (h : ∀ n ≠ 0, f n = g n) :
+lemma LSeriesHasSum_congr {f g : ℕ → ℂ} (s a : ℂ) (h : ∀ {n}, n ≠ 0 → f n = g n) :
     LSeriesHasSum f s a ↔ LSeriesHasSum g s a := by
   simp only [LSeriesHasSum_iff, LSeriesSummable_congr s h, LSeries_congr s h]
 
@@ -211,6 +205,9 @@ theorem LSeriesSummable_iff_of_re_eq_re {f : ℕ → ℂ} {s s' : ℂ} (h : s.re
   ⟨fun H ↦ H.of_re_le_re h.le, fun H ↦ H.of_re_le_re h.symm.le⟩
 #align nat.arithmetic_function.l_series_summable_iff_of_re_eq_re LSeriesSummable_iff_of_re_eq_re
 
+/-- The indicator function of `{1} ⊆ ℕ` with values in `ℂ`. -/
+def LSeries.delta (n : ℕ) : ℂ :=
+  if n = 1 then 1 else 0
 
 /-!
 ### Notation
@@ -226,6 +223,57 @@ or `↗f` when `f : ArithmeticFunction R` or simply `f : N → R` with a coercio
 as an argument to `LSeries`, `LSeriesHasSum`, `LSeriesSummable` etc. -/
 scoped[LSeries.notation] notation:max "↗" f:max => fun n : ℕ ↦ (f n : ℂ)
 
+@[inherit_doc]
+scoped[LSeries.notation] notation "δ" => delta
+
+/-!
+### LSeries of 0 and δ
+-/
+
+@[simp]
+lemma LSeries_zero : LSeries 0 = 0 := by
+  ext
+  simp only [LSeries, LSeries.term, Pi.zero_apply, zero_div, ite_self, tsum_zero]
+
+section delta
+
+open scoped LSeries.notation
+
+namespace LSeries
+
+open Nat Complex
+
+lemma term_delta (s : ℂ) (n : ℕ) : term δ s n = if n = 1 then 1 else 0 := by
+  rcases eq_or_ne n 0 with rfl | hn
+  · simp only [term_zero, zero_ne_one, ↓reduceIte]
+  · simp only [ne_eq, hn, not_false_eq_true, term_of_ne_zero, delta]
+    rcases eq_or_ne n 1 with rfl | hn'
+    · simp only [↓reduceIte, cast_one, one_cpow, ne_eq, one_ne_zero, not_false_eq_true, div_self]
+    · simp only [hn', ↓reduceIte, zero_div]
+
+lemma mul_delta_eq_smul_delta {f : ℕ → ℂ} : f * δ = f 1 • δ := by
+  ext n
+  simp only [Pi.mul_apply, delta, mul_ite, mul_one, mul_zero, Pi.smul_apply, smul_eq_mul]
+  split_ifs with hn <;> simp only [hn]
+
+lemma mul_delta {f : ℕ → ℂ} (h : f 1 = 1) : f * δ = δ := by
+  rw [mul_delta_eq_smul_delta, h, one_smul]
+
+lemma delta_mul_eq_smul_delta {f : ℕ → ℂ} : δ * f = f 1 • δ :=
+  mul_comm δ f ▸ mul_delta_eq_smul_delta
+
+lemma delta_mul {f : ℕ → ℂ} (h : f 1 = 1) : δ * f = δ :=
+  mul_comm δ f ▸ mul_delta h
+
+end LSeries
+
+/-- The L-series of `δ` is the constant function `1`. -/
+lemma LSeries_delta : LSeries δ = 1 := by
+  ext
+  simp only [LSeries, LSeries.term_delta, tsum_ite_eq, Pi.one_apply]
+
+end delta
+
 
 /-!
 ### Criteria for and consequences of summability of L-series
@@ -322,26 +370,3 @@ theorem LSeriesSummable_of_bounded_of_one_lt_real {f : ℕ → ℂ} {m : ℝ}
     LSeriesSummable f s :=
   LSeriesSummable_of_bounded_of_one_lt_re h <| by simp only [ofReal_re, hs]
 #align nat.arithmetic_function.l_series_summable_of_bounded_of_one_lt_real LSeriesSummable_of_bounded_of_one_lt_real
-
--- TODO: Move this to a separate file on concrete L-series
-
-open Set in
-/-- The `LSeries` with all coefficients `1` converges at `s` if and only if `re s > 1`. -/
-theorem LSeriesSummable.one_iff_one_lt_re {s : ℂ} : LSeriesSummable 1 s ↔ 1 < s.re := by
-  rw [← LSeriesSummable_iff_of_re_eq_re (Complex.ofReal_re s.re), LSeriesSummable,
-    ← summable_norm_iff, ← Real.summable_one_div_nat_rpow]
-  simp_rw [← Finite.summable_compl_iff (finite_singleton 0), summable_subtype_iff_indicator]
-  refine summable_congr fun n ↦ ?_
-  by_cases hn : n ∈ ({0}ᶜ :Set ℕ)
-  · simp only [indicator_of_mem hn, norm_term_eq]
-    simp only [show n ≠ 0 from hn, ↓reduceIte, Pi.one_apply, norm_one, ofReal_re]
-  · simp only [indicator_of_not_mem hn]
-
-open scoped ArithmeticFunction in
-/-- The `LSeries` associated to the arithmetic function `ζ` converges at `s` if and only if
-`re s > 1`. -/
-theorem zeta_LSeriesSummable_iff_one_lt_re {s : ℂ} : LSeriesSummable (ζ ·) s ↔ 1 < s.re := by
-  have (n : ℕ) (hn : n ≠ 0) : ζ n = (1 : ℕ → ℂ) n := by
-    simp only [ArithmeticFunction.zeta_apply, hn, ↓reduceIte, Nat.cast_one, Pi.one_apply]
-  exact (LSeriesSummable_congr s this).trans <| LSeriesSummable.one_iff_one_lt_re
-#align nat.arithmetic_function.zeta_l_series_summable_iff_one_lt_re zeta_LSeriesSummable_iff_one_lt_re

Mathlib/NumberTheory/LSeries/Convergence.lean

@@ -26,7 +26,7 @@ when `re s < x`. -/
 noncomputable def LSeries.abscissaOfAbsConv (f : ℕ → ℂ) : EReal :=
   sInf <| Real.toEReal '' {x : ℝ | LSeriesSummable f x}
 
-lemma LSeries.abscissaOfAbsConv_congr {f g : ℕ → ℂ} (h : ∀ n ≠ 0, f n = g n) :
+lemma LSeries.abscissaOfAbsConv_congr {f g : ℕ → ℂ} (h : ∀ {n}, n ≠ 0 → f n = g n) :
     abscissaOfAbsConv f = abscissaOfAbsConv g :=
   congr_arg sInf <| congr_arg _ <| Set.ext fun x ↦ LSeriesSummable_congr x h
 

Mathlib/NumberTheory/LSeries/Convolution.lean

@@ -4,8 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Michael Stoll
 -/
 import Mathlib.Analysis.InnerProductSpace.Basic
-import Mathlib.NumberTheory.LSeries.Convergence
 import Mathlib.Analysis.Normed.Field.InfiniteSum
+import Mathlib.NumberTheory.ArithmeticFunction
+import Mathlib.NumberTheory.LSeries.Convergence
 
 /-!
 # Dirichlet convolution of sequences and products of L-series
@@ -28,14 +29,22 @@ open Complex LSeries
 ### Dirichlet convolution of two functions
 -/
 
-open BigOperators
+open BigOperators Nat
 
 /-- We turn any function `ℕ → R` into an `ArithmeticFunction R` by setting its value at `0`
 to be zero. -/
 def toArithmeticFunction {R : Type*} [Zero R] (f : ℕ → R) : ArithmeticFunction R where
   toFun n := if n = 0 then 0 else f n
   map_zero' := rfl
 
+lemma toArithmeticFunction_congr {R : Type*} [Zero R] {f f' : ℕ → R}
+    (h : ∀ {n}, n ≠ 0 → f n = f' n) :
+    toArithmeticFunction f = toArithmeticFunction f' := by
+  ext ⟨- | _⟩
+  · simp only [zero_eq, ArithmeticFunction.map_zero]
+  · simp only [toArithmeticFunction, ArithmeticFunction.coe_mk, succ_ne_zero, ↓reduceIte,
+      ne_eq, not_false_eq_true, h]
+
 /-- If we consider an arithmetic function just as a function and turn it back into an
 arithmetic function, it is the same as before. -/
 @[simp]
@@ -54,6 +63,11 @@ noncomputable def LSeries.convolution {R : Type*} [Semiring R] (f g : ℕ → R)
 @[inherit_doc]
 scoped[LSeries.notation] infixl:70 " ⍟ " => LSeries.convolution
 
+lemma LSeries.convolution_congr {R : Type*} [Semiring R] {f f' g g' : ℕ → R}
+    (hf : ∀ {n}, n ≠ 0 → f n = f' n) (hg : ∀ {n}, n ≠ 0 → g n = g' n) :
+    f ⍟ g = f' ⍟ g' := by
+  simp only [convolution, toArithmeticFunction_congr hf, toArithmeticFunction_congr hg]
+
 /-- The product of two arithmetic functions defines the same function as the Dirichlet convolution
 of the functions defined by them. -/
 lemma ArithmeticFunction.coe_mul {R : Type*} [Semiring R] (f g : ArithmeticFunction R) :
@@ -68,13 +82,12 @@ lemma convolution_def {R : Type*} [Semiring R] (f g : ℕ → R) :
   simp only [convolution, toArithmeticFunction, ArithmeticFunction.mul_apply,
     ArithmeticFunction.coe_mk, mul_ite, mul_zero, ite_mul, zero_mul]
   refine Finset.sum_congr rfl fun p hp ↦ ?_
-  obtain ⟨hp₁, hp₂⟩ := Nat.mem_divisorsAntidiagonal.mp hp
-  obtain ⟨h₁, h₂⟩ := mul_ne_zero_iff.mp (hp₁.symm ▸ hp₂)
+  obtain ⟨h₁, h₂⟩ := ne_zero_of_mem_divisorsAntidiagonal hp
   simp only [h₂, ↓reduceIte, h₁]
 
 @[simp]
 lemma convolution_map_zero {R : Type*} [Semiring R] (f g : ℕ → R) : (f ⍟ g) 0 = 0 := by
-  simp only [convolution_def, Nat.divisorsAntidiagonal_zero, Finset.sum_empty]
+  simp only [convolution_def, divisorsAntidiagonal_zero, Finset.sum_empty]
 
 
 /-!
@@ -86,14 +99,13 @@ in terms of a sum over `Nat.divisorsAntidiagonal`. -/
 lemma term_convolution (f g : ℕ → ℂ) (s : ℂ) (n : ℕ) :
     term (f ⍟ g) s n = ∑ p in n.divisorsAntidiagonal, term f s p.1 * term g s p.2 := by
   rcases eq_or_ne n 0 with rfl | hn
-  · simp only [term_zero, Nat.divisorsAntidiagonal_zero, Finset.sum_empty]
+  · simp only [term_zero, divisorsAntidiagonal_zero, Finset.sum_empty]
   -- now `n ≠ 0`
   rw [term_of_ne_zero hn, convolution_def, Finset.sum_div]
   refine Finset.sum_congr rfl fun p hp ↦ ?_
-  obtain ⟨hp, hn₀⟩ := Nat.mem_divisorsAntidiagonal.mp hp
-  have ⟨hp₁, hp₂⟩ := mul_ne_zero_iff.mp <| hp.symm ▸ hn₀
-  rw [term_of_ne_zero hp₁ f s, term_of_ne_zero hp₂ g s, mul_comm_div, div_div,
-    ← mul_div_assoc, ← natCast_mul_natCast_cpow, ← Nat.cast_mul, mul_comm p.2, hp]
+  have ⟨hp₁, hp₂⟩ := ne_zero_of_mem_divisorsAntidiagonal hp
+  rw [term_of_ne_zero hp₁ f s, term_of_ne_zero hp₂ g s, mul_comm_div, div_div, ← mul_div_assoc,
+    ← natCast_mul_natCast_cpow, ← cast_mul, mul_comm p.2, (mem_divisorsAntidiagonal.mp hp).1]
 
 open Set in
 /-- We give an expression of the `LSeries.term` of the convolution of two functions
@@ -110,7 +122,7 @@ lemma term_convolution' (f g : ℕ → ℂ) (s : ℂ) :
     -- the right hand sum is over the union below, but in each term, one factor is always zero
     have hS : (fun p ↦ p.1 * p.2) ⁻¹' {0} = {0} ×ˢ univ ∪ univ ×ˢ {0} := by
       ext
-      simp only [mem_preimage, mem_singleton_iff, mul_eq_zero, mem_union, mem_prod, mem_univ,
+      simp only [mem_preimage, mem_singleton_iff, Nat.mul_eq_zero, mem_union, mem_prod, mem_univ,
         and_true, true_and]
     have : ∀ p : (fun p : ℕ × ℕ ↦ p.1 * p.2) ⁻¹' {0}, term f s p.val.1 * term g s p.val.2 = 0 := by
       rintro ⟨⟨p₁, p₂⟩, hp⟩