tendsto_one_add_pow_exp_of_tendsto

English

Let g: N → R. If n·g(n) → t as n → ∞, then (1 + g(n))^n → exp(t).

Русский

Пусть g: ℕ → ℝ. Если n·g(n) → t при n → ∞, то (1 + g(n))^n → exp(t).

LaTeX

$$$$ \left( \lim_{n \to \infty} n\,g(n) = t \right) \Rightarrow \left( \lim_{n \to \infty} (1 + g(n))^n = \exp(t) \right). $$$$

Lean4

/-- The limit of `(1 + g n) ^ n` as `(n : ℝ) → ∞` is `exp t`,
where `t : ℝ` is the limit of `n * g n`. -/
theorem tendsto_one_add_pow_exp_of_tendsto {g : ℕ → ℝ} {t : ℝ} (hg : Tendsto (fun n ↦ n * g n) atTop (𝓝 t)) :
    Tendsto (fun n ↦ (1 + g n) ^ n) atTop (𝓝 (exp t)) :=
  tendsto_one_add_rpow_exp_of_tendsto (tendsto_smul_comp_nat_floor_of_tendsto_mul hg) |>.comp
      tendsto_natCast_atTop_atTop |>.congr
    (by simp)

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