English
If a real-valued function g on natural numbers satisfies Tendsto(n g(n)) to t, then Tendsto(n log(1+g(n))) to t as n→∞.
Русский
Если g:ℕ→ℝ удовлетворяет p. Tendsto(n g(n)) → t, тогда Tendsto(n log(1+g(n))) → t при n→∞.
LaTeX
$$$\\displaystyle \\text{If } \\lim_{n\\to\\infty} n g(n) = t, \\lim_{n\\to\\infty} n \\log(1+g(n)) = t$$$
Lean4
/-- The limit of `x * log (1 + g x)` as `(x : ℝ) → ∞` is `t`,
where `t : ℝ` is the limit of `x * g x`. -/
theorem tendsto_mul_log_one_add_of_tendsto {g : ℝ → ℝ} {t : ℝ} (hg : Tendsto (fun x ↦ x * g x) atTop (𝓝 t)) :
Tendsto (fun x ↦ x * log (1 + g x)) atTop (𝓝 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_mul_log_one_add_of_tendsto hg).congr'
filter_upwards [hg0.eventually_const_le (show (-1 : ℝ) < 0 by simp)] with x hg1
rw [Complex.ofReal_log (by linarith), Complex.ofReal_add, Complex.ofReal_one]
