tendsto_one_add_div_pow_exp — Mathlib

English

Similar statements hold for sequences indexed by natural numbers with the same exponential limit.

Русский

Аналогично, для последовательностей с тем же пределом экспоненты.

LaTeX

$$$\\text{For a sequence } g: \\mathbb{N}\\to \\mathbb{C}, \\; \\lim_{n\\to\\infty} (1+g(n))^{n} = e^{t} \\text{ if } \\lim_{n\\to\\infty} n g(n)=t$$$

Lean4

/-- The limit of `(1 + t/n) ^ n` as `n → ∞` is `exp t` for `t : ℂ`. -/
theorem tendsto_one_add_div_pow_exp (t : ℂ) : Tendsto (fun n : ℕ ↦ (1 + t / n) ^ n) atTop (𝓝 (exp t)) :=
  tendsto_one_add_div_cpow_exp t |>.comp tendsto_natCast_atTop_atTop |>.congr (by simp)

Похожие утверждения