English
If g: ℝ→ℂ satisfies lim x→∞ x g(x) = t, then lim x→∞ x log(1+g(x)) = t.
Русский
Если g: ℝ→ℂ такова, что предел x g(x) при x→∞ равен t, тогда предел x log(1+g(x)) равен t.
LaTeX
$$$\\displaystyle \\text{If } x g(x) \\to t \\text{ as } x\\to\\infty, \\quad x\\log(1+g(x)) \\to 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_cpow_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
apply ((continuous_exp.tendsto _).comp (tendsto_mul_log_one_add_of_tendsto hg)).congr'
have hg0 :=
tendsto_zero_of_isBoundedUnder_smul_of_tendsto_cobounded hg.norm.isBoundedUnder_le
(RCLike.tendsto_ofReal_atTop_cobounded ℂ)
filter_upwards [hg0.eventually_ne (show 0 ≠ -1 by simp)] with x hg1
dsimp
rw [cpow_def_of_ne_zero, mul_comm]
intro hg0
rw [← add_eq_zero_iff_neg_eq.mp hg0] at hg1
norm_num at hg1
