abs — Mathlib

English

If f grows polynomially, then its absolute value |f| grows polynomially.

Русский

Если f растёт полиномиально, то и |f| растёт полиномиально.

LaTeX

$$$\\text{GrowsPolynomially}(f) \\Rightarrow \\text{GrowsPolynomially}(x\\mapsto |f(x)|)$$$

Lean4

protected theorem abs (hf : GrowsPolynomially f) : GrowsPolynomially (fun x => |f x|) := by
  cases eventually_atTop_nonneg_or_nonpos hf with
  | inl
    hf' =>
    have hmain : f =ᶠ[atTop] fun x => |f x| :=
      by
      filter_upwards [hf'] with x hx
      rw [abs_of_nonneg hx]
    rw [← iff_eventuallyEq hmain]
    exact hf
  | inr
    hf' =>
    have hmain : -f =ᶠ[atTop] fun x => |f x| :=
      by
      filter_upwards [hf'] with x hx
      simp only [Pi.neg_apply, abs_of_nonpos hx]
    rw [← iff_eventuallyEq hmain]
    exact hf.neg

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