case pos
f : ArithmeticFunction ℂ
m : ℝ
h : ∀ (n : ℕ), ↑Complex.abs (↑f n) ≤ m
z : ℝ
hz : 1 < z
h0 : m = 0
⊢ LSeriesSummable f ↑z

case neg
f : ArithmeticFunction ℂ
m : ℝ
h : ∀ (n : ℕ), ↑Complex.abs (↑f n) ≤ m
z : ℝ
hz : 1 < z
h0 : ¬m = 0
⊢ LSeriesSummable f ↑z
f : ArithmeticFunction ℂ
m : ℝ
h : ∀ (n : ℕ), ↑Complex.abs (↑f n) ≤ m
z : ℝ
hz : 1 < z
⊢ LSeriesSummable f ↑z
by_cases h0 : m = 0
case neg.refine'_1
f : ArithmeticFunction ℂ
m : ℝ
h : ∀ (n : ℕ), ↑Complex.abs (↑f n) ≤ m
z : ℝ
hz : 1 < z
h0 : ¬m = 0
⊢ Summable fun n => m / ↑n ^ z

case neg.refine'_2
f : ArithmeticFunction ℂ
m : ℝ
h : ∀ (n : ℕ), ↑Complex.abs (↑f n) ≤ m
z : ℝ
hz : 1 < z
h0 : ¬m = 0
⊢ ∀ (i : ℕ), ‖↑f i / ↑i ^ ↑z‖ ≤ (fun n => m / ↑n ^ z) i
case neg
f : ArithmeticFunction ℂ
m : ℝ
h : ∀ (n : ℕ), ↑Complex.abs (↑f n) ≤ m
z : ℝ
hz : 1 < z
h0 : ¬m = 0
⊢ LSeriesSummable f ↑z
refine' summable_of_norm_bounded (fun n : ℕ => m / n ^ z) _ _
case pos
f : ArithmeticFunction ℂ
z : ℝ
hz : 1 < z
h : ∀ (n : ℕ), ↑Complex.abs (↑f n) ≤ 0
⊢ LSeriesSummable f ↑z
case pos
f : ArithmeticFunction ℂ
m : ℝ
h : ∀ (n : ℕ), ↑Complex.abs (↑f n) ≤ m
z : ℝ
hz : 1 < z
h0 : m = 0
⊢ LSeriesSummable f ↑z
subst h0
case pos
f : ArithmeticFunction ℂ
z : ℝ
hz : 1 < z
h : ∀ (n : ℕ), ↑Complex.abs (↑f n) ≤ 0
hf : f = 0
⊢ LSeriesSummable f ↑z
case pos
f : ArithmeticFunction ℂ
z : ℝ
hz : 1 < z
h : ∀ (n : ℕ), ↑Complex.abs (↑f n) ≤ 0
⊢ LSeriesSummable f ↑z
have hf : f = 0 := ArithmeticFunction.ext fun n =>
  Complex.abs.eq_zero.1 (le_antisymm (h n) (Complex.abs.nonneg _))
no goals
case pos
f : ArithmeticFunction ℂ
z : ℝ
hz : 1 < z
h : ∀ (n : ℕ), ↑Complex.abs (↑f n) ≤ 0
hf : f = 0
⊢ LSeriesSummable f ↑z
simp [hf]
case neg.refine'_1
f : ArithmeticFunction ℂ
m : ℝ
h : ∀ (n : ℕ), ↑Complex.abs (↑f n) ≤ m
z : ℝ
hz : 1 < z
h0 : ¬m = 0
⊢ Summable fun n => m * (↑n ^ z)⁻¹
case neg.refine'_1
f : ArithmeticFunction ℂ
m : ℝ
h : ∀ (n : ℕ), ↑Complex.abs (↑f n) ≤ m
z : ℝ
hz : 1 < z
h0 : ¬m = 0
⊢ Summable fun n => m / ↑n ^ z
simp_rw [div_eq_mul_inv]
no goals
case neg.refine'_1
f : ArithmeticFunction ℂ
m : ℝ
h : ∀ (n : ℕ), ↑Complex.abs (↑f n) ≤ m
z : ℝ
hz : 1 < z
h0 : ¬m = 0
⊢ Summable fun n => m * (↑n ^ z)⁻¹
exact (summable_mul_left_iff h0).2 (Real.summable_nat_rpow_inv.2 hz)
case neg.refine'_2
f : ArithmeticFunction ℂ
m : ℝ
h : ∀ (n : ℕ), ↑Complex.abs (↑f n) ≤ m
z : ℝ
hz : 1 < z
h0 : ¬m = 0
n : ℕ
⊢ ‖↑f n / ↑n ^ ↑z‖ ≤ (fun n => m / ↑n ^ z) n
case neg.refine'_2
f : ArithmeticFunction ℂ
m : ℝ
h : ∀ (n : ℕ), ↑Complex.abs (↑f n) ≤ m
z : ℝ
hz : 1 < z
h0 : ¬m = 0
⊢ ∀ (i : ℕ), ‖↑f i / ↑i ^ ↑z‖ ≤ (fun n => m / ↑n ^ z) i
intro n
case neg.refine'_2
f : ArithmeticFunction ℂ
m : ℝ
h : ∀ (n : ℕ), ↑Complex.abs (↑f n) ≤ m
z : ℝ
hz : 1 < z
h0 : ¬m = 0
n : ℕ
hm : 0 ≤ m
⊢ ‖↑f n / ↑n ^ ↑z‖ ≤ (fun n => m / ↑n ^ z) n
case neg.refine'_2
f : ArithmeticFunction ℂ
m : ℝ
h : ∀ (n : ℕ), ↑Complex.abs (↑f n) ≤ m
z : ℝ
hz : 1 < z
h0 : ¬m = 0
n : ℕ
⊢ ‖↑f n / ↑n ^ ↑z‖ ≤ (fun n => m / ↑n ^ z) n
have hm : 0 ≤ m := le_trans (Complex.abs.nonneg _) (h 0)
case neg.refine'_2.zero
f : ArithmeticFunction ℂ
m : ℝ
h : ∀ (n : ℕ), ↑Complex.abs (↑f n) ≤ m
z : ℝ
hz : 1 < z
h0 : ¬m = 0
hm : 0 ≤ m
⊢ ‖↑f Nat.zero / ↑Nat.zero ^ ↑z‖ ≤ (fun n => m / ↑n ^ z) Nat.zero

case neg.refine'_2.succ
f : ArithmeticFunction ℂ
m : ℝ
h : ∀ (n : ℕ), ↑Complex.abs (↑f n) ≤ m
z : ℝ
hz : 1 < z
h0 : ¬m = 0
hm : 0 ≤ m
n : ℕ
⊢ ‖↑f (succ n) / ↑(succ n) ^ ↑z‖ ≤ (fun n => m / ↑n ^ z) (succ n)
case neg.refine'_2
f : ArithmeticFunction ℂ
m : ℝ
h : ∀ (n : ℕ), ↑Complex.abs (↑f n) ≤ m
z : ℝ
hz : 1 < z
h0 : ¬m = 0
n : ℕ
hm : 0 ≤ m
⊢ ‖↑f n / ↑n ^ ↑z‖ ≤ (fun n => m / ↑n ^ z) n
cases' n with n
case neg.refine'_2.succ
f : ArithmeticFunction ℂ
m : ℝ
h : ∀ (n : ℕ), ↑Complex.abs (↑f n) ≤ m
z : ℝ
hz : 1 < z
h0 : ¬m = 0
hm : 0 ≤ m
n : ℕ
⊢ ↑Complex.abs (↑f (succ n)) / ↑Complex.abs (↑(succ n) ^ ↑z) ≤ m / ↑(succ n) ^ z
case neg.refine'_2.succ
f : ArithmeticFunction ℂ
m : ℝ
h : ∀ (n : ℕ), ↑Complex.abs (↑f n) ≤ m
z : ℝ
hz : 1 < z
h0 : ¬m = 0
hm : 0 ≤ m
n : ℕ
⊢ ‖↑f (succ n) / ↑(succ n) ^ ↑z‖ ≤ (fun n => m / ↑n ^ z) (succ n)
simp only [map_div₀, Complex.norm_eq_abs]
f : ArithmeticFunction ℂ
m : ℝ
h : ∀ (n : ℕ), ↑Complex.abs (↑f n) ≤ m
z : ℝ
hz : 1 < z
h0 : ¬m = 0
hm : 0 ≤ m
n : ℕ
⊢ ↑(succ n) ^ z = ↑Complex.abs (↑(succ n) ^ ↑z)
case neg.refine'_2.succ
f : ArithmeticFunction ℂ
m : ℝ
h : ∀ (n : ℕ), ↑Complex.abs (↑f n) ≤ m
z : ℝ
hz : 1 < z
h0 : ¬m = 0
hm : 0 ≤ m
n : ℕ
⊢ ↑Complex.abs (↑f (succ n)) / ↑Complex.abs (↑(succ n) ^ ↑z) ≤ m / ↑(succ n) ^ z
apply div_le_div hm (h _) (Real.rpow_pos_of_pos (Nat.cast_pos.2 n.succ_pos) _) (le_of_eq _)
no goals
f : ArithmeticFunction ℂ
m : ℝ
h : ∀ (n : ℕ), ↑Complex.abs (↑f n) ≤ m
z : ℝ
hz : 1 < z
h0 : ¬m = 0
hm : 0 ≤ m
n : ℕ
⊢ ↑(succ n) ^ z = ↑Complex.abs (↑(succ n) ^ ↑z)
rw [Complex.abs_cpow_real, Complex.abs_cast_nat]
no goals
case neg.refine'_2.zero
f : ArithmeticFunction ℂ
m : ℝ
h : ∀ (n : ℕ), ↑Complex.abs (↑f n) ≤ m
z : ℝ
hz : 1 < z
h0 : ¬m = 0
hm : 0 ≤ m
⊢ ‖↑f Nat.zero / ↑Nat.zero ^ ↑z‖ ≤ (fun n => m / ↑n ^ z) Nat.zero
simp [hm, Real.zero_rpow (_root_.ne_of_gt (lt_trans Real.zero_lt_one hz))]