abs_isBoundedUnder_iff — Mathlib

English

For a polynomial P ∈ 𝕜[X], the function x ↦ |P(x)| is bounded above along the atTop direction if and only if deg P ≤ 0.

Русский

Для многочлена P ∈ 𝕜[X] функция x ↦ |P(x)| ограничена сверху при x → ∞ тогда и только тогда, когда deg P ≤ 0.

LaTeX

$$$$\text{IsBoundedUnder}_{\le}(atTop)\bigl(x \mapsto |P(x)|\bigr) \iff \deg P \le 0.$$$$

Lean4

theorem abs_isBoundedUnder_iff : (IsBoundedUnder (· ≤ ·) atTop fun x => |eval x P|) ↔ P.degree ≤ 0 :=
  by
  refine
    ⟨fun h => ?_, fun h =>
      ⟨|P.coeff 0|,
        eventually_map.mpr
          (Eventually.of_forall
            (forall_imp (fun _ => le_of_eq) fun x =>
              congr_arg abs <| _root_.trans (congr_arg (eval x) (eq_C_of_degree_le_zero h)) eval_C))⟩⟩
  contrapose! h
  exact not_isBoundedUnder_of_tendsto_atTop (abs_tendsto_atTop P h)

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