feat(NumberTheory/LSeries/*): add material on convergence (#10728)

This continues a series of PRs on L-series.

Here we add `ArithmeticFunction.LSeriesHasSum` (in `NumberTheory.LSeries.Basic`) and `ArithmeticFunction.abscissaOfAbsConv` (in a new file `NumberTheory.LSeries.Convergence`), together with some results about these notions.

See [here](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/L-series/near/422275501) on Zulip.

Author: MichaelStollBayreuth

Mathlib.lean

@@ -2903,6 +2903,7 @@ import Mathlib.NumberTheory.FrobeniusNumber
 import Mathlib.NumberTheory.FunctionField
 import Mathlib.NumberTheory.KummerDedekind
 import Mathlib.NumberTheory.LSeries.Basic
+import Mathlib.NumberTheory.LSeries.Convergence
 import Mathlib.NumberTheory.LegendreSymbol.AddCharacter
 import Mathlib.NumberTheory.LegendreSymbol.Basic
 import Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Mathlib/NumberTheory/LSeries/Basic.lean

@@ -1,12 +1,11 @@
 /-
 Copyright (c) 2021 Aaron Anderson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Aaron Anderson
+Authors: Aaron Anderson, Michael Stoll
 -/
-import Mathlib.Analysis.NormedSpace.FiniteDimension
 import Mathlib.Analysis.PSeries
 import Mathlib.NumberTheory.ArithmeticFunction
-import Mathlib.Topology.Algebra.InfiniteSum.Basic
+import Mathlib.Analysis.NormedSpace.FiniteDimension
 
 #align_import number_theory.l_series from "leanprover-community/mathlib"@"32253a1a1071173b33dc7d6a218cf722c6feb514"
 
@@ -16,29 +15,44 @@ import Mathlib.Topology.Algebra.InfiniteSum.Basic
 Given an arithmetic function, we define the corresponding L-series.
 
 ## Main Definitions
+
  * `ArithmeticFunction.LSeries` is the `LSeries` with a given arithmetic function as its
   coefficients. This is not the analytic continuation, just the infinite series.
+
  * `ArithmeticFunction.LSeriesSummable` indicates that the `LSeries`
   converges at a given point.
 
+ * `ArithmeticFunction.LSeriesHasSum f s a` expresses that the L-series
+  of `f : ArithmeticFunction ℂ` converges (absolutely) at `s : ℂ` to `a : ℂ`.
+
 ## Main Results
- * `ArithmeticFunction.LSeriesSummable_of_bounded_of_one_lt_real`: the `LSeries` of a bounded
-  arithmetic function converges when `1 < z.re`.
+
+ * `ArithmeticFunction.LSeriesSummable_of_le_const_mul_rpow`: the `LSeries` of an
+  arithmetic function bounded by a constant times `n^(x-1)` converges at `s` when `x < s.re`.
+
  * `ArithmeticFunction.zeta_LSeriesSummable_iff_one_lt_re`: the `LSeries` of `ζ`
   (whose analytic continuation is the Riemann ζ) converges iff `1 < z.re`.
 
--/
+## Tags
+
+L-series, abscissa of convergence
 
+## TODO
+
+* Move `zeta_LSeriesSummable_iff_one_lt_r` to a new file on L-series of specific functions
+
+* Move `LSeries_add` to a new file on algebraic operations on L-series
+-/
 
-noncomputable section
 
 open scoped BigOperators
 
 namespace ArithmeticFunction
 
-open Nat
+open Complex Nat
 
 /-- The L-series of an `ArithmeticFunction`. -/
+noncomputable
 def LSeries (f : ArithmeticFunction ℂ) (z : ℂ) : ℂ :=
   ∑' n, f n / n ^ z
 #align nat.arithmetic_function.l_series ArithmeticFunction.LSeries
@@ -58,50 +72,136 @@ theorem LSeriesSummable_zero {z : ℂ} : LSeriesSummable 0 z := by
   simp [LSeriesSummable, summable_zero]
 #align nat.arithmetic_function.l_series_summable_zero ArithmeticFunction.LSeriesSummable_zero
 
-theorem LSeriesSummable_of_bounded_of_one_lt_real {f : ArithmeticFunction ℂ} {m : ℝ}
-    (h : ∀ n : ℕ, Complex.abs (f n) ≤ m) {z : ℝ} (hz : 1 < z) : f.LSeriesSummable z := by
-  by_cases h0 : m = 0
-  · subst h0
-    have hf : f = 0 := ArithmeticFunction.ext fun n =>
-      Complex.abs.eq_zero.1 (le_antisymm (h n) (Complex.abs.nonneg _))
-    simp [hf]
-  refine' .of_norm_bounded (fun n : ℕ => m / n ^ z) _ _
-  · simp_rw [div_eq_mul_inv]
-    exact (summable_mul_left_iff h0).2 (Real.summable_nat_rpow_inv.2 hz)
-  · intro n
-    have hm : 0 ≤ m := le_trans (Complex.abs.nonneg _) (h 0)
-    cases' n with n
-    · simp [hm, Real.zero_rpow (_root_.ne_of_gt (lt_trans Real.zero_lt_one hz))]
-    simp only [map_div₀, Complex.norm_eq_abs]
-    apply div_le_div hm (h _) (Real.rpow_pos_of_pos (Nat.cast_pos.2 n.succ_pos) _) (le_of_eq _)
-    rw [Complex.abs_cpow_real, Complex.abs_natCast]
-#align nat.arithmetic_function.l_series_summable_of_bounded_of_one_lt_real ArithmeticFunction.LSeriesSummable_of_bounded_of_one_lt_real
+/-- This states that the L-series of the arithmetic function `f` converges at `s` to `a`. -/
+def LSeriesHasSum (f : ArithmeticFunction ℂ) (s a : ℂ) : Prop :=
+  HasSum (fun (n : ℕ) => f n / n ^ s) a
+
+lemma LSeriesHasSum.LSeriesSummable {f : ArithmeticFunction ℂ} {s a : ℂ}
+    (h : LSeriesHasSum f s a) : LSeriesSummable f s :=
+  h.summable
+
+lemma LSeriesHasSum.LSeries_eq {f : ArithmeticFunction ℂ} {s a : ℂ}
+    (h : LSeriesHasSum f s a) : LSeries f s = a :=
+  h.tsum_eq
+
+lemma LSeriesSummable.LSeriesHasSum {f : ArithmeticFunction ℂ} {s : ℂ} (h : LSeriesSummable f s) :
+    LSeriesHasSum f s (LSeries f s) :=
+  h.hasSum
+
+lemma norm_LSeriesTerm_eq (f : ArithmeticFunction ℂ) (s : ℂ) (n : ℕ) :
+    ‖f n / n ^ s‖ = ‖f n‖ / n ^ s.re := by
+  rcases n.eq_zero_or_pos with rfl | hn
+  · simp only [map_zero, zero_div, norm_zero, zero_mul]
+  rw [norm_div, norm_natCast_cpow_of_pos hn]
+
+lemma norm_LSeriesTerm_le_of_re_le_re (f : ArithmeticFunction ℂ) {w : ℂ} {z : ℂ}
+    (h : w.re ≤ z.re) (n : ℕ) : ‖f n / n ^ z‖ ≤ ‖f n / n ^ w‖ := by
+  rcases n.eq_zero_or_pos with rfl | hn
+  · simp only [map_zero, CharP.cast_eq_zero, zero_div, norm_zero, le_refl]
+  have hn' := norm_natCast_cpow_pos_of_pos hn w
+  simp_rw [norm_div]
+  suffices H : ‖(n : ℂ) ^ w‖ ≤ ‖(n : ℂ) ^ z‖ from div_le_div (norm_nonneg _) le_rfl hn' H
+  refine (one_le_div hn').mp ?_
+  rw [← norm_div, ← cpow_sub _ _ <| cast_ne_zero.mpr hn.ne', norm_natCast_cpow_of_pos hn]
+  exact Real.one_le_rpow (one_le_cast.mpr hn) <| by simp only [sub_re, sub_nonneg, h]
+
+lemma LSeriesSummable.of_re_le_re {f : ArithmeticFunction ℂ} {w : ℂ} {z : ℂ} (h : w.re ≤ z.re)
+    (hf : LSeriesSummable f w) : LSeriesSummable f z := by
+  rw [LSeriesSummable, ← summable_norm_iff] at hf ⊢
+  exact hf.of_nonneg_of_le (fun _ ↦ norm_nonneg _) (norm_LSeriesTerm_le_of_re_le_re f h)
 
 theorem LSeriesSummable_iff_of_re_eq_re {f : ArithmeticFunction ℂ} {w z : ℂ} (h : w.re = z.re) :
-    f.LSeriesSummable w ↔ f.LSeriesSummable z := by
-  suffices h : ∀ n : ℕ,
-      Complex.abs (f n) / Complex.abs (↑n ^ w) = Complex.abs (f n) / Complex.abs (↑n ^ z) by
-    simp [LSeriesSummable, ← summable_norm_iff, h, Complex.norm_eq_abs]
-  intro n
-  cases' n with n; · simp
-  apply congr rfl
-  have h0 : (n.succ : ℂ) ≠ 0 := by
-    rw [Ne.def, Nat.cast_eq_zero]
-    apply n.succ_ne_zero
-  rw [Complex.cpow_def, Complex.cpow_def, if_neg h0, if_neg h0, Complex.abs_exp_eq_iff_re_eq]
-  simp only [h, Complex.mul_re, mul_eq_mul_left_iff, sub_right_inj]
-  right
-  rw [Complex.log_im, ← Complex.ofReal_nat_cast]
-  exact Complex.arg_ofReal_of_nonneg (le_of_lt (cast_pos.2 n.succ_pos))
+    f.LSeriesSummable w ↔ f.LSeriesSummable z :=
+  ⟨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 ArithmeticFunction.LSeriesSummable_iff_of_re_eq_re
 
+lemma LSeriesSummable.le_const_mul_rpow {f : ArithmeticFunction ℂ} {s : ℂ}
+    (h : LSeriesSummable f s) : ∃ C, ∀ n, ‖f n‖ ≤ C * n ^ s.re := by
+  replace h := h.norm
+  by_contra! H
+  obtain ⟨n, hn⟩ := H (tsum fun n ↦ ‖f n / n ^ s‖)
+  have hn₀ : 0 < n := by
+    refine n.eq_zero_or_pos.resolve_left ?_
+    rintro rfl
+    rw [map_zero, norm_zero, Nat.cast_zero, mul_neg_iff] at hn
+    replace hn := hn.resolve_left <| fun hh ↦ hh.2.not_le <| Real.rpow_nonneg (le_refl 0) s.re
+    exact hn.1.not_le <| tsum_nonneg (fun _ ↦ norm_nonneg _)
+  have := le_tsum h n fun _ _ ↦ norm_nonneg _
+  rw [norm_LSeriesTerm_eq, div_le_iff <| Real.rpow_pos_of_pos (Nat.cast_pos.mpr hn₀) _] at this
+  exact (this.trans_lt hn).false.elim
+
+open Filter in
+lemma LSeriesSummable.isBigO_rpow {f : ArithmeticFunction ℂ} {s : ℂ}
+    (h : LSeriesSummable f s) : f =O[atTop] fun n ↦ (n : ℝ) ^ s.re := by
+  obtain ⟨C, hC⟩ := h.le_const_mul_rpow
+  refine Asymptotics.IsBigO.of_bound C ?_
+  convert eventually_of_forall hC using 4 with n
+  have hn₀ : (0 : ℝ) ≤ n := Nat.cast_nonneg _
+  rw [Real.norm_eq_abs, Real.abs_rpow_of_nonneg hn₀, _root_.abs_of_nonneg hn₀]
+
+lemma LSeriesSummable_of_le_const_mul_rpow {f : ArithmeticFunction ℂ} {x : ℝ} {s : ℂ}
+    (hs : x < s.re) (h : ∃ C, ∀ n, ‖f n‖ ≤ C * n ^ (x - 1)) :
+    LSeriesSummable f s := by
+  obtain ⟨C, hC⟩ := h
+  have hC₀ : 0 ≤ C := by
+    specialize hC 1
+    simp only [cast_one, Real.one_rpow, mul_one] at hC
+    exact (norm_nonneg _).trans hC
+  have hsum : Summable fun n : ℕ ↦ ‖(C : ℂ) / n ^ (s + (1 - x))‖ := by
+    simp_rw [div_eq_mul_inv, norm_mul, ← cpow_neg]
+    have hsx : -s.re + x - 1 < -1 := by linarith only [hs]
+    refine Summable.mul_left _ <|
+      Summable.of_norm_bounded_eventually_nat (fun n ↦ (n : ℝ) ^ (-s.re + x - 1)) ?_ ?_
+    · simp only [Real.summable_nat_rpow, hsx]
+    · simp only [neg_add_rev, neg_sub, norm_norm, Filter.eventually_atTop]
+      refine ⟨1, fun n hn ↦ ?_⟩
+      simp only [norm_natCast_cpow_of_pos hn, add_re, sub_re, neg_re, ofReal_re, one_re]
+      convert le_refl ?_ using 2
+      ring
+  refine Summable.of_norm <| hsum.of_nonneg_of_le (fun _ ↦ norm_nonneg _) (fun n ↦ ?_)
+  rcases n.eq_zero_or_pos with rfl | hn
+  · simp only [map_zero, zero_div, norm_zero, norm_nonneg]
+  have hn' : 0 < (n : ℝ) ^ s.re := Real.rpow_pos_of_pos (Nat.cast_pos.mpr hn) _
+  simp_rw [norm_div, norm_natCast_cpow_of_pos hn, div_le_iff hn', add_re, sub_re, one_re,
+    ofReal_re, Real.rpow_add <| Nat.cast_pos.mpr hn, div_eq_mul_inv, mul_inv]
+  rw [mul_assoc, mul_comm _ ((n : ℝ) ^ s.re), ← mul_assoc ((n : ℝ) ^ s.re), mul_inv_cancel hn'.ne',
+    ← Real.rpow_neg n.cast_nonneg, norm_eq_abs (C : ℂ), abs_ofReal, _root_.abs_of_nonneg hC₀,
+    neg_sub, one_mul]
+  exact hC n
+
+open Filter Finset Real Nat in
+lemma LSeriesSummable_of_isBigO_rpow {f : ArithmeticFunction ℂ} {x : ℝ} {s : ℂ}
+    (hs : x < s.re) (h : f =O[atTop] fun n ↦ (n : ℝ) ^ (x - 1)) :
+    LSeriesSummable f s := by
+  obtain ⟨C, hC⟩ := Asymptotics.isBigO_iff.mp h
+  obtain ⟨m, hm⟩ := eventually_atTop.mp hC
+  let C' := max C (max' (insert 0 (image (fun n : ℕ ↦ ‖f n‖ / (n : ℝ) ^ (x - 1)) (range m)))
+    (insert_nonempty 0 _))
+  have hC'₀ : 0 ≤ C' := (le_max' _ _ (mem_insert.mpr (Or.inl rfl))).trans <| le_max_right ..
+  have hCC' : C ≤ C' := le_max_left ..
+  refine LSeriesSummable_of_le_const_mul_rpow hs ⟨C', fun n ↦ ?_⟩
+  rcases le_or_lt m n with hn | hn
+  · refine (hm n hn).trans ?_
+    have hn₀ : (0 : ℝ) ≤ n := cast_nonneg _
+    gcongr
+    rw [Real.norm_eq_abs, abs_rpow_of_nonneg hn₀, _root_.abs_of_nonneg hn₀]
+  · rcases n.eq_zero_or_pos with rfl | hn'
+    · simpa only [map_zero, norm_zero, cast_zero] using mul_nonneg hC'₀ <| zero_rpow_nonneg _
+    refine (div_le_iff <| rpow_pos_of_pos (cast_pos.mpr hn') _).mp ?_
+    refine (le_max' _ _ <| mem_insert_of_mem ?_).trans <| le_max_right ..
+    exact mem_image.mpr ⟨n, mem_range.mpr hn, rfl⟩
+
 theorem LSeriesSummable_of_bounded_of_one_lt_re {f : ArithmeticFunction ℂ} {m : ℝ}
     (h : ∀ n : ℕ, Complex.abs (f n) ≤ m) {z : ℂ} (hz : 1 < z.re) : f.LSeriesSummable z := by
-  rw [← LSeriesSummable_iff_of_re_eq_re (Complex.ofReal_re z.re)]
-  apply LSeriesSummable_of_bounded_of_one_lt_real h
-  exact hz
+  refine LSeriesSummable_of_le_const_mul_rpow hz ⟨m, fun n ↦ ?_⟩
+  simp only [norm_eq_abs, sub_self, Real.rpow_zero, mul_one, h n]
 #align nat.arithmetic_function.l_series_summable_of_bounded_of_one_lt_re ArithmeticFunction.LSeriesSummable_of_bounded_of_one_lt_re
 
+theorem LSeriesSummable_of_bounded_of_one_lt_real {f : ArithmeticFunction ℂ} {m : ℝ}
+    (h : ∀ n : ℕ, Complex.abs (f n) ≤ m) {z : ℝ} (hz : 1 < z) : f.LSeriesSummable z :=
+  LSeriesSummable_of_bounded_of_one_lt_re h <| by simp only [ofReal_re, hz]
+#align nat.arithmetic_function.l_series_summable_of_bounded_of_one_lt_real ArithmeticFunction.LSeriesSummable_of_bounded_of_one_lt_real
+
 open scoped ArithmeticFunction
 
 theorem zeta_LSeriesSummable_iff_one_lt_re {z : ℂ} : LSeriesSummable ζ z ↔ 1 < z.re := by

Mathlib/NumberTheory/LSeries/Convergence.lean

@@ -0,0 +1,111 @@
+/-
+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.NumberTheory.LSeries.Basic
+import Mathlib.Data.Real.EReal
+
+/-!
+# Convergence of L-series
+
+We define `ArithmeticFunction.abscissaOfAbsConv f` (as an `EReal`) to be the infimum
+of all real numbers `x` such that the L-series of `f` converges for complex arguments with
+real part `x` and provide some results about it.
+
+## Tags
+
+L-series, abscissa of convergence
+-/
+
+namespace ArithmeticFunction
+
+open Complex Nat
+
+/-- The abscissa `x : EReal` of absolute convergence of the L-series associated to `f`:
+the series converges absolutely at `s` when `re s > x` and does not converge absolutely
+when `re s < x`. -/
+noncomputable def abscissaOfAbsConv (f : ArithmeticFunction ℂ) : EReal :=
+  sInf <| Real.toEReal '' {x : ℝ | LSeriesSummable f x}
+
+lemma LSeriesSummable_of_abscissaOfAbsConv_lt_re {f : ArithmeticFunction ℂ} {s : ℂ}
+    (hs : abscissaOfAbsConv f < s.re) : LSeriesSummable f s := by
+  simp only [abscissaOfAbsConv, sInf_lt_iff, Set.mem_image, Set.mem_setOf_eq,
+    exists_exists_and_eq_and, EReal.coe_lt_coe_iff] at hs
+  obtain ⟨y, hy, hys⟩ := hs
+  exact hy.of_re_le_re <| ofReal_re y ▸ hys.le
+
+lemma LSeriesSummable_lt_re_of_abscissaOfAbsConv_lt_re {f : ArithmeticFunction ℂ} {s : ℂ}
+    (hs : abscissaOfAbsConv f < s.re) :
+    ∃ x : ℝ, x < s.re ∧ LSeriesSummable f x := by
+  obtain ⟨x, hx₁, hx₂⟩ := EReal.exists_between_coe_real hs
+  exact ⟨x, EReal.coe_lt_coe_iff.mp hx₂, LSeriesSummable_of_abscissaOfAbsConv_lt_re hx₁⟩
+
+lemma LSeriesSummable.abscissaOfAbsConv_le {f : ArithmeticFunction ℂ} {s : ℂ}
+    (h : LSeriesSummable f s) : abscissaOfAbsConv f ≤ s.re := by
+  refine sInf_le <| Membership.mem.out ?_
+  simp only [Set.mem_setOf_eq, Set.mem_image, EReal.coe_eq_coe_iff, exists_eq_right]
+  exact h.of_re_le_re <| by simp only [ofReal_re, le_refl]
+
+lemma abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable {f : ArithmeticFunction ℂ} {x : ℝ}
+    (h : ∀ y : ℝ, x < y → LSeriesSummable f y) :
+    abscissaOfAbsConv f ≤ x := by
+  refine sInf_le_iff.mpr fun y hy ↦ ?_
+  simp only [mem_lowerBounds, Set.mem_image, Set.mem_setOf_eq, forall_exists_index, and_imp,
+    forall_apply_eq_imp_iff₂] at hy
+  have H (a : EReal) : x < a → y ≤ a := by
+    induction' a using EReal.rec with a₀
+    · simp only [not_lt_bot, le_bot_iff, IsEmpty.forall_iff]
+    · exact_mod_cast fun ha ↦ hy a₀ (h a₀ ha)
+    · simp only [EReal.coe_lt_top, le_top, forall_true_left]
+  exact Set.Ioi_subset_Ici_iff.mp H
+
+lemma abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable' {f : ArithmeticFunction ℂ} {x : EReal}
+    (h : ∀ y : ℝ, x < y → LSeriesSummable f y) :
+    abscissaOfAbsConv f ≤ x := by
+  induction' x using EReal.rec with y
+  · refine le_of_eq <| sInf_eq_bot.mpr fun y hy ↦ ?_
+    induction' y using EReal.rec with z
+    · simp only [gt_iff_lt, lt_self_iff_false] at hy
+    · exact ⟨z - 1,  ⟨z-1, h (z - 1) <| EReal.bot_lt_coe _, rfl⟩, by norm_cast; exact sub_one_lt z⟩
+    · exact ⟨0, ⟨0, h 0 <| EReal.bot_lt_coe 0, rfl⟩, EReal.zero_lt_top⟩
+  · exact abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable <| by exact_mod_cast h
+  · exact le_top
+
+/-- If `‖f n‖` is bounded by a constant times `n^x`, then the abscissa of absolute convergence
+of `f` is bounded by `x + 1`. -/
+lemma abscissaOfAbsConv_le_of_le_const_mul_rpow {f : ArithmeticFunction ℂ} {x : ℝ}
+    (h : ∃ C, ∀ n, ‖f n‖ ≤ C * n ^ x) : abscissaOfAbsConv f ≤ x + 1 := by
+  rw [show x = x + 1 - 1 by ring] at h
+  by_contra! H
+  obtain ⟨y, hy₁, hy₂⟩ := EReal.exists_between_coe_real H
+  exact (LSeriesSummable_of_le_const_mul_rpow (s := y) (EReal.coe_lt_coe_iff.mp hy₁) h
+    |>.abscissaOfAbsConv_le.trans_lt hy₂).false
+
+open Filter in
+/-- If `‖f n‖` is `O(n^x)`, then the abscissa of absolute convergence
+of `f` is bounded by `x + 1`. -/
+lemma abscissaOfAbsConv_le_of_isBigO_rpow {f : ArithmeticFunction ℂ} {x : ℝ}
+    (h : f =O[atTop] fun n ↦ (n : ℝ) ^ x) : abscissaOfAbsConv f ≤ x + 1 := by
+  rw [show x = x + 1 - 1 by ring] at h
+  by_contra! H
+  obtain ⟨y, hy₁, hy₂⟩ := EReal.exists_between_coe_real H
+  exact (LSeriesSummable_of_isBigO_rpow (s := y) (EReal.coe_lt_coe_iff.mp hy₁) h
+    |>.abscissaOfAbsConv_le.trans_lt hy₂).false
+
+/-- If `f` is bounded, then the abscissa of absolute convergence of `f` is bounded above by `1`. -/
+lemma abscissaOfAbsConv_le_of_le_const {f : ArithmeticFunction ℂ}
+    (h : ∃ C, ∀ n, ‖f n‖ ≤ C) : abscissaOfAbsConv f ≤ 1 := by
+  convert abscissaOfAbsConv_le_of_le_const_mul_rpow (x := 0) ?_
+  · norm_num
+  · simpa only [norm_eq_abs, Real.rpow_zero, mul_one] using h
+
+open Filter in
+/-- If `f` is `O(1)`, then the abscissa of absolute convergence of `f` is bounded above by `1`. -/
+lemma abscissaOfAbsConv_le_one_of_isBigO_one {f : ArithmeticFunction ℂ}
+    (h : f =O[atTop] fun _ ↦ (1 : ℝ)) : abscissaOfAbsConv f ≤ 1 := by
+  convert abscissaOfAbsConv_le_of_isBigO_rpow (x := 0) ?_
+  · norm_num
+  · simpa only [Real.rpow_zero] using h
+
+end ArithmeticFunction