feat(NumberTheory/LSeries/Deriv): derivatives of L-series (#11245)

This adds a file `Mathlib.NumberTheory.LSeries.Deriv` that contains results on differentiability and derivatives of L-series, including the fact that the L-series is holomorphic on its right half-plane of absolute convergence.

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



Co-authored-by: David Loeffler <d.loeffler.01@cantab.net>

Mathlib.lean

@@ -711,6 +711,7 @@ import Mathlib.Analysis.Complex.CauchyIntegral
 import Mathlib.Analysis.Complex.Circle
 import Mathlib.Analysis.Complex.Conformal
 import Mathlib.Analysis.Complex.Convex
+import Mathlib.Analysis.Complex.HalfPlane
 import Mathlib.Analysis.Complex.Isometry
 import Mathlib.Analysis.Complex.Liouville
 import Mathlib.Analysis.Complex.LocallyUniformLimit
@@ -2957,6 +2958,7 @@ import Mathlib.NumberTheory.KummerDedekind
 import Mathlib.NumberTheory.LSeries.AbstractFuncEq
 import Mathlib.NumberTheory.LSeries.Basic
 import Mathlib.NumberTheory.LSeries.Convergence
+import Mathlib.NumberTheory.LSeries.Deriv
 import Mathlib.NumberTheory.LSeries.Linearity
 import Mathlib.NumberTheory.LegendreSymbol.AddCharacter
 import Mathlib.NumberTheory.LegendreSymbol.Basic

Mathlib/Analysis/Complex/HalfPlane.lean

@@ -0,0 +1,39 @@
+/-
+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.Analysis.Complex.Basic
+import Mathlib.Topology.Instances.EReal
+
+/-!
+# Half-planes in ℂ are open
+
+We state that open left, right, upper and lower half-planes in the complex numbers are open sets,
+where the bounding value of the real or imaginary part is given by an `EReal` `x`.
+So this includes the full plane and the empty set for `x = ⊤`/`x = ⊥`.
+-/
+
+namespace Complex
+
+/-- An open left half-plane (with boundary real part given by an `EReal`) is an open set
+in the complex plane. -/
+lemma isOpen_re_lt_EReal (x : EReal) : IsOpen {z : ℂ | z.re < x} :=
+  isOpen_lt (EReal.continuous_coe_iff.mpr continuous_re) continuous_const
+
+/-- An open right half-plane (with boundary real part given by an `EReal`) is an open set
+in the complex plane. -/
+lemma isOpen_re_gt_EReal (x : EReal) : IsOpen {z : ℂ | x < z.re} :=
+  isOpen_lt continuous_const <| EReal.continuous_coe_iff.mpr continuous_re
+
+/-- An open lower half-plane (with boundary imaginary part given by an `EReal`) is an open set
+in the complex plane. -/
+lemma isOpen_im_lt_EReal (x : EReal) : IsOpen {z : ℂ | z.im < x} :=
+  isOpen_lt (EReal.continuous_coe_iff.mpr continuous_im) continuous_const
+
+/-- An open upper half-plane (with boundary imaginary part given by an `EReal`) is an open set
+in the complex plane. -/
+lemma isOpen_im_gt_EReal (x : EReal) : IsOpen {z : ℂ | x < z.im} :=
+  isOpen_lt continuous_const <| EReal.continuous_coe_iff.mpr continuous_im
+
+end Complex

Mathlib/NumberTheory/LSeries/Basic.lean

@@ -143,6 +143,28 @@ lemma LSeriesSummable_congr {f g : ℕ → ℂ} (s : ℂ) (h : ∀ n ≠ 0, f n
     LSeriesSummable f s ↔ LSeriesSummable g s :=
   summable_congr <| term_congr h s
 
+open Filter in
+/-- If `f` and `g` agree on large `n : ℕ` and the `LSeries` of `f` converges at `s`,
+then so does that of `g`. -/
+lemma LSeriesSummable.congr' {f g : ℕ → ℂ} (s : ℂ) (h : f =ᶠ[atTop] g) (hf : LSeriesSummable f s) :
+    LSeriesSummable g s := by
+  rw [← Nat.cofinite_eq_atTop] at h
+  refine (summable_norm_iff.mpr hf).of_norm_bounded_eventually _ ?_
+  have : term f s =ᶠ[cofinite] term g s := by
+    rw [eventuallyEq_iff_exists_mem] at h ⊢
+    obtain ⟨S, hS, hS'⟩ := h
+    refine ⟨S \ {0}, diff_mem hS <| (Set.finite_singleton 0).compl_mem_cofinite, fun n hn ↦ ?_⟩
+    simp only [Set.mem_diff, Set.mem_singleton_iff] at hn
+    simp only [term_of_ne_zero hn.2, hS' hn.1]
+  exact Eventually.mono this.symm fun n hn ↦ by simp only [hn, le_rfl]
+
+open Filter in
+/-- If `f` and `g` agree on large `n : ℕ`, then the `LSeries` of `f` converges at `s`
+if and only if that of `g` does. -/
+lemma LSeriesSummable_congr' {f g : ℕ → ℂ} (s : ℂ) (h : f =ᶠ[atTop] g) :
+    LSeriesSummable f s ↔ LSeriesSummable g s :=
+  ⟨fun H ↦ H.congr' s h, fun H ↦ H.congr' s h.symm⟩
+
 theorem LSeries.eq_zero_of_not_LSeriesSummable (f : ℕ → ℂ) (s : ℂ) :
     ¬ LSeriesSummable f s → LSeries f s = 0 :=
   tsum_eq_zero_of_not_summable

Mathlib/NumberTheory/LSeries/Convergence.lean

@@ -26,6 +26,17 @@ 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) :
+    abscissaOfAbsConv f = abscissaOfAbsConv g :=
+  congr_arg sInf <| congr_arg _ <| Set.ext fun x ↦ LSeriesSummable_congr x h
+
+open Filter in
+/-- If `f` and `g` agree on large `n : ℕ`, then their `LSeries` have the same
+abscissa of absolute convergence. -/
+lemma LSeries.abscissaOfAbsConv_congr' {f g : ℕ → ℂ} (h : f =ᶠ[atTop] g) :
+    abscissaOfAbsConv f = abscissaOfAbsConv g :=
+  congr_arg sInf <| congr_arg _ <| Set.ext fun x ↦ LSeriesSummable_congr' x h
+
 open LSeries
 
 lemma LSeriesSummable_of_abscissaOfAbsConv_lt_re {f : ℕ → ℂ} {s : ℂ}

Mathlib/NumberTheory/LSeries/Deriv.lean

@@ -0,0 +1,156 @@
+/-
+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.Analysis.Complex.LocallyUniformLimit
+import Mathlib.NumberTheory.LSeries.Convergence
+import Mathlib.Analysis.SpecialFunctions.Pow.Deriv
+import Mathlib.Analysis.Complex.HalfPlane
+
+/-!
+# Differentiability and derivatives of L-series
+
+## Main results
+
+* We show that the `LSeries` of `f` is differentiable at `s` when `re s` is greater than
+  the abscissa of absolute convergence of `f` (`LSeries.hasDerivAt`) and that its derivative
+  there is the negative of the `LSeries` of the point-wise product `log * f` (`LSeries.deriv`).
+
+* We prove similar results for iterated derivatives (`LSeries.iteratedDeriv`).
+
+* We use this to show that `LSeries f` is holomorphic on the right half-plane of
+  absolute convergence (`LSeries.analyticOn`).
+
+## Implementation notes
+
+We introduce `LSeries.logMul` as an abbreviation for the point-wise product `log * f`, to avoid
+the problem that this expression does not type-check.
+-/
+
+open Complex LSeries
+
+/-!
+### The derivative of an L-series
+-/
+
+/-- The (point-wise) product of `log : ℕ → ℂ` with `f`. -/
+noncomputable abbrev LSeries.logMul (f : ℕ → ℂ) (n : ℕ) : ℂ := log n * f n
+
+/-- The derivative of the terms of an L-series. -/
+lemma LSeries.hasDerivAt_term (f : ℕ → ℂ) (n : ℕ) (s : ℂ) :
+    HasDerivAt (fun z ↦ term f z n) (-(term (logMul f) s n)) s := by
+  rcases eq_or_ne n 0 with rfl | hn
+  · simp only [term_zero, neg_zero, hasDerivAt_const]
+  simp_rw [term_of_ne_zero hn, ← neg_div, ← neg_mul, mul_comm, mul_div_assoc, div_eq_mul_inv,
+    ← cpow_neg]
+  exact HasDerivAt.const_mul (f n) (by simpa only [mul_comm, ← mul_neg_one (log n), ← mul_assoc]
+    using (hasDerivAt_neg' s).const_cpow (Or.inl <| Nat.cast_ne_zero.mpr hn))
+
+/- This lemma proves two things at once, since their proofs are intertwined; we give separate
+non-private lemmas below that extract the two statements. -/
+private lemma LSeries.LSeriesSummable_logMul_and_hasDerivAt {f : ℕ → ℂ} {s : ℂ}
+    (h : abscissaOfAbsConv f < s.re) :
+    LSeriesSummable (logMul f) s ∧ HasDerivAt (LSeries f) (-LSeries (logMul f) s) s := by
+  -- The L-series of `f` is summable at some real `x < re s`.
+  obtain ⟨x, hxs, hf⟩ := LSeriesSummable_lt_re_of_abscissaOfAbsConv_lt_re h
+  obtain ⟨y, hxy, hys⟩ := exists_between hxs
+  -- We work in the right half-plane `y < re z`, for some `y` such that `x < y < re s`, on which
+  -- we have a uniform summable bound on `‖term f z ·‖`.
+  let S : Set ℂ := {z | y < z.re}
+  have h₀ : Summable (fun n ↦ ‖term f x n‖) := summable_norm_iff.mpr hf
+  have h₁ (n) : DifferentiableOn ℂ (term f · n) S :=
+    fun z _ ↦ (hasDerivAt_term f n _).differentiableAt.differentiableWithinAt
+  have h₂ : IsOpen S := isOpen_lt continuous_const continuous_re
+  have h₃ (n z) (hz : z ∈ S) : ‖term f z n‖ ≤ ‖term f x n‖ :=
+    norm_term_le_of_re_le_re f (by simpa using (hxy.trans hz).le) n
+  have H := hasSum_deriv_of_summable_norm h₀ h₁ h₂ h₃ hys
+  simp_rw [(hasDerivAt_term f _ _).deriv] at H
+  refine ⟨summable_neg_iff.mp H.summable, ?_⟩
+  have H' := differentiableOn_tsum_of_summable_norm h₀ h₁ h₂ h₃
+  simpa only [← H.tsum_eq, tsum_neg]
+    using (H'.differentiableAt <| IsOpen.mem_nhds h₂ hys).hasDerivAt
+
+/-- If `re s` is greater than the abscissa of absolute convergence of `f`, then the L-series
+of `f` is differentiable with derivative the negative of the L-series of the point-wise
+product of `log` with `f`. -/
+lemma LSeries_hasDerivAt {f : ℕ → ℂ} {s : ℂ} (h : abscissaOfAbsConv f < s.re) :
+    HasDerivAt (LSeries f) (- LSeries (logMul f) s) s :=
+  (LSeriesSummable_logMul_and_hasDerivAt h).2
+
+/-- If `re s` is greater than the abscissa of absolute convergence of `f`, then
+the derivative of this L-series at `s` is the negative of the L-series of `log * f`. -/
+lemma LSeries_deriv {f : ℕ → ℂ} {s : ℂ} (h : abscissaOfAbsConv f < s.re) :
+    deriv (LSeries f) s = - LSeries (logMul f) s :=
+  (LSeries_hasDerivAt h).deriv
+
+/-- The derivative of the L-series of `f` agrees with the negative of the L-series of
+`log * f` on the right half-plane of absolute convergence. -/
+lemma LSeries_deriv_eqOn {f : ℕ → ℂ} :
+    {s | abscissaOfAbsConv f < s.re}.EqOn (deriv (LSeries f)) (- LSeries (logMul f)) :=
+  deriv_eqOn (isOpen_re_gt_EReal _) fun _ hs ↦ (LSeries_hasDerivAt hs).hasDerivWithinAt
+
+/-- If the L-series of `f` is summable at `s` and `re s < re s'`, then the L-series of the
+point-wise product of `log` with `f` is summable at `s'`. -/
+lemma LSeriesSummable_logMul_of_lt_re {f : ℕ → ℂ} {s : ℂ} (h : abscissaOfAbsConv f < s.re) :
+    LSeriesSummable (logMul f) s :=
+  (LSeriesSummable_logMul_and_hasDerivAt h).1
+
+/-- The abscissa of absolute convergence of the point-wise product of `log` and `f`
+is the same as that of `f`. -/
+@[simp]
+lemma LSeries.abscissaOfAbsConv_logMul {f : ℕ → ℂ} :
+    abscissaOfAbsConv (logMul f) = abscissaOfAbsConv f := by
+  apply le_antisymm <;> refine abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable' fun s hs ↦ ?_
+  · exact LSeriesSummable_logMul_of_lt_re <| by simp [hs]
+  · refine (LSeriesSummable_of_abscissaOfAbsConv_lt_re <| by simp only [ofReal_re, hs])
+      |>.norm.of_norm_bounded_eventually_nat (‖term (logMul f) s ·‖) ?_
+    filter_upwards [Filter.eventually_ge_atTop <| max 1 (Nat.ceil (Real.exp 1))] with n hn
+    simp only [term_of_ne_zero (show n ≠ 0 by omega), logMul, norm_mul, mul_div_assoc,
+      ← natCast_log, norm_real]
+    refine le_mul_of_one_le_left (norm_nonneg _) (.trans ?_ <| Real.le_norm_self _)
+    rw [← Real.log_exp 1]
+    exact Real.log_le_log (Real.exp_pos 1) <| Nat.ceil_le.mp <| (le_max_right _ _).trans hn
+
+/-!
+### Higher derivatives of L-series
+-/
+
+/-- The abscissa of absolute convergence of the point-wise product of a power of `log` and `f`
+is the same as that of `f`. -/
+@[simp]
+lemma LSeries.absicssaOfAbsConv_logPowMul {f : ℕ → ℂ} {m : ℕ} :
+    abscissaOfAbsConv (logMul^[m] f) = abscissaOfAbsConv f := by
+  induction' m with n ih
+  · simp only [Nat.zero_eq, Function.iterate_zero, id_eq]
+  · simp only [ih, Function.iterate_succ', Function.comp_def, abscissaOfAbsConv_logMul]
+
+/-- If `re s` is greater than the abscissa of absolute convergence of `f`, then
+the `m`th derivative of this L-series is `(-1)^m` times the L-series of `log^m * f`. -/
+lemma LSeries_iteratedDeriv {f : ℕ → ℂ} (m : ℕ) {s : ℂ} (h : abscissaOfAbsConv f < s.re) :
+    iteratedDeriv m (LSeries f) s = (-1) ^ m * LSeries (logMul^[m] f) s := by
+  induction' m with m ih generalizing s
+  · simp only [Nat.zero_eq, iteratedDeriv_zero, pow_zero, Function.iterate_zero, id_eq, one_mul]
+  · have ih' : {s | abscissaOfAbsConv f < re s}.EqOn (iteratedDeriv m (LSeries f))
+        ((-1) ^ m * LSeries (logMul^[m] f)) := fun _ hs ↦ ih hs
+    have := derivWithin_congr ih' (ih h)
+    simp_rw [derivWithin_of_isOpen (isOpen_re_gt_EReal _) h] at this
+    rw [iteratedDeriv_succ, this]
+    simp only [Pi.mul_def, Pi.pow_apply, Pi.neg_apply, Pi.one_apply, deriv_const_mul_field',
+      pow_succ', mul_assoc, neg_one_mul, Function.iterate_succ', Function.comp_def,
+      LSeries_deriv <| absicssaOfAbsConv_logPowMul.symm ▸ h]
+
+/-!
+### The L-series is holomorphic
+-/
+
+/-- The L-series of `f` is complex differentiable in its open half-plane of absolute
+convergence. -/
+lemma LSeries_differentiableOn (f : ℕ → ℂ) :
+    DifferentiableOn ℂ (LSeries f) {s | abscissaOfAbsConv f < s.re} :=
+  fun _ hz ↦ (LSeries_hasDerivAt hz).differentiableAt.differentiableWithinAt
+
+/-- The L-series of `f` is holomorphic on its open half-plane of absolute convergence. -/
+lemma LSeries_analyticOn (f : ℕ → ℂ) :
+    AnalyticOn ℂ (LSeries f) {s | abscissaOfAbsConv f < s.re} :=
+  (LSeries_differentiableOn f).analyticOn <| isOpen_re_gt_EReal _