Theorem: Complex.cpow_tendsto (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
s : ℂ
s_re_gt : 1 < s.re
⊢ Tendsto (fun x => ↑x ^ (1 - s)) atTop (𝓝 0)
Tactic:
have one_sub_s_re_ne : (1 - s).re ≠ 0 := by simp only [sub_re, one_re]; linarith
State after:
s : ℂ
s_re_gt : 1 < s.re
one_sub_s_re_ne : (1 - s).re ≠ 0
⊢ Tendsto (fun x => ↑x ^ (1 - s)) atTop (𝓝 0)

State before:
s : ℂ
s_re_gt : 1 < s.re
one_sub_s_re_ne : (1 - s).re ≠ 0
⊢ Tendsto (fun x => ↑x ^ (1 - s)) atTop (𝓝 0)
Tactic:
rw [tendsto_zero_iff_norm_tendsto_zero]
State after:
s : ℂ
s_re_gt : 1 < s.re
one_sub_s_re_ne : (1 - s).re ≠ 0
⊢ Tendsto (fun x => ‖↑x ^ (1 - s)‖) atTop (𝓝 0)

State before:
s : ℂ
s_re_gt : 1 < s.re
one_sub_s_re_ne : (1 - s).re ≠ 0
⊢ Tendsto (fun x => ‖↑x ^ (1 - s)‖) atTop (𝓝 0)
Tactic:
simp_rw [Complex.norm_natCast_cpow_of_re_ne_zero _ (one_sub_s_re_ne)]
State after:
s : ℂ
s_re_gt : 1 < s.re
one_sub_s_re_ne : (1 - s).re ≠ 0
⊢ Tendsto (fun x => ↑x ^ (1 - s).re) atTop (𝓝 0)

State before:
s : ℂ
s_re_gt : 1 < s.re
one_sub_s_re_ne : (1 - s).re ≠ 0
⊢ Tendsto (fun x => ↑x ^ (1 - s).re) atTop (𝓝 0)
Tactic:
rw [(by simp only [sub_re, one_re, neg_sub] : (1 - s).re = - (s - 1).re)]
State after:
s : ℂ
s_re_gt : 1 < s.re
one_sub_s_re_ne : (1 - s).re ≠ 0
⊢ Tendsto (fun x => ↑x ^ (-(s - 1).re)) atTop (𝓝 0)

State before:
s : ℂ
s_re_gt : 1 < s.re
one_sub_s_re_ne : (1 - s).re ≠ 0
⊢ Tendsto (fun x => ↑x ^ (-(s - 1).re)) atTop (𝓝 0)
Tactic:
apply (tendsto_rpow_neg_atTop _).comp tendsto_natCast_atTop_atTop
State after:
s : ℂ
s_re_gt : 1 < s.re
one_sub_s_re_ne : (1 - s).re ≠ 0
⊢ 0 < (s - 1).re

State before:
s : ℂ
s_re_gt : 1 < s.re
one_sub_s_re_ne : (1 - s).re ≠ 0
⊢ 0 < (s - 1).re
Tactic:
simp [s_re_gt]
State after:
no goals

State before:
s : ℂ
s_re_gt : 1 < s.re
⊢ (1 - s).re ≠ 0
Tactic:
simp only [sub_re, one_re]
State after:
s : ℂ
s_re_gt : 1 < s.re
⊢ 1 - s.re ≠ 0

State before:
s : ℂ
s_re_gt : 1 < s.re
⊢ 1 - s.re ≠ 0
Tactic:
linarith
State after:
no goals

State before:
s : ℂ
s_re_gt : 1 < s.re
one_sub_s_re_ne : (1 - s).re ≠ 0
⊢ (1 - s).re = -(s - 1).re
Tactic:
simp only [sub_re, one_re, neg_sub]
State after:
no goals