tendsto_nat_mul_log_one_add_of_tendsto

English

If g: ℝ→ℂ satisfies the hypotheses, then (1+g(x))^{x} tends to exp(t) as x→∞.

Русский

Если g удовлетворяет условиям, то (1+g(x))^{x} стремится к exp(t) при x→∞.

LaTeX

$$$\\displaystyle \\lim_{x\\to\\infty} (1 + g(x))^{x} = e^{t}$$$

Lean4

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

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