English
If IsBigOWith c l f g holds, then for all natural n, f^n = OWith c' l g^n with an explicit growth c'' depending on n.
Русский
Если IsBigOWith c l f g выполняется, то для всех натуральных n выполняется f^n = OWith c' l g^n с явным ростом зависящим от n.
LaTeX
$$$\text{IsBigOWith}(c, l, f, g) \Rightarrow \forall n\in\mathbb{N}, \text{IsBigOWith}(c_n, l, f^n, g^n).$$$
Lean4
theorem pow' [NormOneClass S] {f : α → R} {g : α → S} (h : IsBigOWith c l f g) :
∀ n : ℕ, IsBigOWith (Nat.casesOn n ‖(1 : R)‖ fun n ↦ c ^ (n + 1)) l (fun x => f x ^ n) fun x => g x ^ n
| 0 => by
have : Nontrivial S := NormOneClass.nontrivial
simpa using isBigOWith_const_const (1 : R) (one_ne_zero' S) l
| 1 => by simpa
| n + 2 => by simpa [pow_succ] using (IsBigOWith.pow' h (n + 1)).mul h
