f : ArithmeticFunction ℂ
m : ℝ
h : ∀ (n : ℕ), ↑Complex.abs (↑f n) ≤ m
z : ℂ
hz : 1 < z.re
⊢ LSeriesSummable f ↑z.re
f : ArithmeticFunction ℂ
m : ℝ
h : ∀ (n : ℕ), ↑Complex.abs (↑f n) ≤ m
z : ℂ
hz : 1 < z.re
⊢ LSeriesSummable f z
rw [← LSeriesSummable_iff_of_re_eq_re (Complex.ofReal_re z.re)]
f : ArithmeticFunction ℂ
m : ℝ
h : ∀ (n : ℕ), ↑Complex.abs (↑f n) ≤ m
z : ℂ
hz : 1 < z.re
⊢ 1 < z.re
f : ArithmeticFunction ℂ
m : ℝ
h : ∀ (n : ℕ), ↑Complex.abs (↑f n) ≤ m
z : ℂ
hz : 1 < z.re
⊢ LSeriesSummable f ↑z.re
apply LSeriesSummable_of_bounded_of_one_lt_real h
no goals
f : ArithmeticFunction ℂ
m : ℝ
h : ∀ (n : ℕ), ↑Complex.abs (↑f n) ≤ m
z : ℂ
hz : 1 < z.re
⊢ 1 < z.re
exact hz