rpow — Mathlib

English

If f = O_l g with c ≥ 0 and g ≥ 0 eventually, and r ≥ 0, then f^r = O_l g^r.

Русский

Если f = O_l g с неотрицательной константой c и g ≥ 0 почти наверняка, и r ≥ 0, тогда f^r = O_l g^r.

LaTeX

$$$$ f^r = O_l (g^r) \quad (r \ge 0). $$$$

Lean4

theorem rpow (h : IsBigOWith c l f g) (hc : 0 ≤ c) (hr : 0 ≤ r) (hg : 0 ≤ᶠ[l] g) :
    IsBigOWith (c ^ r) l (fun x => f x ^ r) fun x => g x ^ r :=
  by
  apply IsBigOWith.of_bound
  filter_upwards [hg, h.bound] with x hgx hx
  calc
    |f x ^ r| ≤ |f x| ^ r := abs_rpow_le_abs_rpow _ _
    _ ≤ (c * |g x|) ^ r := (rpow_le_rpow (abs_nonneg _) hx hr)
    _ = c ^ r * |g x ^ r| := by rw [mul_rpow hc (abs_nonneg _), abs_rpow_of_nonneg hgx]

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