tendsto_one_add_pow_exp_of_tendsto

English

For a sequence g: ℕ→ℂ with tendsto behavior, (1+g n)^n → exp t as n→∞ where t is the limit of n g(n).

Русский

Для последовательности g: ℕ→ℂ, где n g(n) сходится к t, (1+g(n))^n стремится к exp(t) при n→∞.

LaTeX

$$$\\displaystyle (1+g(n))^{n} \\to e^{t} \\quad (n\\to\\infty),\\; t=\\lim_{n\\to\\infty} n g(n)$$$

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_cpow_exp_of_tendsto (tendsto_smul_comp_nat_floor_of_tendsto_mul hg) |>.comp
      tendsto_natCast_atTop_atTop |>.congr
    (by simp)

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