English
For a finite index set ι and a family of normed groups (E_i), the bound for a function f: α → ∀ i, E_i is equivalent to bounds on each coordinate f_i: α → E_i with the same constant.
Русский
Для конечного множества индексов ι и семейства нормированных групп (E_i) ограничение для f: α → ∀ i, E_i эквивалентно ограничению на каждую компоненту f_i: α → E_i с тем же константным множителем.
LaTeX
$$$\\displaystyle f = O_l g \\;\\text{in } (\\prod_i E_i) \\iff \\forall i, (\\lambda x. f(x))(i) = O_l g.$$$
Lean4
theorem isBigO_cofinite_iff (h : ∀ x, g'' x = 0 → f'' x = 0) : f'' =O[cofinite] g'' ↔ ∃ C, ∀ x, ‖f'' x‖ ≤ C * ‖g'' x‖ :=
by
classical
exact
⟨fun h' =>
let ⟨C, _C₀, hC⟩ := bound_of_isBigO_cofinite h'
⟨C, fun x => if hx : g'' x = 0 then by simp [h _ hx, hx] else hC hx⟩,
fun h => (isBigO_top.2 h).mono le_top⟩
