tendsto_nat_mul_log_one_add_of_tendsto

English

If a real-valued sequence g(n) satisfies that n·g(n) tends to t, then n·log(1+g(n)) tends to t as n → ∞.

Русский

Если последовательность g(n) удовлетворяет условию, что n·g(n) → t, то n·log(1+g(n)) → t при n → ∞.

LaTeX

$$$\\displaystyle \\text{If } \\lim_{n\\to\\infty} n\,g(n) = t, \\text{ then } \\lim_{n\\to\\infty} n\\log(1+g(n)) = 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)

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