English
If g(x) → 0 and |f(x)| ≤ C eventually, then f(x)g(x) → 0.
Русский
Если g(x) → 0 и существует константа C сEventually |f(x)| ≤ C, то f(x)g(x) → 0.
LaTeX
$$If g \xrightarrow{l} 0 and ∀ᶠ x, |f(x)| ≤ C, then f(x)g(x) \to 0.$$
Lean4
/-- If `g` tends to zero and there exists a constant `C : 𝕜` such that eventually `|f x| ≤ C`,
then the product `f * g` tends to zero. -/
theorem bdd_le_mul_tendsto_zero' {f g : α → 𝕜} (C : 𝕜) (hf : ∀ᶠ x in l, |f x| ≤ C) (hg : Tendsto g l (𝓝 0)) :
Tendsto (fun x ↦ f x * g x) l (𝓝 0) :=
by
rw [tendsto_zero_iff_abs_tendsto_zero]
have hC : Tendsto (fun x ↦ |C * g x|) l (𝓝 0) :=
by
convert (hg.const_mul C).abs
simp_rw [mul_zero, abs_zero]
apply tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds hC
· filter_upwards [hf] with x _ using abs_nonneg _
· filter_upwards [hf] with x hx
simp only [comp_apply, abs_mul]
exact mul_le_mul_of_nonneg_right (hx.trans (le_abs_self C)) (abs_nonneg _)
