add — Mathlib

English

Let f1, f2 be functions that are each O_l(g). Then their sum f1 + f2 is also O_l(g). In other words, the Big-O bound is closed under addition.

Русский

Пусть f1 и f2 — функции, каждая из которых удовлетворяет условию f = O_l(g). Тогда сумма f1 + f2 тоже удовлетворяет f = O_l(g). Иными словами, пределоуказательность Большого-O сохранится при сложении.

LaTeX

$$$ (f_1 + f_2) = O_l(g) $$$

Lean4

theorem add (h₁ : f₁ =O[l] g) (h₂ : f₂ =O[l] g) : (fun x => f₁ x + f₂ x) =O[l] g :=
  let ⟨_c₁, hc₁⟩ := h₁.isBigOWith
  let ⟨_c₂, hc₂⟩ := h₂.isBigOWith
  (hc₁.add hc₂).isBigO

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