mul_isLittleO — 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{IsLittleO}(l, f_2, g_2) \Rightarrow \text{IsLittleO}(l, (f_1 f_2), (g_1 g_2)).$$$

Lean4

theorem mul_isLittleO {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 (hc'.mul (h₂ (div_pos cpos c'pos))).congr_const (mul_div_cancel₀ _ (ne_of_gt c'pos))

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