English
If a function f is Big-O with respect to g along a filter l with bound c, then for every natural exponent n, the n-th power of f is Big-O with respect to the n-th power of g along l, with bound c^n.
Русский
Пусть функция f ограничена по порядку относительно g вдоль фильтра l с коэффициентом c. Тогда для каждого натурального n степень функции f^n ограничена относительно g^n вдоль l с коэффициентом c^n.
LaTeX
$$$\\text{If } f =O_l(g) \\text{ with bound } c, \\text{ then } \\forall n \\in \\mathbb{N},\\ f^n =O_l(g^n)\\text{ with bound } c^n.$$$
Lean4
theorem pow [NormOneClass R] [NormOneClass S] {f : α → R} {g : α → S} (h : IsBigOWith c l f g) :
∀ n : ℕ, IsBigOWith (c ^ n) l (fun x => f x ^ n) fun x => g x ^ n
| 0 => by simpa using h.pow' 0
| n + 1 => h.pow' (n + 1)
