[GOAL]
z : ℂ
⊢ LSeriesSummable 0 z
[PROOFSTEP]
simp [LSeriesSummable, summable_zero]
[GOAL]
f : ArithmeticFunction ℂ
m : ℝ
h : ∀ (n : ℕ), ↑Complex.abs (↑f n) ≤ m
z : ℝ
hz : 1 < z
⊢ LSeriesSummable f ↑z
[PROOFSTEP]
by_cases h0 : m = 0
[GOAL]
case pos
f : ArithmeticFunction ℂ
m : ℝ
h : ∀ (n : ℕ), ↑Complex.abs (↑f n) ≤ m
z : ℝ
hz : 1 < z
h0 : m = 0
⊢ LSeriesSummable f ↑z
[PROOFSTEP]
subst h0
[GOAL]
case pos
f : ArithmeticFunction ℂ
z : ℝ
hz : 1 < z
h : ∀ (n : ℕ), ↑Complex.abs (↑f n) ≤ 0
⊢ LSeriesSummable f ↑z
[PROOFSTEP]
have hf : f = 0 := ArithmeticFunction.ext fun n => Complex.abs.eq_zero.1 (le_antisymm (h n) (Complex.abs.nonneg _))
[GOAL]
case pos
f : ArithmeticFunction ℂ
z : ℝ
hz : 1 < z
h : ∀ (n : ℕ), ↑Complex.abs (↑f n) ≤ 0
hf : f = 0
⊢ LSeriesSummable f ↑z
[PROOFSTEP]
simp [hf]
[GOAL]
case neg
f : ArithmeticFunction ℂ
m : ℝ
h : ∀ (n : ℕ), ↑Complex.abs (↑f n) ≤ m
z : ℝ
hz : 1 < z
h0 : ¬m = 0
⊢ LSeriesSummable f ↑z
[PROOFSTEP]
refine' summable_of_norm_bounded (fun n : ℕ => m / n ^ z) _ _
[GOAL]
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
[PROOFSTEP]
simp_rw [div_eq_mul_inv]
[GOAL]
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)⁻¹
[PROOFSTEP]
exact (summable_mul_left_iff h0).2 (Real.summable_nat_rpow_inv.2 hz)
[GOAL]
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
[PROOFSTEP]
intro n
[GOAL]
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
[PROOFSTEP]
have hm : 0 ≤ m := le_trans (Complex.abs.nonneg _) (h 0)
[GOAL]
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
[PROOFSTEP]
cases' n with n
[GOAL]
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
[PROOFSTEP]
simp [hm, Real.zero_rpow (_root_.ne_of_gt (lt_trans Real.zero_lt_one hz))]
[GOAL]
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)
[PROOFSTEP]
simp only [map_div₀, Complex.norm_eq_abs]
[GOAL]
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
[PROOFSTEP]
apply div_le_div hm (h _) (Real.rpow_pos_of_pos (Nat.cast_pos.2 n.succ_pos) _) (le_of_eq _)
[GOAL]
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)
[PROOFSTEP]
rw [Complex.abs_cpow_real, Complex.abs_cast_nat]
[GOAL]
f : ArithmeticFunction ℂ
w z : ℂ
h : w.re = z.re
⊢ LSeriesSummable f w ↔ LSeriesSummable f z
[PROOFSTEP]
suffices h : ∀ n : ℕ, Complex.abs (f n) / Complex.abs (↑n ^ w) = Complex.abs (f n) / Complex.abs (↑n ^ z)
[GOAL]
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
[PROOFSTEP]
simp [LSeriesSummable, ← summable_norm_iff, h, Complex.norm_eq_abs]
[GOAL]
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)
[PROOFSTEP]
intro n
[GOAL]
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)
[PROOFSTEP]
cases' n with n
[GOAL]
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)
[PROOFSTEP]
simp
[GOAL]
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)
[PROOFSTEP]
apply congr rfl
[GOAL]
case h.succ
f : ArithmeticFunction ℂ
w z : ℂ
h : w.re = z.re
n : ℕ
⊢ ↑Complex.abs (↑(succ n) ^ w) = ↑Complex.abs (↑(succ n) ^ z)
[PROOFSTEP]
have h0 : (n.succ : ℂ) ≠ 0 := by
  rw [Ne.def, Nat.cast_eq_zero]
  apply n.succ_ne_zero
[GOAL]
f : ArithmeticFunction ℂ
w z : ℂ
h : w.re = z.re
n : ℕ
⊢ ↑(succ n) ≠ 0
[PROOFSTEP]
rw [Ne.def, Nat.cast_eq_zero]
[GOAL]
f : ArithmeticFunction ℂ
w z : ℂ
h : w.re = z.re
n : ℕ
⊢ ¬succ n = 0
[PROOFSTEP]
apply n.succ_ne_zero
[GOAL]
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)
[PROOFSTEP]
rw [Complex.cpow_def, Complex.cpow_def, if_neg h0, if_neg h0, Complex.abs_exp_eq_iff_re_eq]
[GOAL]
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
[PROOFSTEP]
simp only [h, Complex.mul_re, mul_eq_mul_left_iff, sub_right_inj]
[GOAL]
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
[PROOFSTEP]
right
[GOAL]
case h.succ.h
f : ArithmeticFunction ℂ
w z : ℂ
h : w.re = z.re
n : ℕ
h0 : ↑(succ n) ≠ 0
⊢ (Complex.log ↑(succ n)).im = 0
[PROOFSTEP]
rw [Complex.log_im, ← Complex.ofReal_nat_cast]
[GOAL]
case h.succ.h
f : ArithmeticFunction ℂ
w z : ℂ
h : w.re = z.re
n : ℕ
h0 : ↑(succ n) ≠ 0
⊢ Complex.arg ↑↑(succ n) = 0
[PROOFSTEP]
exact Complex.arg_ofReal_of_nonneg (le_of_lt (cast_pos.2 n.succ_pos))
[GOAL]
f : ArithmeticFunction ℂ
m : ℝ
h : ∀ (n : ℕ), ↑Complex.abs (↑f n) ≤ m
z : ℂ
hz : 1 < z.re
⊢ LSeriesSummable f z
[PROOFSTEP]
rw [← LSeriesSummable_iff_of_re_eq_re (Complex.ofReal_re z.re)]
[GOAL]
f : ArithmeticFunction ℂ
m : ℝ
h : ∀ (n : ℕ), ↑Complex.abs (↑f n) ≤ m
z : ℂ
hz : 1 < z.re
⊢ LSeriesSummable f ↑z.re
[PROOFSTEP]
apply LSeriesSummable_of_bounded_of_one_lt_real h
[GOAL]
f : ArithmeticFunction ℂ
m : ℝ
h : ∀ (n : ℕ), ↑Complex.abs (↑f n) ≤ m
z : ℂ
hz : 1 < z.re
⊢ 1 < z.re
[PROOFSTEP]
exact hz
[GOAL]
z : ℂ
⊢ LSeriesSummable (↑ζ) z ↔ 1 < z.re
[PROOFSTEP]
rw [← LSeriesSummable_iff_of_re_eq_re (Complex.ofReal_re z.re), LSeriesSummable, ← summable_norm_iff, ←
  Real.summable_one_div_nat_rpow, iff_iff_eq]
[GOAL]
z : ℂ
⊢ (Summable fun x => ‖↑↑ζ x / ↑x ^ ↑z.re‖) = Summable fun n => 1 / ↑n ^ z.re
[PROOFSTEP]
by_cases h0 : z.re = 0
[GOAL]
case pos
z : ℂ
h0 : z.re = 0
⊢ (Summable fun x => ‖↑↑ζ x / ↑x ^ ↑z.re‖) = Summable fun n => 1 / ↑n ^ z.re
[PROOFSTEP]
rw [h0, ← summable_nat_add_iff 1]
[GOAL]
case pos
z : ℂ
h0 : z.re = 0
⊢ (Summable fun n => ‖↑↑ζ (n + 1) / ↑(n + 1) ^ ↑0‖) = Summable fun n => 1 / ↑n ^ 0
[PROOFSTEP]
apply congr rfl
[GOAL]
case pos
z : ℂ
h0 : z.re = 0
⊢ (fun n => ‖↑↑ζ (n + 1) / ↑(n + 1) ^ ↑0‖) = fun n => 1 / ↑n ^ 0
[PROOFSTEP]
ext n
[GOAL]
case pos.h
z : ℂ
h0 : z.re = 0
n : ℕ
⊢ ‖↑↑ζ (n + 1) / ↑(n + 1) ^ ↑0‖ = 1 / ↑n ^ 0
[PROOFSTEP]
simp [n.succ_ne_zero]
[GOAL]
case neg
z : ℂ
h0 : ¬z.re = 0
⊢ (Summable fun x => ‖↑↑ζ x / ↑x ^ ↑z.re‖) = Summable fun n => 1 / ↑n ^ z.re
[PROOFSTEP]
apply congr rfl
[GOAL]
case neg
z : ℂ
h0 : ¬z.re = 0
⊢ (fun x => ‖↑↑ζ x / ↑x ^ ↑z.re‖) = fun n => 1 / ↑n ^ z.re
[PROOFSTEP]
ext ⟨- | n⟩
[GOAL]
case neg.h.zero
z : ℂ
h0 : ¬z.re = 0
⊢ ‖↑↑ζ Nat.zero / ↑Nat.zero ^ ↑z.re‖ = 1 / ↑Nat.zero ^ z.re
[PROOFSTEP]
simp [h0]
[GOAL]
case neg.h.succ
z : ℂ
h0 : ¬z.re = 0
n✝ : ℕ
⊢ ‖↑↑ζ (succ n✝) / ↑(succ n✝) ^ ↑z.re‖ = 1 / ↑(succ n✝) ^ z.re
[PROOFSTEP]
simp only [cast_zero, natCoe_apply, zeta_apply, succ_ne_zero, if_false, cast_succ, one_div, Complex.norm_eq_abs,
  map_inv₀, Complex.abs_cpow_real, inv_inj, zero_add]
[GOAL]
case neg.h.succ
z : ℂ
h0 : ¬z.re = 0
n✝ : ℕ
⊢ ↑Complex.abs (↑n✝ + 1) ^ z.re = (↑n✝ + 1) ^ z.re
[PROOFSTEP]
rw [← cast_one, ← cast_add, Complex.abs_of_nat, cast_add, cast_one]
[GOAL]
f g : ArithmeticFunction ℂ
z : ℂ
hf : LSeriesSummable f z
hg : LSeriesSummable g z
⊢ LSeries (f + g) z = LSeries f z + LSeries g z
[PROOFSTEP]
simp only [LSeries, add_apply]
[GOAL]
f g : ArithmeticFunction ℂ
z : ℂ
hf : LSeriesSummable f z
hg : LSeriesSummable g z
⊢ ∑' (n : ℕ), (↑f n + ↑g n) / ↑n ^ z = ∑' (n : ℕ), ↑f n / ↑n ^ z + ∑' (n : ℕ), ↑g n / ↑n ^ z
[PROOFSTEP]
rw [← tsum_add hf hg]
[GOAL]
f g : ArithmeticFunction ℂ
z : ℂ
hf : LSeriesSummable f z
hg : LSeriesSummable g z
⊢ ∑' (n : ℕ), (↑f n + ↑g n) / ↑n ^ z = ∑' (b : ℕ), (↑f b / ↑b ^ z + ↑g b / ↑b ^ z)
[PROOFSTEP]
apply congr rfl (funext fun n => _)
[GOAL]
f g : ArithmeticFunction ℂ
z : ℂ
hf : LSeriesSummable f z
hg : LSeriesSummable g z
⊢ ∀ (n : ℕ), (↑f n + ↑g n) / ↑n ^ z = ↑f n / ↑n ^ z + ↑g n / ↑n ^ z
[PROOFSTEP]
simp [_root_.add_div]
