English
If the product f1(x) • g(x) tends to t, and f1 tends to cobounded in K, and f1 − f2 remains bounded, then f2(x) • g(x) also tends to t.
Русский
Если произведение f1(x) • g(x) сходится к t и f1 стремится к границе в K, а разность f1−f2 ограничена, то и f2(x) • g(x) сходится к t.
LaTeX
$$\forall x, \; (f1(x) - f2(x)) bounded ∧ f1(x) • g(x) → t ∧ f1(x) → cobounded(K) ⇒ f2(x) • g(x) → t$$
Lean4
theorem tendsto_smul_congr_of_tendsto_left_cobounded_of_isBoundedUnder {f₁ f₂ : α → K} {g : α → R} {t : R}
{l : Filter α} (hmul : Tendsto (fun x ↦ f₁ x • g x) l (𝓝 t)) (hf₁ : Tendsto f₁ l (cobounded K))
(hbdd : IsBoundedUnder (· ≤ ·) l fun x ↦ ‖f₁ x - f₂ x‖) : Tendsto (fun x ↦ f₂ x • g x) l (𝓝 t) :=
by
apply hmul.congr_dist
dsimp
simp_rw [dist_eq_norm, ← sub_smul, norm_smul]
apply isBoundedUnder_le_mul_tendsto_zero
· change IsBoundedUnder _ _ fun _ ↦ _
simpa using hbdd
· rw [← tendsto_zero_iff_norm_tendsto_zero]
exact tendsto_zero_of_isBoundedUnder_smul_of_tendsto_cobounded hmul.norm.isBoundedUnder_le hf₁
