smul_isBigO — Mathlib

English

If k1 = o_l k2 and f' = O_l g', then k1 x • f' x = o_l k2 x • g' x.

Русский

Если k1 = o_l k2 и f' = O_l g', то k1 x • f' x = o_l k2 x • g' x.

LaTeX

$$$ IsLittleO l k1 k2 \land IsBigOWith c l f' g' \Rightarrow (fun x => k1 x • f' x) =o[l] (fun x => k2 x • g' x). $$$

Lean4

theorem smul_isBigO (h₁ : k₁ =o[l] k₂) (h₂ : f' =O[l] g') : (fun x => k₁ x • f' x) =o[l] fun x => k₂ 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)).smul hc').congr_const (div_mul_cancel₀ _ (ne_of_gt c'pos))

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