English
If f1 = OWith c1 l f1 g1 and f2 = OWith c2 l f2 g2, then f1·f2 = OWith (c1 c2) l (f1 f2) (g1 g2).
Русский
Если две функции удовлетворяют условиям IsBigOWith, их произведение удовлетворяет IsBigOWith с произведением констант.
LaTeX
$$$\text{IsBigOWith}(c_1, l, f_1, g_1) \land \text{IsBigOWith}(c_2, l, f_2, g_2) \Rightarrow \text{IsBigOWith}(c_1 c_2, l, (f_1 f_2), (g_1 g_2)).$$$
Lean4
theorem mul {f₁ f₂ : α → R} {g₁ g₂ : α → S} {c₁ c₂ : ℝ} (h₁ : IsBigOWith c₁ l f₁ g₁) (h₂ : IsBigOWith c₂ l f₂ g₂) :
IsBigOWith (c₁ * c₂) l (fun x => f₁ x * f₂ x) fun x => g₁ x * g₂ x :=
by
simp only [IsBigOWith_def] at *
filter_upwards [h₁, h₂] with _ hx₁ hx₂
apply le_trans (norm_mul_le _ _)
convert mul_le_mul hx₁ hx₂ (norm_nonneg _) (le_trans (norm_nonneg _) hx₁) using 1
rw [norm_mul, mul_mul_mul_comm]
