zpow — Mathlib

English

If f grows polynomially and is nonnegative eventually, then f^p grows polynomially for any integer p.

Русский

Если f растёт полиномиально и неотрицательна в бесконечности, то f^p растёт полиномиально для любого целого p.

LaTeX

$$$\\text{GrowsPolynomially}(f) \\land (\\forall^\\infty x, 0 \\le f(x)) \\Rightarrow \\text{GrowsPolynomially}(x \\mapsto f(x)^{p})\\text{ for }p\\in\\mathbb{Z}$$$

Lean4

protected theorem zpow (p : ℤ) (hf : GrowsPolynomially f) (hf_nonneg : ∀ᶠ x in atTop, 0 ≤ f x) :
    GrowsPolynomially fun x => (f x) ^ p := by
  simp_rw [← rpow_intCast]
  exact hf.rpow p hf_nonneg

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