feat(NumberTheory/LSeries): completed L-functions (#16894)

Define the completed L-function for a function on `ZMod N`, and prove its functional equation.

Mathlib/NumberTheory/LSeries/ZMod.lean

@@ -12,7 +12,10 @@ import Mathlib.NumberTheory.LSeries.RiemannZeta
 # L-series of functions on `ZMod N`
 
 We show that if `N` is a positive integer and `Φ : ZMod N → ℂ`, then the L-series of `Φ` has
-analytic continuation (away from a pole at `s = 1` if `∑ j, Φ j ≠ 0`).
+analytic continuation (away from a pole at `s = 1` if `∑ j, Φ j ≠ 0`) and satisfies a functional
+equation. We also define completed L-functions (given by multiplying the naive L-function by a
+Gamma-factor), and prove analytic continuation and functional equations for these too, assuming `Φ`
+is either even or odd.
 
 The most familiar case is when `Φ` is a Dirichlet character, but the results here are valid
 for general functions; for the specific case of Dirichlet characters see
@@ -21,15 +24,35 @@ for general functions; for the specific case of Dirichlet characters see
 ## Main definitions
 
 * `ZMod.LFunction Φ s`: the meromorphic continuation of the function `∑ n : ℕ, Φ n * n ^ (-s)`.
+* `ZMod.completedLFunction Φ s`: the completed L-function, which for *almost* all `s` is equal to
+  `LFunction Φ s` multiplied by an Archimedean Gamma-factor.
+
+Note that `ZMod.completedLFunction Φ s` is only mathematically well-defined if `Φ` is either even
+or odd. Here we extend it to all functions `Φ` by linearity  (but the functional equation only holds
+if `Φ` is either even or odd).
 
 ## Main theorems
 
+Results for non-completed L-functions:
+
 * `ZMod.LFunction_eq_LSeries`: if `1 < re s` then the `LFunction` coincides with the naive
   `LSeries`.
 * `ZMod.differentiableAt_LFunction`: `ZMod.LFunction Φ` is differentiable at `s ∈ ℂ` if either
   `s ≠ 1` or `∑ j, Φ j = 0`.
 * `ZMod.LFunction_one_sub`: the functional equation relating `LFunction Φ (1 - s)` to
   `LFunction (𝓕 Φ) s`, where `𝓕` is the Fourier transform.
+
+Results for completed L-functions:
+
+* `ZMod.LFunction_eq_completed_div_gammaFactor_even` and
+  `LFunction_eq_completed_div_gammaFactor_odd`: we have
+  `LFunction Φ s = completedLFunction Φ s / Gammaℝ s` for `Φ` even, and
+  `LFunction Φ s = completedLFunction Φ s / Gammaℝ (s + 1)` for `Φ` odd. (We formulate it this way
+  around so it is still valid at the poles of the Gamma factor.)
+* `ZMod.differentiableAt_completedLFunction`: `ZMod.completedLFunction Φ` is differentiable at
+  `s ∈ ℂ`, unless `s = 1` and `∑ j, Φ j ≠ 0`, or `s = 0` and `Φ 0 ≠ 0`.
+* `ZMod.completedLFunction_one_sub_even` and `ZMod.completedLFunction_one_sub_odd`:
+  the functional equation relating `completedLFunction Φ (1 - s)` to `completedLFunction (𝓕 Φ) s`.
 -/
 
 open HurwitzZeta Complex ZMod Finset Classical Topology Filter Set
@@ -219,4 +242,279 @@ theorem LFunction_one_sub (Φ : ZMod N → ℂ) {s : ℂ}
   simp_rw [neg_neg, mul_sum, ← sum_add_distrib, ← mul_assoc, mul_comm _ (Φ _), mul_assoc,
     ← mul_add, map_neg, add_comm]
 
+section signed
+
+variable {Φ : ZMod N → ℂ}
+
+lemma LFunction_def_even (hΦ : Φ.Even) (s : ℂ) :
+    LFunction Φ s = N ^ (-s) * ∑ j : ZMod N, Φ j * hurwitzZetaEven (toAddCircle j) s := by
+  simp only [LFunction, hurwitzZeta, mul_add (Φ _), sum_add_distrib]
+  congr 1
+  simp only [add_right_eq_self, ← neg_eq_self ℂ, ← sum_neg_distrib]
+  refine Fintype.sum_equiv (.neg _) _ _ fun i ↦ ?_
+  simp only [Equiv.neg_apply, hΦ i, map_neg, hurwitzZetaOdd_neg, mul_neg]
+
+lemma LFunction_def_odd (hΦ : Φ.Odd) (s : ℂ) :
+    LFunction Φ s = N ^ (-s) * ∑ j : ZMod N, Φ j * hurwitzZetaOdd (toAddCircle j) s := by
+  simp only [LFunction, hurwitzZeta, mul_add (Φ _), sum_add_distrib]
+  congr 1
+  simp only [add_left_eq_self, ← neg_eq_self ℂ, ← sum_neg_distrib]
+  refine Fintype.sum_equiv (.neg _) _ _ fun i ↦ ?_
+  simp only [Equiv.neg_apply, hΦ i, map_neg, hurwitzZetaEven_neg, neg_mul]
+
+/-- Explicit formula for `LFunction Φ 0` when `Φ` is even. -/
+@[simp] lemma LFunction_apply_zero_of_even (hΦ : Φ.Even) :
+    LFunction Φ 0 = -Φ 0 / 2 := by
+  simp only [LFunction_def_even hΦ, neg_zero, cpow_zero, hurwitzZetaEven_apply_zero,
+    toAddCircle_eq_zero, mul_ite, mul_div, mul_neg_one, mul_zero, sum_ite_eq', Finset.mem_univ,
+    ↓reduceIte, one_mul]
+
+/-- The L-function of an even function vanishes at negative even integers. -/
+@[simp] lemma LFunction_neg_two_mul_nat_add_one (hΦ : Φ.Even) (n : ℕ) :
+    LFunction Φ (-(2 * (n + 1))) = 0 := by
+  simp only [LFunction_def_even hΦ, hurwitzZetaEven_neg_two_mul_nat_add_one, mul_zero,
+    sum_const_zero, ← neg_mul]
+
+/-- The L-function of an odd function vanishes at negative odd integers. -/
+@[simp] lemma LFunction_neg_two_mul_nat_sub_one (hΦ : Φ.Odd) (n : ℕ) :
+    LFunction Φ (-(2 * n) - 1) = 0 := by
+  simp only [LFunction_def_odd hΦ, hurwitzZetaOdd_neg_two_mul_nat_sub_one, mul_zero, ← neg_mul,
+    sum_const_zero]
+
+/--
+The completed L-function of a function `Φ : ZMod N → ℂ`.
+
+This is only mathematically meaningful if `Φ` is either even, or odd; here we extend this to all `Φ`
+by linearity.
+-/
+noncomputable def completedLFunction (Φ : ZMod N → ℂ) (s : ℂ) : ℂ :=
+  N ^ (-s) * ∑ j, Φ j * completedHurwitzZetaEven (toAddCircle j) s
+  + N ^ (-s) * ∑ j, Φ j * completedHurwitzZetaOdd (toAddCircle j) s
+
+@[simp] lemma completedLFunction_zero (s : ℂ) : completedLFunction (0 : ZMod N → ℂ) s = 0 := by
+  simp only [completedLFunction, Pi.zero_apply, zero_mul, sum_const_zero, mul_zero, zero_add]
+
+lemma completedLFunction_def_even (hΦ : Φ.Even) (s : ℂ) :
+    completedLFunction Φ s = N ^ (-s) * ∑ j, Φ j * completedHurwitzZetaEven (toAddCircle j) s := by
+  suffices ∑ j, Φ j * completedHurwitzZetaOdd (toAddCircle j) s = 0 by
+    rw [completedLFunction, this, mul_zero, add_zero]
+  refine (hΦ.mul_odd fun j ↦ ?_).sum_eq_zero
+  rw [map_neg, completedHurwitzZetaOdd_neg]
+
+lemma completedLFunction_def_odd (hΦ : Φ.Odd) (s : ℂ) :
+    completedLFunction Φ s = N ^ (-s) * ∑ j, Φ j * completedHurwitzZetaOdd (toAddCircle j) s := by
+  suffices ∑ j, Φ j * completedHurwitzZetaEven (toAddCircle j) s = 0 by
+    rw [completedLFunction, this, mul_zero, zero_add]
+  refine (hΦ.mul_even fun j ↦ ?_).sum_eq_zero
+  rw [map_neg, completedHurwitzZetaEven_neg]
+
+/--
+The completed L-function of a function `ZMod 1 → ℂ` is a scalar multiple of the completed Riemann
+zeta function.
+-/
+lemma completedLFunction_modOne_eq (Φ : ZMod 1 → ℂ) (s : ℂ) :
+    completedLFunction Φ s = Φ 1 * completedRiemannZeta s := by
+  rw [completedLFunction_def_even (show Φ.Even from fun _ ↦ congr_arg Φ (Subsingleton.elim ..)),
+    Nat.cast_one, one_cpow, one_mul, ← singleton_eq_univ 0, sum_singleton, map_zero,
+    completedHurwitzZetaEven_zero, Subsingleton.elim 0 1]
+
+/--
+The completed L-function of a function `ZMod N → ℂ`, modified by adding multiples of `N ^ (-s) / s`
+and `N ^ (-s) / (1 - s)` to make it entire.
+-/
+noncomputable def completedLFunction₀ (Φ : ZMod N → ℂ) (s : ℂ) : ℂ :=
+  N ^ (-s) * ∑ j : ZMod N, Φ j * completedHurwitzZetaEven₀ (toAddCircle j) s
+  + N ^ (-s) * ∑ j : ZMod N, Φ j * completedHurwitzZetaOdd (toAddCircle j) s
+
+/-- The function `completedLFunction₀ Φ` is differentiable. -/
+lemma differentiable_completedLFunction₀ (Φ : ZMod N → ℂ) :
+    Differentiable ℂ (completedLFunction₀ Φ) := by
+  refine .add ?_ ?_ <;>
+  refine (differentiable_neg.const_cpow <| .inl <| NeZero.ne _).mul (.sum fun i _ ↦ .const_mul ?_ _)
+  exacts [differentiable_completedHurwitzZetaEven₀ _, differentiable_completedHurwitzZetaOdd _]
+
+lemma completedLFunction_eq (Φ : ZMod N → ℂ) (s : ℂ) :
+    completedLFunction Φ s =
+      completedLFunction₀ Φ s - N ^ (-s) * Φ 0 / s - N ^ (-s) * (∑ j, Φ j) / (1 - s) := by
+  simp only [completedLFunction, completedHurwitzZetaEven_eq, toAddCircle_eq_zero, div_eq_mul_inv,
+    ite_mul, one_mul, zero_mul, mul_sub, mul_ite, mul_zero, sum_sub_distrib, Fintype.sum_ite_eq',
+    ← sum_mul, completedLFunction₀, mul_assoc]
+  abel
+
+/--
+The completed L-function of a function `ZMod N → ℂ` is differentiable, with the following
+exceptions: at `s = 1` if `∑ j, Φ j ≠ 0`; and at `s = 0` if `Φ 0 ≠ 0`.
+-/
+lemma differentiableAt_completedLFunction (Φ : ZMod N → ℂ) (s : ℂ) (hs₀ : s ≠ 0 ∨ Φ 0 = 0)
+    (hs₁ : s ≠ 1 ∨ ∑ j, Φ j = 0) : DifferentiableAt ℂ (completedLFunction Φ) s := by
+  simp only [funext (completedLFunction_eq Φ), mul_div_assoc]
+  -- We know `completedLFunction₀` is differentiable everywhere, so it suffices to show that the
+  -- correction terms from `completedLFunction_eq` are differentiable at `s`.
+  refine ((differentiable_completedLFunction₀ _ _).sub ?_).sub ?_
+  · -- term with `1 / s`
+    refine ((differentiable_neg.const_cpow <| .inl <| NeZero.ne _) s).mul (hs₀.elim ?_ ?_)
+    · exact fun h ↦ (differentiableAt_const _).div differentiableAt_id h
+    · exact fun h ↦ by simp only [h, funext zero_div, differentiableAt_const]
+  · -- term with `1 / (1 - s)`
+    refine ((differentiable_neg.const_cpow <| .inl <| NeZero.ne _) s).mul (hs₁.elim ?_ ?_)
+    · exact fun h ↦ (differentiableAt_const _).div (by fun_prop) (by rwa [sub_ne_zero, ne_comm])
+    · exact fun h ↦ by simp only [h, zero_div, differentiableAt_const]
+
+/--
+Special case of `differentiableAt_completedLFunction` asserting differentiability everywhere
+under suitable hypotheses.
+-/
+lemma differentiable_completedLFunction (hΦ₂ : Φ 0 = 0) (hΦ₃ : ∑ j, Φ j = 0) :
+    Differentiable ℂ (completedLFunction Φ) :=
+  fun s ↦ differentiableAt_completedLFunction Φ s (.inr hΦ₂) (.inr hΦ₃)
+
+/--
+Relation between the completed L-function and the usual one (even case).
+We state it this way around so it holds at the poles of the gamma factor as well
+(except at `s = 0`, where it is genuinely false if `N > 1` and `Φ 0 ≠ 0`).
+-/
+lemma LFunction_eq_completed_div_gammaFactor_even (hΦ : Φ.Even) (s : ℂ) (hs : s ≠ 0 ∨ Φ 0 = 0) :
+    LFunction Φ s = completedLFunction Φ s / Gammaℝ s := by
+  simp only [completedLFunction_def_even hΦ, LFunction_def_even hΦ, mul_div_assoc, sum_div]
+  congr 2 with i
+  rcases ne_or_eq i 0 with hi | rfl
+  · rw [hurwitzZetaEven_def_of_ne_or_ne (.inl (hi ∘ toAddCircle_eq_zero.mp))]
+  · rcases hs with hs | hΦ'
+    · rw [hurwitzZetaEven_def_of_ne_or_ne (.inr hs)]
+    · simp only [hΦ', map_zero, zero_mul]
+
+/--
+Relation between the completed L-function and the usual one (odd case).
+We state it this way around so it holds at the poles of the gamma factor as well.
+-/
+lemma LFunction_eq_completed_div_gammaFactor_odd (hΦ : Φ.Odd) (s : ℂ) :
+    LFunction Φ s = completedLFunction Φ s / Gammaℝ (s + 1) := by
+  simp only [LFunction_def_odd hΦ, completedLFunction_def_odd hΦ, hurwitzZetaOdd, mul_div_assoc,
+    sum_div]
+
+/--
+First form of functional equation for completed L-functions (even case).
+
+Private because it is superseded by `completedLFunction_one_sub_even` below, which is valid for a
+much wider range of `s`.
+-/
+private lemma completedLFunction_one_sub_of_one_lt_even (hΦ : Φ.Even) {s : ℂ} (hs : 1 < re s) :
+    completedLFunction Φ (1 - s) = N ^ (s - 1) * completedLFunction (𝓕 Φ) s := by
+  have hs₀ : s ≠ 0 := ne_zero_of_one_lt_re hs
+  have hs₁ : s ≠ 1 := (lt_irrefl _ <| one_re ▸ · ▸ hs)
+  -- strip down to the key equality:
+  suffices ∑ x, Φ x * completedCosZeta (toAddCircle x) s = completedLFunction (𝓕 Φ) s by
+    simp only [completedLFunction_def_even hΦ, neg_sub, completedHurwitzZetaEven_one_sub, this]
+  -- reduce to equality with un-completed L-functions:
+  suffices ∑ x, Φ x * cosZeta (toAddCircle x) s = LFunction (𝓕 Φ) s by
+    simpa only [cosZeta, Function.update_noteq hs₀, ← mul_div_assoc, ← sum_div,
+      LFunction_eq_completed_div_gammaFactor_even (dft_even_iff.mpr hΦ) _ (.inl hs₀),
+      div_left_inj' (Gammaℝ_ne_zero_of_re_pos (zero_lt_one.trans hs))]
+  -- expand out `LFunction (𝓕 Φ)` and use parity:
+  simp only [cosZeta_eq, ← mul_div_assoc _ _ (2 : ℂ), mul_add, ← sum_div, sum_add_distrib,
+    LFunction_dft Φ (.inr hs₁), map_neg, div_eq_iff (two_ne_zero' ℂ), mul_two, add_left_inj]
+  exact Fintype.sum_equiv (.neg _) _ _ (by simp [hΦ _])
+
+/--
+First form of functional equation for completed L-functions (odd case).
+
+Private because it is superseded by `completedLFunction_one_sub_odd` below, which is valid for a
+much wider range of `s`.
+-/
+private lemma completedLFunction_one_sub_of_one_lt_odd (hΦ : Φ.Odd) {s : ℂ} (hs : 1 < re s) :
+    completedLFunction Φ (1 - s) = N ^ (s - 1) * I * completedLFunction (𝓕 Φ) s := by
+  -- strip down to the key equality:
+  suffices ∑ x, Φ x * completedSinZeta (toAddCircle x) s = I * completedLFunction (𝓕 Φ) s by
+    simp only [completedLFunction_def_odd hΦ, neg_sub, completedHurwitzZetaOdd_one_sub, this,
+      mul_assoc]
+  -- reduce to equality with un-completed L-functions:
+  suffices ∑ x, Φ x * sinZeta (toAddCircle x) s = I * LFunction (𝓕 Φ) s by
+    have hs' : 0 < re (s + 1) := by simp only [add_re, one_re]; linarith
+    simpa only [sinZeta, ← mul_div_assoc, ← sum_div, div_left_inj' (Gammaℝ_ne_zero_of_re_pos hs'),
+      LFunction_eq_completed_div_gammaFactor_odd (dft_odd_iff.mpr hΦ)]
+  -- now calculate:
+  calc ∑ x, Φ x * sinZeta (toAddCircle x) s
+  _ = (∑ x, Φ x * expZeta (toAddCircle x) s) / (2 * I)
+      - (∑ x, Φ x * expZeta (toAddCircle (-x)) s) / (2 * I) := by
+    simp only [sinZeta_eq, ← mul_div_assoc, mul_sub, sub_div, sum_sub_distrib, sum_div, map_neg]
+  _ = (∑ x, Φ (-x) * expZeta (toAddCircle (-x)) s) / (_) - (_) := by
+    congrm ?_ / _ - _
+    exact (Fintype.sum_equiv (.neg _) _ _ fun x ↦ by rfl).symm
+  _ = -I⁻¹ * LFunction (𝓕 Φ) s := by
+    simp only [hΦ _, neg_mul, sum_neg_distrib, LFunction_dft Φ (.inl hΦ.map_zero)]
+    ring
+  _ = I * LFunction (𝓕 Φ) s := by rw [inv_I, neg_neg]
+
+/--
+Functional equation for completed L-functions (even case), valid at all points of differentiability.
+-/
+theorem completedLFunction_one_sub_even (hΦ : Φ.Even) (s : ℂ)
+    (hs₀ : s ≠ 0 ∨ ∑ j, Φ j = 0) (hs₁ : s ≠ 1 ∨ Φ 0 = 0) :
+    completedLFunction Φ (1 - s) = N ^ (s - 1) * completedLFunction (𝓕 Φ) s := by
+  -- We prove this using `AnalyticOn.eqOn_of_preconnected_of_eventuallyEq`, so we need to
+  -- gather up the ingredients for this big theorem.
+  -- First set up some notations:
+  let F (t) := completedLFunction Φ (1 - t)
+  let G (t) := ↑N ^ (t - 1) * completedLFunction (𝓕 Φ) t
+  -- Set on which F, G are analytic:
+  let U := {t : ℂ | (t ≠ 0 ∨ ∑ j, Φ j = 0) ∧ (t ≠ 1 ∨ Φ 0 = 0)}
+  -- Properties of U:
+  have hsU : s ∈ U := ⟨hs₀, hs₁⟩
+  have h2U : 2 ∈ U := ⟨.inl two_ne_zero, .inl (OfNat.ofNat_ne_one _)⟩
+  have hUo : IsOpen U := (isOpen_compl_singleton.union isOpen_const).inter
+    (isOpen_compl_singleton.union isOpen_const)
+  have hUp : IsPreconnected U := by
+    -- need to write `U` as the complement of an obviously countable set
+    let Uc : Set ℂ := (if ∑ j, Φ j = 0 then ∅ else {0}) ∪ (if Φ 0 = 0 then ∅ else {1})
+    have : Uc.Countable := by
+      apply Countable.union <;>
+      split_ifs <;>
+      simp only [countable_singleton, countable_empty]
+    convert (this.isConnected_compl_of_one_lt_rank ?_).isPreconnected using 1
+    · ext x
+      by_cases h : Φ 0 = 0 <;>
+      by_cases h' : ∑ j, Φ j = 0 <;>
+      simp [U, Uc, h, h', and_comm]
+    · simp only [rank_real_complex, Nat.one_lt_ofNat]
+  -- Analyticity on U:
+  have hF : AnalyticOn ℂ F U := by
+    refine DifferentiableOn.analyticOn (fun t ht ↦ DifferentiableAt.differentiableWithinAt ?_) hUo
+    refine (differentiableAt_completedLFunction Φ _ ?_ ?_).comp t (differentiableAt_id.const_sub 1)
+    exacts [ht.2.imp_left (sub_ne_zero.mpr ∘ Ne.symm), ht.1.imp_left sub_eq_self.not.mpr]
+  have hG : AnalyticOn ℂ G U := by
+    refine DifferentiableOn.analyticOn (fun t ht ↦ DifferentiableAt.differentiableWithinAt ?_) hUo
+    apply ((differentiableAt_id.sub_const 1).const_cpow (.inl (NeZero.ne _))).mul
+    apply differentiableAt_completedLFunction _ _ (ht.1.imp_right fun h ↦ dft_apply_zero Φ ▸ h)
+    exact ht.2.imp_right (fun h ↦ by simp only [← dft_apply_zero, dft_dft, neg_zero, h, smul_zero])
+  -- set where we know equality
+  have hV : {z | 1 < re z} ∈ 𝓝 2 := (continuous_re.isOpen_preimage _ isOpen_Ioi).mem_nhds (by simp)
+  have hFG : F =ᶠ[𝓝 2] G := eventually_of_mem hV <| fun t ht ↦ by
+    simpa only [F, G, pow_zero, mul_one] using completedLFunction_one_sub_of_one_lt_even hΦ ht
+  -- now apply the big hammer to finish
+  exact hF.eqOn_of_preconnected_of_eventuallyEq hG hUp h2U hFG hsU
+
+/-- Functional equation for completed L-functions (odd case), valid for all `s`. -/
+theorem completedLFunction_one_sub_odd (hΦ : Φ.Odd) (s : ℂ) :
+    completedLFunction Φ (1 - s) = N ^ (s - 1) * I * completedLFunction (𝓕 Φ) s := by
+  -- This is much easier than the even case since both functions are entire.
+  -- First set up some notations:
+  let F (t) := completedLFunction Φ (1 - t)
+  let G (t) := ↑N ^ (t - 1) * I * completedLFunction (𝓕 Φ) t
+  -- check F, G globally differentiable
+  have hF : Differentiable ℂ F := (differentiable_completedLFunction hΦ.map_zero
+    hΦ.sum_eq_zero).comp (differentiable_id.const_sub 1)
+  have hG : Differentiable ℂ G := by
+    apply (((differentiable_id.sub_const 1).const_cpow (.inl (NeZero.ne _))).mul_const _).mul
+    rw [← dft_odd_iff] at hΦ
+    exact differentiable_completedLFunction hΦ.map_zero hΦ.sum_eq_zero
+  -- set where we know equality
+  have : {z | 1 < re z} ∈ 𝓝 2 := (continuous_re.isOpen_preimage _ isOpen_Ioi).mem_nhds (by simp)
+  have hFG : F =ᶠ[𝓝 2] G := by filter_upwards [this] with t ht
+    using completedLFunction_one_sub_of_one_lt_odd hΦ ht
+  -- now apply the big hammer to finish
+  rw [← analyticOn_univ_iff_differentiable] at hF hG
+  exact congr_fun (hF.eq_of_eventuallyEq hG hFG) s
+
+end signed
+
 end ZMod