English
If f^n = O_l(g^n) for some n ≠ 0 and suitable nonnegative bounds c ≤ c'^n and c' ≥ 0, then f = O_l(g) with bound c'.
Русский
Если f^n = O_l(g^n) при некотором n ≠ 0 и существуют такие константы c, c' ≥ 0, что c ≤ c'^n и c' ≥ 0, то f = O_l(g) с константой c'.
LaTeX
$$$(f^n) =O_l(g^n) \\text{ and } n \\neq 0 \\text{ and } c \\le c'^n \\text{ and } c' \\ge 0 \\Rightarrow f =O_l(g) \\text{ with bound } c'.$$$
Lean4
theorem of_pow [NormOneClass S] {n : ℕ} {f : α → S} {g : α → R} (h : IsBigOWith c l (f ^ n) (g ^ n)) (hn : n ≠ 0)
(hc : c ≤ c' ^ n) (hc' : 0 ≤ c') : IsBigOWith c' l f g :=
IsBigOWith.of_bound <|
(h.weaken hc).bound.mono fun x hx ↦
le_of_pow_le_pow_left₀ hn (by positivity) <|
calc
‖f x‖ ^ n = ‖f x ^ n‖ := (norm_pow _ _).symm
_ ≤ c' ^ n * ‖g x ^ n‖ := hx
_ ≤ c' ^ n * ‖g x‖ ^ n := by gcongr; exact norm_pow_le' _ hn.bot_lt
_ = (c' * ‖g x‖) ^ n := (mul_pow _ _ _).symm
