English
As x → 0 from the left, log|x| · |x| → 0, hence log x · x → 0 for x < 0.
Русский
При x, стремящемся к 0 слева, log|x| · |x| → 0, следовательно log x · x → 0 при x < 0.
LaTeX
$$$$ \lim_{x \to 0^{-}} \log|x| \cdot |x| = 0. $$$$
Lean4
theorem tendsto_log_mul_self_nhdsLT_zero : Filter.Tendsto (fun x ↦ log x * x) (𝓝[<] 0) (𝓝 0) :=
by
have h := tendsto_log_mul_rpow_nhdsGT_zero zero_lt_one
simp only [Real.rpow_one] at h
have h_eq : ∀ x ∈ Set.Iio 0, (-(fun x ↦ log x * x) ∘ (fun x ↦ |x|)) x = log x * x :=
by
simp only [Set.mem_Iio, Pi.neg_apply, Function.comp_apply, log_abs]
intro x hx
simp only [abs_of_nonpos hx.le, mul_neg, neg_neg]
refine tendsto_nhdsWithin_congr h_eq ?_
nth_rewrite 3 [← neg_zero]
refine (h.comp (tendsto_abs_nhdsNE_zero.mono_left ?_)).neg
refine nhdsWithin_mono 0 (fun x hx ↦ ?_)
simp only [Set.mem_Iio] at hx
simp only [Set.mem_compl_iff, Set.mem_singleton_iff, hx.ne, not_false_eq_true]
