tendsto_one_add_div_cpow_exp — Mathlib

English

The limit of (1+g(x))^x as x→∞ is exp(t) whenever x g(x)→t (g real or complex).

Русский

Предел (1+g(x))^x при x→∞ равен exp(t), если x g(x) → t (для вещественных или комплексных g).

LaTeX

$$$\\displaystyle (1+g(x))^x \\xrightarrow[x\\to\\infty]{} e^{t} \\quad\\text{when } x g(x) \\to t$$$

Lean4

/-- The limit of `(1 + t/x) ^ x` as `x → ∞` is `exp t` for `t : ℂ`. -/
theorem tendsto_one_add_div_cpow_exp (t : ℂ) : Tendsto (fun x : ℝ ↦ (1 + t / x) ^ (x : ℂ)) atTop (𝓝 (exp t)) :=
  by
  apply tendsto_one_add_cpow_exp_of_tendsto
  apply tendsto_nhds_of_eventually_eq
  filter_upwards [eventually_ne_atTop 0] with x hx0
  exact mul_div_cancel₀ t (mod_cast hx0)

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