isBigO_one_nat_atTop_iff — Mathlib

English

If f = O_l g with a nonnegative bound C, then for each coordinate i of a finite product, the same bound holds coordinatewise.

Русский

Если f = O_l g с неотрицательной константой C, тогда по координатам для каждого i в произведении та же граница выполняется.

LaTeX

$$$\\displaystyle \\text{If } f = O_l g \\text{ with } C\\ge 0, \\text{ then } \\forall i, f_i = O_l g.$$$

Lean4

theorem isBigO_one_nat_atTop_iff {f : ℕ → E''} : f =O[atTop] (fun _n => 1 : ℕ → ℝ) ↔ ∃ C, ∀ n, ‖f n‖ ≤ C :=
  Iff.trans (isBigO_nat_atTop_iff fun _ h => (one_ne_zero h).elim) <| by simp only [norm_one, mul_one]

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