mul_isBigO — Mathlib

English

If f1 = O l g1 and f2 = O l g2, then (f1 f2) = O l (g1 g2).

Русский

Если f1 = O_l(g1) и f2 = O_l(g2), то f1 f2 = O_l(g1 g2).

LaTeX

$$$\text{IsBigO}(l, f_1, g_1) \land \text{IsBigO}(l, f_2, g_2) \Rightarrow \text{IsBigO}(l, (f_1 f_2), (g_1 g_2)).$$$

Lean4

theorem mul_isBigO {f₁ f₂ : α → R} {g₁ g₂ : α → S} (h₁ : f₁ =o[l] g₁) (h₂ : f₂ =O[l] g₂) :
    (fun x ↦ f₁ x * f₂ x) =o[l] fun x ↦ g₁ x * g₂ x :=
  by
  simp only [IsLittleO_def] at *
  intro c cpos
  rcases h₂.exists_pos with ⟨c', c'pos, hc'⟩
  exact ((h₁ (div_pos cpos c'pos)).mul hc').congr_const (div_mul_cancel₀ _ (ne_of_gt c'pos))

Похожие утверждения