English
If there exists C with ∥f(n)∥ ≤ C n^{x-1} and Re(s) > x, then LSeriesSummable f s.
Русский
Если существует C и ∥f(n)∥ ≤ C n^{x-1} и Re(s) > x, то LSeriesSummable f s.
LaTeX
$$∃ C, ∀ n ≠ 0, ∥f(n)∥ ≤ C · n^{x-1} ∧ hs : x < s.re → LSeriesSummable(f,s)$$
Lean4
/-- If `f n` is bounded in absolute value by a constant times `n^(x-1)` and `re s > x`,
then the `LSeries` of `f` is summable at `s`. -/
theorem LSeriesSummable_of_le_const_mul_rpow {f : ℕ → ℂ} {x : ℝ} {s : ℂ} (hs : x < s.re)
(h : ∃ C, ∀ n ≠ 0, ‖f n‖ ≤ C * n ^ (x - 1)) : LSeriesSummable f s :=
by
obtain ⟨C, hC⟩ := h
have hC₀ : 0 ≤ C := (norm_nonneg <| f 1).trans <| by simpa using hC 1 one_ne_zero
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 (g := fun n ↦ (n : ℝ) ^ (-s.re + x - 1)) ?_ ?_
· simpa
· simp only [norm_norm, Filter.eventually_atTop]
refine ⟨1, fun n hn ↦ le_of_eq ?_⟩
simp only [norm_natCast_cpow_of_pos hn, add_re, sub_re, neg_re, ofReal_re, one_re]
ring_nf
refine Summable.of_norm <| hsum.of_nonneg_of_le (fun _ ↦ norm_nonneg _) (fun n ↦ ?_)
rcases n.eq_zero_or_pos with rfl | hn
· simpa only [term_zero, norm_zero] using norm_nonneg _
have hn' : 0 < (n : ℝ) ^ s.re := Real.rpow_pos_of_pos (Nat.cast_pos.mpr hn) _
simp_rw [term_of_ne_zero hn.ne', norm_div, norm_natCast_cpow_of_pos hn, div_le_iff₀ hn', norm_real,
Real.norm_of_nonneg hC₀, div_eq_mul_inv, mul_assoc, ← Real.rpow_neg <| Nat.cast_nonneg _, ←
Real.rpow_add <| Nat.cast_pos.mpr hn]
simpa using hC n <| Nat.pos_iff_ne_zero.mp hn
