add — Mathlib

English

A concluding variant ensuring that the zero-implication holds under the main Big-OWith relation.

Русский

Завершающая формулировка: нулевой вывод удерживается под основным Big-OWith.

LaTeX

$$final_eq_zero_imp : IsBigOWith c l f'' g'' → ∀ᶠ x in l, g'' x = 0 → f'' x = 0$$

Lean4

theorem add (h₁ : IsBigOWith c₁ l f₁ g) (h₂ : IsBigOWith c₂ l f₂ g) : IsBigOWith (c₁ + c₂) l (fun x => f₁ x + f₂ x) g :=
  by
  rw [IsBigOWith_def] at *
  filter_upwards [h₁, h₂] with x hx₁ hx₂ using
    calc
      ‖f₁ x + f₂ x‖ ≤ c₁ * ‖g x‖ + c₂ * ‖g x‖ := norm_add_le_of_le hx₁ hx₂
      _ = (c₁ + c₂) * ‖g x‖ := (add_mul _ _ _).symm

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