feat(NumberTheory/LSeries): results involving partial sums of coefficients (part 1) (#20661)

 We prove several results involving partial sums of coefficients (or norm of coefficients) of  L-series. 

The two main results of this PR are:

- `LSeriesSummable_of_sum_norm_bigO`: for `f : ℕ → ℂ`, if the partial sums `∑ k ∈ Icc 1 n, ‖f k‖` are `O(n ^ r)` for some real `0 ≤ r`, then the L-series `Lseries f` converges at `s : ℂ` for all `s` such that `r < s.re`.

- `LSeries_eq_mul_integral` : for `f : ℕ → ℂ`, if the partial sums `∑ k ∈ Icc 1 n, f k` are `O(n ^ r)` for some real `0 ≤ r` and the L-series `LSeries f` converges at `s : ℂ` with `r < s.re`, then `LSeries f s = s * ∫ t in Set.Ioi 1, (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * t ^ (- (s + 1))`.

More results will be proved in #20660

Author: xroblot

Mathlib.lean

@@ -4020,6 +4020,7 @@ import Mathlib.NumberTheory.LSeries.Nonvanishing
 import Mathlib.NumberTheory.LSeries.Positivity
 import Mathlib.NumberTheory.LSeries.PrimesInAP
 import Mathlib.NumberTheory.LSeries.RiemannZeta
+import Mathlib.NumberTheory.LSeries.SumCoeff
 import Mathlib.NumberTheory.LSeries.ZMod
 import Mathlib.NumberTheory.LegendreSymbol.AddCharacter
 import Mathlib.NumberTheory.LegendreSymbol.Basic

Mathlib/Analysis/Asymptotics/SpecificAsymptotics.lean

@@ -3,9 +3,8 @@ Copyright (c) 2021 Anatole Dedecker. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anatole Dedecker
 -/
-import Mathlib.Analysis.Normed.Order.Basic
-import Mathlib.Analysis.Asymptotics.Lemmas
-import Mathlib.Analysis.Normed.Module.Basic
+import Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
+import Mathlib.Analysis.SpecificLimits.Basic
 
 /-!
 # A collection of specific asymptotic results
@@ -143,3 +142,19 @@ theorem Filter.Tendsto.cesaro {u : ℕ → ℝ} {l : ℝ} (h : Tendsto u atTop (
   h.cesaro_smul
 
 end Real
+
+section NormedLinearOrderedField
+
+variable {R : Type*} [NormedLinearOrderedField R] [OrderTopology R] [FloorRing R]
+
+theorem Asymptotics.isEquivalent_nat_floor :
+    (fun (x : R) ↦ ↑⌊x⌋₊) ~[atTop] (fun x ↦ x) := by
+  refine isEquivalent_of_tendsto_one ?_ tendsto_nat_floor_div_atTop
+  filter_upwards with x hx using by rw [hx, Nat.floor_zero, Nat.cast_eq_zero]
+
+theorem Asymptotics.isEquivalent_nat_ceil :
+    (fun (x : R) ↦ ↑⌈x⌉₊) ~[atTop] (fun x ↦ x) := by
+  refine isEquivalent_of_tendsto_one ?_ tendsto_nat_ceil_div_atTop
+  filter_upwards with x hx using by rw [hx, Nat.ceil_zero, Nat.cast_eq_zero]
+
+end NormedLinearOrderedField

Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean

@@ -81,6 +81,14 @@ theorem integrableOn_Ioi_rpow_iff {s t : ℝ} (ht : 0 < t) :
     exact Real.rpow_le_rpow_of_exponent_le x_one h
   exact not_IntegrableOn_Ioi_inv this
 
+theorem integrableAtFilter_rpow_atTop_iff {s : ℝ} :
+    IntegrableAtFilter (fun x : ℝ ↦ x ^ s) atTop ↔ s < -1 := by
+  refine ⟨fun ⟨t, ht, hint⟩ ↦ ?_, fun h ↦
+    ⟨Set.Ioi 1, Ioi_mem_atTop 1, (integrableOn_Ioi_rpow_iff zero_lt_one).mpr h⟩⟩
+  obtain ⟨a, ha⟩ := mem_atTop_sets.mp ht
+  refine (integrableOn_Ioi_rpow_iff (zero_lt_one.trans_le (le_max_right a 1))).mp ?_
+  exact hint.mono_set <| fun x hx ↦ ha _ <| (le_max_left a 1).trans hx.le
+
 /-- The real power function with any exponent is not integrable on `(0, +∞)`. -/
 theorem not_integrableOn_Ioi_rpow (s : ℝ) : ¬ IntegrableOn (fun x ↦ x ^ s) (Ioi (0 : ℝ)) := by
   intro h
@@ -127,6 +135,24 @@ theorem integrableOn_Ioi_cpow_iff {s : ℂ} {t : ℝ} (ht : 0 < t) :
     simp [Complex.abs_cpow_eq_rpow_re_of_pos this]
   rwa [integrableOn_Ioi_rpow_iff ht] at B
 
+theorem integrableOn_Ioi_deriv_ofReal_cpow {s : ℂ} {t : ℝ} (ht : 0 < t) (hs : s.re < 0) :
+    IntegrableOn (deriv fun x : ℝ ↦ (x : ℂ) ^ s) (Set.Ioi t) := by
+  have h : IntegrableOn (fun x : ℝ ↦ s * x ^ (s - 1)) (Set.Ioi t) := by
+    refine (integrableOn_Ioi_cpow_of_lt ?_ ht).const_mul _
+    rwa [Complex.sub_re, Complex.one_re, sub_lt_iff_lt_add, neg_add_cancel]
+  refine h.congr_fun (fun x hx ↦ ?_) measurableSet_Ioi
+  rw [Complex.deriv_ofReal_cpow_const (ht.trans hx).ne' (fun h ↦ (Complex.zero_re ▸ h ▸ hs).false)]
+
+theorem integrableOn_Ioi_deriv_norm_ofReal_cpow {s : ℂ} {t : ℝ} (ht : 0 < t) (hs : s.re ≤ 0):
+    IntegrableOn (deriv fun x : ℝ ↦ ‖(x : ℂ) ^ s‖) (Set.Ioi t) := by
+  rw [integrableOn_congr_fun (fun x hx ↦ by
+    rw [deriv_norm_ofReal_cpow _ (ht.trans hx)]) measurableSet_Ioi]
+  obtain hs | hs := eq_or_lt_of_le hs
+  · simp_rw [hs, zero_mul]
+    exact integrableOn_zero
+  · replace hs : s.re - 1 < - 1 := by rwa [sub_lt_iff_lt_add, neg_add_cancel]
+    exact (integrableOn_Ioi_rpow_of_lt hs ht).const_mul s.re
+
 /-- The complex power function with any exponent is not integrable on `(0, +∞)`. -/
 theorem not_integrableOn_Ioi_cpow (s : ℂ) :
     ¬ IntegrableOn (fun x : ℝ ↦ (x : ℂ) ^ s) (Ioi (0 : ℝ)) := by

Mathlib/Analysis/SpecialFunctions/Pow/Complex.lean

@@ -42,6 +42,13 @@ theorem cpow_eq_zero_iff (x y : ℂ) : x ^ y = 0 ↔ x = 0 ∧ y ≠ 0 := by
   simp only [cpow_def]
   split_ifs <;> simp [*, exp_ne_zero]
 
+theorem cpow_ne_zero_iff {x y : ℂ} :
+    x ^ y ≠ 0 ↔ x ≠ 0 ∨ y = 0 := by
+  rw [ne_eq, cpow_eq_zero_iff, not_and_or, ne_eq, not_not]
+
+theorem cpow_ne_zero_iff_of_exponent_ne_zero {x y : ℂ} (hy : y ≠ 0) :
+    x ^ y ≠ 0 ↔ x ≠ 0 := by simp [hy]
+
 @[simp]
 theorem zero_cpow {x : ℂ} (h : x ≠ 0) : (0 : ℂ) ^ x = 0 := by simp [cpow_def, *]
 

Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean

@@ -623,6 +623,13 @@ theorem deriv_rpow_const (hf : DifferentiableAt ℝ f x) (hx : f x ≠ 0 ∨ 1 
     deriv (fun x => f x ^ p) x = deriv f x * p * f x ^ (p - 1) :=
   (hf.hasDerivAt.rpow_const hx).deriv
 
+theorem deriv_norm_ofReal_cpow (c : ℂ) {t : ℝ} (ht : 0 < t) :
+    (deriv fun x : ℝ ↦ ‖(x : ℂ) ^ c‖) t = c.re * t ^ (c.re - 1) := by
+  rw [EventuallyEq.deriv_eq (f := fun x ↦ x ^ c.re)]
+  · rw [Real.deriv_rpow_const (Or.inl ht.ne')]
+  · filter_upwards [eventually_gt_nhds ht] with x hx
+    rw [Complex.norm_eq_abs, Complex.abs_cpow_eq_rpow_re_of_pos hx]
+
 lemma isTheta_deriv_rpow_const_atTop {p : ℝ} (hp : p ≠ 0) :
     deriv (fun (x : ℝ) => x ^ p) =Θ[atTop] fun x => x ^ (p-1) := by
   calc deriv (fun (x : ℝ) => x ^ p) =ᶠ[atTop] fun x => p * x ^ (p - 1) := by

Mathlib/Analysis/SpecialFunctions/Pow/Real.lean

@@ -318,6 +318,12 @@ theorem abs_cpow_eq_rpow_re_of_nonneg {x : ℝ} (hx : 0 ≤ x) {y : ℂ} (hy : r
     abs (x ^ y) = x ^ re y := by
   rw [abs_cpow_of_imp] <;> simp [*, arg_ofReal_of_nonneg, _root_.abs_of_nonneg]
 
+open Filter in
+lemma norm_ofReal_cpow_eventually_eq_atTop (c : ℂ) :
+    (fun t : ℝ ↦ ‖(t : ℂ) ^ c‖) =ᶠ[atTop] fun t ↦ t ^ c.re := by
+  filter_upwards [eventually_gt_atTop 0] with t ht
+  rw [Complex.norm_eq_abs, abs_cpow_eq_rpow_re_of_pos ht]
+
 lemma norm_natCast_cpow_of_re_ne_zero (n : ℕ) {s : ℂ} (hs : s.re ≠ 0) :
     ‖(n : ℂ) ^ s‖ = (n : ℝ) ^ (s.re) := by
   rw [norm_eq_abs, ← ofReal_natCast, abs_cpow_eq_rpow_re_of_nonneg n.cast_nonneg hs]
@@ -962,6 +968,35 @@ lemma norm_log_natCast_le_rpow_div (n : ℕ) {ε : ℝ} (hε : 0 < ε) : ‖log
 
 end Complex
 
+namespace  Asymptotics
+
+open Filter
+
+variable {E : Type*} [SeminormedRing E] (a b c : ℝ)
+
+theorem IsBigO.mul_atTop_rpow_of_isBigO_rpow {f g : ℝ → E}
+    (hf : f =O[atTop] fun t ↦ (t : ℝ) ^ a) (hg : g =O[atTop] fun t ↦ (t : ℝ) ^ b)
+    (h : a + b ≤ c) :
+    (f * g) =O[atTop] fun t ↦ (t : ℝ) ^ c := by
+  refine (hf.mul hg).trans (Eventually.isBigO ?_)
+  filter_upwards [eventually_ge_atTop 1] with t ht
+  rw [← Real.rpow_add (zero_lt_one.trans_le ht), Real.norm_of_nonneg (Real.rpow_nonneg
+    (zero_le_one.trans ht) (a + b))]
+  exact Real.rpow_le_rpow_of_exponent_le ht h
+
+theorem IsBigO.mul_atTop_rpow_natCast_of_isBigO_rpow {f g : ℕ → E}
+    (hf : f =O[atTop] fun n ↦ (n : ℝ) ^ a) (hg : g =O[atTop] fun n ↦ (n : ℝ) ^ b)
+    (h : a + b ≤ c) :
+    (f * g) =O[atTop] fun n ↦ (n : ℝ) ^ c := by
+  refine (hf.mul hg).trans (Eventually.isBigO ?_)
+  filter_upwards [eventually_ge_atTop 1] with t ht
+  replace ht : 1 ≤ (t : ℝ) := Nat.one_le_cast.mpr ht
+  rw [← Real.rpow_add (zero_lt_one.trans_le ht), Real.norm_of_nonneg (Real.rpow_nonneg
+    (zero_le_one.trans ht) (a + b))]
+  exact Real.rpow_le_rpow_of_exponent_le ht h
+
+end Asymptotics
+
 /-!
 ## Square roots of reals
 -/

Mathlib/Data/Complex/Abs.lean

@@ -291,10 +291,16 @@ theorem lim_abs (f : CauSeq ℂ Complex.abs) : lim (cauSeqAbs f) = Complex.abs (
     let ⟨i, hi⟩ := equiv_lim f ε ε0
     ⟨i, fun j hj => lt_of_le_of_lt (Complex.abs.abs_abv_sub_le_abv_sub _ _) (hi j hj)⟩
 
+lemma ne_zero_of_re_pos {s : ℂ} (hs : 0 < s.re) : s ≠ 0 :=
+  fun h ↦ (zero_re ▸ h ▸ hs).false
+
 lemma ne_zero_of_one_lt_re {s : ℂ} (hs : 1 < s.re) : s ≠ 0 :=
-  fun h ↦ ((zero_re ▸ h ▸ hs).trans zero_lt_one).false
+  ne_zero_of_re_pos <| zero_lt_one.trans hs
+
+lemma re_neg_ne_zero_of_re_pos {s : ℂ} (hs : 0 < s.re) : (-s).re ≠ 0 :=
+  ne_iff_lt_or_gt.mpr <| Or.inl <| neg_re s ▸ (neg_lt_zero.mpr hs)
 
 lemma re_neg_ne_zero_of_one_lt_re {s : ℂ} (hs : 1 < s.re) : (-s).re ≠ 0 :=
-  ne_iff_lt_or_gt.mpr <| Or.inl <| neg_re s ▸ by linarith
+  re_neg_ne_zero_of_re_pos <| zero_lt_one.trans hs
 
 end Complex

Mathlib/NumberTheory/AbelSummation.lean

@@ -51,8 +51,8 @@ namespace abelSummationProof
 
 open intervalIntegral IntervalIntegrable
 
-private theorem sumlocc (n : ℕ) :
-    ∀ᵐ t, t ∈ Set.Icc (n : ℝ) (n + 1) → ∑ k ∈ Icc 0 ⌊t⌋₊, c k = ∑ k ∈ Icc 0 n, c k := by
+private theorem sumlocc {m : ℕ} (n : ℕ) :
+    ∀ᵐ t, t ∈ Set.Icc (n : ℝ) (n + 1) → ∑ k ∈ Icc m ⌊t⌋₊, c k = ∑ k ∈ Icc m n, c k := by
   filter_upwards [Ico_ae_eq_Icc] with t h ht
   rw [Nat.floor_eq_on_Ico _ _ (h.mpr ht)]
 
@@ -83,19 +83,20 @@ private theorem ineqofmemIco' {k : ℕ} (hk : k ∈ Ico (⌊a⌋₊ + 1) ⌊b⌋
     a ≤ k ∧ k + 1 ≤ b :=
   ineqofmemIco (by rwa [← Finset.coe_Ico])
 
-private theorem integrablemulsum (ha : 0 ≤ a) {g : ℝ → 𝕜} (hg_int : IntegrableOn g (Set.Icc a b)) :
-    IntegrableOn (fun t ↦ g t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) (Set.Icc a b) := by
+theorem _root_.integrableOn_mul_sum_Icc {m : ℕ} (ha : 0 ≤ a) {g : ℝ → 𝕜}
+    (hg_int : IntegrableOn g (Set.Icc a b)) :
+    IntegrableOn (fun t ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) (Set.Icc a b) := by
   obtain hab | hab := le_or_gt a b
   · obtain hb | hb := eq_or_lt_of_le (Nat.floor_le_floor hab)
-    · have : ∀ᵐ t, t ∈ Set.Icc a b → ∑ k ∈ Icc 0 ⌊a⌋₊, c k = ∑ k ∈ Icc 0 ⌊t⌋₊, c k := by
+    · have : ∀ᵐ t, t ∈ Set.Icc a b → ∑ k ∈ Icc m ⌊a⌋₊, c k = ∑ k ∈ Icc m ⌊t⌋₊, c k := by
         filter_upwards [sumlocc c ⌊a⌋₊] with t ht₁ ht₂
         rw [ht₁ ⟨(Nat.floor_le ha).trans ht₂.1, hb ▸ ht₂.2.trans (Nat.lt_floor_add_one b).le⟩]
       rw [← ae_restrict_iff' measurableSet_Icc] at this
       exact IntegrableOn.congr_fun_ae
         (hg_int.mul_const _) ((Filter.EventuallyEq.refl _ g).mul this)
     · have h_locint {t₁ t₂ : ℝ} {n : ℕ} (h : t₁ ≤ t₂) (h₁ : n ≤ t₁) (h₂ : t₂ ≤ n + 1)
           (h₃ : a ≤ t₁) (h₄ : t₂ ≤ b) :
-          IntervalIntegrable (fun t ↦ g t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) volume t₁ t₂ := by
+          IntervalIntegrable (fun t ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume t₁ t₂ := by
         rw [intervalIntegrable_iff_integrableOn_Icc_of_le h]
         exact (IntegrableOn.mono_set (hg_int.mul_const _) (Set.Icc_subset_Icc h₃ h₄)).congr
           <| ae_restrict_of_ae_restrict_of_subset (Set.Icc_subset_Icc h₁ h₂)
@@ -154,15 +155,15 @@ theorem _root_.sum_mul_eq_sub_sub_integral_mul (ha : 0 ≤ a) (hab : a ≤ b)
   -- (Note we have 5 goals, but the 1st and 3rd are identical. TODO: find a non-hacky way of dealing
   -- with both at once.)
   · rw [intervalIntegrable_iff_integrableOn_Icc_of_le aux6]
-    exact (integrablemulsum c ha hf_int).mono_set (Set.Icc_subset_Icc_right aux5)
+    exact (integrableOn_mul_sum_Icc c ha hf_int).mono_set (Set.Icc_subset_Icc_right aux5)
   · rw [intervalIntegrable_iff_integrableOn_Icc_of_le aux5]
-    exact (integrablemulsum c ha hf_int).mono_set (Set.Icc_subset_Icc_left aux6)
+    exact (integrableOn_mul_sum_Icc c ha hf_int).mono_set (Set.Icc_subset_Icc_left aux6)
   · rw [intervalIntegrable_iff_integrableOn_Icc_of_le aux6]
-    exact (integrablemulsum c ha hf_int).mono_set (Set.Icc_subset_Icc_right aux5)
+    exact (integrableOn_mul_sum_Icc c ha hf_int).mono_set (Set.Icc_subset_Icc_right aux5)
   · rw [intervalIntegrable_iff_integrableOn_Icc_of_le aux3]
-    exact (integrablemulsum c ha hf_int).mono_set (Set.Icc_subset_Icc_right aux4)
+    exact (integrableOn_mul_sum_Icc c ha hf_int).mono_set (Set.Icc_subset_Icc_right aux4)
   · exact fun k hk ↦ (intervalIntegrable_iff_integrableOn_Icc_of_le (mod_cast k.le_succ)).mpr
-      <| (integrablemulsum c ha hf_int).mono_set
+      <| (integrableOn_mul_sum_Icc c ha hf_int).mono_set
         <| (Set.Icc_subset_Icc_iff (mod_cast k.le_succ)).mpr <| mod_cast (ineqofmemIco hk)
 
 /-- A version of `sum_mul_eq_sub_sub_integral_mul` where the endpoints are `Nat`. -/
@@ -209,7 +210,7 @@ theorem sum_mul_eq_sub_integral_mul₀ (hc : c 0 = 0) (b : ℝ)
       f b * (∑ k ∈ Icc 0 ⌊b⌋₊, c k) - ∫ t in Set.Ioc 1 b, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k := by
   obtain hb | hb := le_or_gt 1 b
   · have : 1 ≤ ⌊b⌋₊ := (Nat.one_le_floor_iff _).mpr hb
-    nth_rewrite 1 [Icc_eq_cons_Ioc (by omega), sum_cons, ← Nat.Icc_succ_left,
+    nth_rewrite 1 [Icc_eq_cons_Ioc (Nat.zero_le _), sum_cons, ← Nat.Icc_succ_left,
       Icc_eq_cons_Ioc (by omega), sum_cons]
     rw [Nat.succ_eq_add_one, zero_add, ← Nat.floor_one (α := ℝ),
       sum_mul_eq_sub_sub_integral_mul c zero_le_one hb hf_diff hf_int, Nat.floor_one, Nat.cast_one,
@@ -235,13 +236,14 @@ section limit
 
 open Filter Topology abelSummationProof intervalIntegral
 
-private theorem locallyintegrablemulsum (ha : 0 ≤ a) {g : ℝ → 𝕜} (hg : IntegrableOn g (Set.Ici a)) :
-    LocallyIntegrableOn (fun t ↦ g t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) (Set.Ici a) := by
+theorem locallyIntegrableOn_mul_sum_Icc {m : ℕ} (ha : 0 ≤ a) {g : ℝ → 𝕜}
+    (hg : IntegrableOn g (Set.Ici a)) :
+    LocallyIntegrableOn (fun t ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) (Set.Ici a) := by
   refine (locallyIntegrableOn_iff isLocallyClosed_Ici).mpr fun K hK₁ hK₂ ↦ ?_
   by_cases hK₃ : K.Nonempty
   · have h_inf : a ≤ sInf K := (hK₁ (hK₂.sInf_mem hK₃))
     refine IntegrableOn.mono_set ?_ (Bornology.IsBounded.subset_Icc_sInf_sSup hK₂.isBounded)
-    refine integrablemulsum _ (ha.trans h_inf) (hg.mono_set ?_)
+    refine integrableOn_mul_sum_Icc _ (ha.trans h_inf) (hg.mono_set ?_)
     exact (Set.Icc_subset_Ici_iff (Real.sInf_le_sSup _ hK₂.bddBelow hK₂.bddAbove)).mpr h_inf
   · rw [Set.not_nonempty_iff_eq_empty.mp hK₃]
     exact integrableOn_empty
@@ -259,7 +261,8 @@ theorem tendsto_sum_mul_atTop_nhds_one_sub_integral
     refine Tendsto.congr (fun _ ↦ by rw [← integral_of_le (Nat.cast_nonneg _)]) ?_
     refine intervalIntegral_tendsto_integral_Ioi _ ?_ tendsto_natCast_atTop_atTop
     exact integrableOn_Ici_iff_integrableOn_Ioi.mp
-      <| (locallyintegrablemulsum c le_rfl hf_int).integrableOn_of_isBigO_atTop hg_dom hg_int
+      <| (locallyIntegrableOn_mul_sum_Icc c le_rfl hf_int).integrableOn_of_isBigO_atTop
+        hg_dom hg_int
   refine (h_lim.sub h_lim').congr (fun _ ↦ ?_)
   rw [sum_mul_eq_sub_integral_mul' _ _ (fun t ht ↦ hf_diff _ ht.1)
     (hf_int.mono_set Set.Icc_subset_Ici_self)]
@@ -280,7 +283,8 @@ theorem tendsto_sum_mul_atTop_nhds_one_sub_integral₀ (hc : c 0 = 0)
       atTop (𝓝 (∫ t in Set.Ioi 1, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k)) := by
     refine Tendsto.congr' h (intervalIntegral_tendsto_integral_Ioi _ ?_ tendsto_natCast_atTop_atTop)
     exact integrableOn_Ici_iff_integrableOn_Ioi.mp
-      <| (locallyintegrablemulsum c zero_le_one hf_int).integrableOn_of_isBigO_atTop hg_dom hg_int
+      <| (locallyIntegrableOn_mul_sum_Icc c zero_le_one hf_int).integrableOn_of_isBigO_atTop
+        hg_dom hg_int
   refine (h_lim.sub h_lim').congr (fun _ ↦ ?_)
   rw [sum_mul_eq_sub_integral_mul₀' _ hc _ (fun t ht ↦ hf_diff _ ht.1)
     (hf_int.mono_set Set.Icc_subset_Ici_self)]
@@ -325,9 +329,10 @@ private theorem summable_mul_of_bigO_atTop_aux (m : ℕ)
       · exact add_le_add_left
           (le_trans (neg_le_abs _) (Real.norm_eq_abs _ ▸ norm_integral_le_integral_norm _)) _
       · refine add_le_add_left (setIntegral_mono_set ?_ ?_ Set.Ioc_subset_Ioi_self.eventuallyLE) C₁
-        · refine integrableOn_Ici_iff_integrableOn_Ioi.mp <|
+        · exact integrableOn_Ici_iff_integrableOn_Ioi.mp <|
             (integrable_norm_iff h_mes.aestronglyMeasurable).mpr <|
-              (locallyintegrablemulsum _ m.cast_nonneg hf_int).integrableOn_of_isBigO_atTop hg₁ hg₂
+              (locallyIntegrableOn_mul_sum_Icc _ m.cast_nonneg hf_int).integrableOn_of_isBigO_atTop
+                hg₁ hg₂
         · filter_upwards with t using norm_nonneg _
 
 theorem summable_mul_of_bigO_atTop

Mathlib/NumberTheory/LSeries/Basic.lean

@@ -68,6 +68,12 @@ lemma term_def (f : ℕ → ℂ) (s : ℂ) (n : ℕ) :
     term f s n = if n = 0 then 0 else f n / n ^ s :=
   rfl
 
+/-- An alternate spelling of `term_def` for the case `f 0 = 0`. -/
+lemma term_def₀ {f : ℕ → ℂ} (hf : f 0 = 0) (s : ℂ) (n : ℕ) :
+    LSeries.term f s n = f n * (n : ℂ) ^ (- s) := by
+  rw [LSeries.term]
+  split_ifs with h <;> simp [h, hf, cpow_neg, div_eq_inv_mul, mul_comm]
+
 @[simp]
 lemma term_zero (f : ℕ → ℂ) (s : ℂ) : term f s 0 = 0 := rfl