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

State before:
s : ℂ
hs : 0 < s.re
⊢ Tendsto (fun x => (↑x ^ s)⁻¹) atTop (𝓝 0)
Tactic:
rw [tendsto_zero_iff_norm_tendsto_zero]
State after:
s : ℂ
hs : 0 < s.re
⊢ Tendsto (fun x => ‖(↑x ^ s)⁻¹‖) atTop (𝓝 0)

State before:
s : ℂ
hs : 0 < s.re
⊢ Tendsto (fun x => ‖(↑x ^ s)⁻¹‖) atTop (𝓝 0)
Tactic:
simp_rw [norm_inv, Complex.norm_natCast_cpow_of_re_ne_zero _ <| ne_of_gt hs]
State after:
s : ℂ
hs : 0 < s.re
⊢ Tendsto (fun x => (↑x ^ s.re)⁻¹) atTop (𝓝 0)

State before:
s : ℂ
hs : 0 < s.re
⊢ Tendsto (fun x => (↑x ^ s.re)⁻¹) atTop (𝓝 0)
Tactic:
apply Filter.Tendsto.inv_tendsto_atTop
State after:
case h
s : ℂ
hs : 0 < s.re
⊢ Tendsto (fun x => ↑x ^ s.re) atTop atTop

State before:
case h
s : ℂ
hs : 0 < s.re
⊢ Tendsto (fun x => ↑x ^ s.re) atTop atTop
Tactic:
exact (tendsto_rpow_atTop hs).comp tendsto_natCast_atTop_atTop
State after:
no goals