Source indexedlemma · leanprover/lean4:v4.32.0

ZetaPartialSum.tendsto_natCast_cpow_zero_of_neg_re

PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaPartialSum · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZetaPartialSum.lean:167 to 175

Mathematical statement

Exact Lean statement

lemma tendsto_natCast_cpow_zero_of_neg_re (w : ℂ) (hw : w.re < 0) :
    Tendsto (fun N : ℕ => (N : ℂ) ^ w) atTop (𝓝 0)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma tendsto_natCast_cpow_zero_of_neg_re (w : ℂ) (hw : w.re < 0) :    Tendsto (fun N : ℕ => (N : ℂ) ^ w) atTop (𝓝 0) := by  rw [tendsto_zero_iff_norm_tendsto_zero]  have h1 : (fun N : ℕ => (N : ℝ) ^ w.re) =ᶠ[atTop] fun N : ℕ => ‖(N : ℂ) ^ w‖ := by    filter_upwards [eventually_gt_atTop 0] with N hN    rw [Complex.norm_natCast_cpow_of_pos hN w]  rw [tendsto_congr' (EventuallyEq.symm h1)]  rw [show w.re = -(-w.re) from by ring]  exact (tendsto_rpow_neg_atTop (neg_pos.mpr hw)).comp tendsto_natCast_atTop_atTop