English
For real t, the limit of (1+ t/x)^x as x→∞ equals exp(t).
Русский
Для вещественного t предел (1+ t/x)^x при x→∞ равен exp(t).
LaTeX
$$$\\displaystyle \\lim_{x\\to\\infty} (1 + \\frac{t}{x})^{x} = e^{t}$$$
Lean4
/-- The limit of `(1 + g x) ^ x` as `(x : ℝ) → ∞` is `exp t`,
where `t : ℝ` is the limit of `x * g x`. -/
theorem tendsto_one_add_rpow_exp_of_tendsto {g : ℝ → ℝ} {t : ℝ} (hg : Tendsto (fun x ↦ x * g x) atTop (𝓝 t)) :
Tendsto (fun x ↦ (1 + g x) ^ x) atTop (𝓝 (exp t)) :=
by
have hg0 :=
tendsto_zero_of_isBoundedUnder_smul_of_tendsto_cobounded hg.norm.isBoundedUnder_le (tendsto_id'.mpr (by simp))
rw [← tendsto_ofReal_iff] at hg ⊢
push_cast at hg ⊢
apply (Complex.tendsto_one_add_cpow_exp_of_tendsto hg).congr'
filter_upwards [hg0.eventually_const_le (show (-1 : ℝ) < 0 by simp)] with x hg1
rw [Complex.ofReal_cpow (by linarith), Complex.ofReal_add, Complex.ofReal_one]
