smul — Mathlib

English

For any c, IsBigOWith (‖c‖) l f' g' holds if IsBigOWith c l f' g'.

Русский

Для любого c: IsBigOWith (‖c‖) l f' g' следует из IsBigOWith c l f' g'.

LaTeX

$$$ IsBigOWith (\|c\|) l f' g' \leftarrow IsBigOWith c l f' g'. $$$

Lean4

theorem smul (h₁ : IsBigOWith c l k₁ k₂) (h₂ : IsBigOWith c' l f' g') :
    IsBigOWith (c * c') l (fun x => k₁ x • f' x) fun x => k₂ x • g' x :=
  by
  simp only [IsBigOWith_def] at *
  filter_upwards [h₁, h₂] with _ hx₁ hx₂
  apply le_trans (norm_smul_le _ _)
  convert mul_le_mul hx₁ hx₂ (norm_nonneg _) (le_trans (norm_nonneg _) hx₁) using 1
  rw [norm_smul, mul_mul_mul_comm]

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