English
If f = O(n^{x-1}) and Re(s) > x, then LSeriesSummable f s.
Русский
Если f = O(n^{x-1}) и Re(s) > x, тогда LSeriesSummable f s.
LaTeX
$$Real.instLT.lt x s.re ∧ (f =O[atTop] n^{x-1}) → LSeriesSummable f s$$
Lean4
/-- If `f = O(n^(x-1))` and `re s > x`, then the `LSeries` of `f` is summable at `s`. -/
theorem LSeriesSummable_of_isBigO_rpow {f : ℕ → ℂ} {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 hn₀ ↦ ?_⟩
rcases le_or_gt 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₀, abs_of_nonneg hn₀]
· have hn' : 0 < n := Nat.pos_of_ne_zero hn₀
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⟩
