f : ArithmeticFunction ℂ
w z : ℂ
h✝ : w.re = z.re
h : ∀ (n : ℕ), ↑Complex.abs (↑f n) / ↑Complex.abs (↑n ^ w) = ↑Complex.abs (↑f n) / ↑Complex.abs (↑n ^ z)
⊢ LSeriesSummable f w ↔ LSeriesSummable f z

case h
f : ArithmeticFunction ℂ
w z : ℂ
h : w.re = z.re
⊢ ∀ (n : ℕ), ↑Complex.abs (↑f n) / ↑Complex.abs (↑n ^ w) = ↑Complex.abs (↑f n) / ↑Complex.abs (↑n ^ z)
f : ArithmeticFunction ℂ
w z : ℂ
h : w.re = z.re
⊢ LSeriesSummable f w ↔ LSeriesSummable f z
suffices h :
  ∀ n : ℕ, Complex.abs (f n) / Complex.abs (↑n ^ w) = Complex.abs (f n) / Complex.abs (↑n ^ z)
case h
f : ArithmeticFunction ℂ
w z : ℂ
h : w.re = z.re
n : ℕ
⊢ ↑Complex.abs (↑f n) / ↑Complex.abs (↑n ^ w) = ↑Complex.abs (↑f n) / ↑Complex.abs (↑n ^ z)
case h
f : ArithmeticFunction ℂ
w z : ℂ
h : w.re = z.re
⊢ ∀ (n : ℕ), ↑Complex.abs (↑f n) / ↑Complex.abs (↑n ^ w) = ↑Complex.abs (↑f n) / ↑Complex.abs (↑n ^ z)
intro n
case h.zero
f : ArithmeticFunction ℂ
w z : ℂ
h : w.re = z.re
⊢ ↑Complex.abs (↑f Nat.zero) / ↑Complex.abs (↑Nat.zero ^ w) = ↑Complex.abs (↑f Nat.zero) / ↑Complex.abs (↑Nat.zero ^ z)

case h.succ
f : ArithmeticFunction ℂ
w z : ℂ
h : w.re = z.re
n : ℕ
⊢ ↑Complex.abs (↑f (succ n)) / ↑Complex.abs (↑(succ n) ^ w) = ↑Complex.abs (↑f (succ n)) / ↑Complex.abs (↑(succ n) ^ z)
case h
f : ArithmeticFunction ℂ
w z : ℂ
h : w.re = z.re
n : ℕ
⊢ ↑Complex.abs (↑f n) / ↑Complex.abs (↑n ^ w) = ↑Complex.abs (↑f n) / ↑Complex.abs (↑n ^ z)
cases' n with n
case h.succ
f : ArithmeticFunction ℂ
w z : ℂ
h : w.re = z.re
n : ℕ
⊢ ↑Complex.abs (↑(succ n) ^ w) = ↑Complex.abs (↑(succ n) ^ z)
case h.succ
f : ArithmeticFunction ℂ
w z : ℂ
h : w.re = z.re
n : ℕ
⊢ ↑Complex.abs (↑f (succ n)) / ↑Complex.abs (↑(succ n) ^ w) = ↑Complex.abs (↑f (succ n)) / ↑Complex.abs (↑(succ n) ^ z)
apply congr rfl
case h.succ
f : ArithmeticFunction ℂ
w z : ℂ
h : w.re = z.re
n : ℕ
h0 : ↑(succ n) ≠ 0
⊢ ↑Complex.abs (↑(succ n) ^ w) = ↑Complex.abs (↑(succ n) ^ z)
case h.succ
f : ArithmeticFunction ℂ
w z : ℂ
h : w.re = z.re
n : ℕ
⊢ ↑Complex.abs (↑(succ n) ^ w) = ↑Complex.abs (↑(succ n) ^ z)
have h0 : (n.succ : ℂ) ≠ 0 := by
  rw [Ne.def, Nat.cast_eq_zero]
  apply n.succ_ne_zero
case h.succ
f : ArithmeticFunction ℂ
w z : ℂ
h : w.re = z.re
n : ℕ
h0 : ↑(succ n) ≠ 0
⊢ (Complex.log ↑(succ n) * w).re = (Complex.log ↑(succ n) * z).re
case h.succ
f : ArithmeticFunction ℂ
w z : ℂ
h : w.re = z.re
n : ℕ
h0 : ↑(succ n) ≠ 0
⊢ ↑Complex.abs (↑(succ n) ^ w) = ↑Complex.abs (↑(succ n) ^ z)
rw [Complex.cpow_def, Complex.cpow_def, if_neg h0, if_neg h0, Complex.abs_exp_eq_iff_re_eq]
case h.succ
f : ArithmeticFunction ℂ
w z : ℂ
h : w.re = z.re
n : ℕ
h0 : ↑(succ n) ≠ 0
⊢ w.im = z.im ∨ (Complex.log ↑(succ n)).im = 0
case h.succ
f : ArithmeticFunction ℂ
w z : ℂ
h : w.re = z.re
n : ℕ
h0 : ↑(succ n) ≠ 0
⊢ (Complex.log ↑(succ n) * w).re = (Complex.log ↑(succ n) * z).re
simp only [h, Complex.mul_re, mul_eq_mul_left_iff, sub_right_inj]
case h.succ.h
f : ArithmeticFunction ℂ
w z : ℂ
h : w.re = z.re
n : ℕ
h0 : ↑(succ n) ≠ 0
⊢ (Complex.log ↑(succ n)).im = 0
case h.succ
f : ArithmeticFunction ℂ
w z : ℂ
h : w.re = z.re
n : ℕ
h0 : ↑(succ n) ≠ 0
⊢ w.im = z.im ∨ (Complex.log ↑(succ n)).im = 0
right
case h.succ.h
f : ArithmeticFunction ℂ
w z : ℂ
h : w.re = z.re
n : ℕ
h0 : ↑(succ n) ≠ 0
⊢ Complex.arg ↑↑(succ n) = 0
case h.succ.h
f : ArithmeticFunction ℂ
w z : ℂ
h : w.re = z.re
n : ℕ
h0 : ↑(succ n) ≠ 0
⊢ (Complex.log ↑(succ n)).im = 0
rw [Complex.log_im, ← Complex.ofReal_nat_cast]
no goals
case h.succ.h
f : ArithmeticFunction ℂ
w z : ℂ
h : w.re = z.re
n : ℕ
h0 : ↑(succ n) ≠ 0
⊢ Complex.arg ↑↑(succ n) = 0
exact Complex.arg_ofReal_of_nonneg (le_of_lt (cast_pos.2 n.succ_pos))
no goals
f : ArithmeticFunction ℂ
w z : ℂ
h✝ : w.re = z.re
h : ∀ (n : ℕ), ↑Complex.abs (↑f n) / ↑Complex.abs (↑n ^ w) = ↑Complex.abs (↑f n) / ↑Complex.abs (↑n ^ z)
⊢ LSeriesSummable f w ↔ LSeriesSummable f z
simp [LSeriesSummable, ← summable_norm_iff, h, Complex.norm_eq_abs]
no goals
case h.zero
f : ArithmeticFunction ℂ
w z : ℂ
h : w.re = z.re
⊢ ↑Complex.abs (↑f Nat.zero) / ↑Complex.abs (↑Nat.zero ^ w) = ↑Complex.abs (↑f Nat.zero) / ↑Complex.abs (↑Nat.zero ^ z)
simp
f : ArithmeticFunction ℂ
w z : ℂ
h : w.re = z.re
n : ℕ
⊢ ¬succ n = 0
f : ArithmeticFunction ℂ
w z : ℂ
h : w.re = z.re
n : ℕ
⊢ ↑(succ n) ≠ 0
rw [Ne.def, Nat.cast_eq_zero]
no goals
f : ArithmeticFunction ℂ
w z : ℂ
h : w.re = z.re
n : ℕ
⊢ ¬succ n = 0
apply n.succ_ne_zero