isBigO_pi — Mathlib

English

If f1 = o_l f2, then f2 = O_l (f2 + f1).

Русский

Если f1 = o_l f2, то f2 = O_l (f2 + f1).

LaTeX

$$$\\displaystyle \\text{If } f_1 = o_l f_2, \\; f_2 = O_l (f_2 + f_1).$$$

Lean4

@[simp]
theorem isBigO_pi {ι : Type*} [Fintype ι] {E' : ι → Type*} [∀ i, NormedAddCommGroup (E' i)] {f : α → ∀ i, E' i} :
    f =O[l] g' ↔ ∀ i, (fun x => f x i) =O[l] g' :=
  by
  simp only [isBigO_iff_eventually_isBigOWith, ← eventually_all]
  exact eventually_congr (eventually_atTop.2 ⟨0, fun c => isBigOWith_pi⟩)

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