English
For any function f, Tendsto f to 1 is equivalent to Tendsto (mabs ∘ f) to 1.
Русский
Для любой функции f, стремление к 1 эквивалентно стремлению к 1 модуля значения.
LaTeX
$$$\mathrm{Tendsto}\ f\ l\to (\mathcal{nhds}\ 1) \iff \mathrm{Tendsto}\ (\mathrm{mabs}\circ f)\ l\to (\mathcal{nhds}\ 1).$$$
Lean4
theorem le_liminf_mul [f.NeBot] (h₁ : 0 ≤ᶠ[f] u) (h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u) (h₃ : 0 ≤ᶠ[f] v)
(h₄ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) f v) : (liminf u f) * liminf v f ≤ liminf (u * v) f :=
by
have h := isCoboundedUnder_ge_mul_of_nonneg h₁ h₂ h₃ h₄
have h' := isBoundedUnder_of_eventually_ge (a := 0) <| (h₁.and h₃).mono fun x ⟨u0, v0⟩ ↦ mul_nonneg u0 v0
apply
mul_le_of_forall_lt_of_nonneg (le_liminf_of_le h₂.isCoboundedUnder_ge h₁)
(le_liminf_of_le h ((h₁.and h₃).mono fun x ⟨u0, v0⟩ ↦ mul_nonneg u0 v0))
intro a a0 au b b0 bv
refine (le_liminf_iff h h').2 fun c c_ab ↦ ?_
filter_upwards [eventually_lt_of_lt_liminf au (isBoundedUnder_of_eventually_ge h₁),
eventually_lt_of_lt_liminf bv (isBoundedUnder_of_eventually_ge h₃)] with x xa xb
exact c_ab.trans_le (mul_le_mul xa.le xb.le b0 (a0.trans xa.le))
