tendsto_atTop_of_leadingCoeff_nonneg

English

If deg(P) > 0 and leadingCoeff(P) ≥ 0, then eval x P → ∞ as x → ∞.

Русский

Если deg(P) > 0 и ведущий коэффициент P ≥ 0, тогда P(x) → ∞ при x → ∞.

LaTeX

$$$$\operatorname{Tendsto}(\lambda x. P(x))\;\text{atTop}\;\text{atTop} \quad\text{under } \deg(P)>0,\; \text{lc}(P)\ge 0.$$$$

Lean4

theorem tendsto_atTop_of_leadingCoeff_nonneg (hdeg : 0 < P.degree) (hnng : 0 ≤ P.leadingCoeff) :
    Tendsto (fun x => eval x P) atTop atTop :=
  P.isEquivalent_atTop_lead.symm.tendsto_atTop <|
    tendsto_const_mul_pow_atTop (natDegree_pos_iff_degree_pos.2 hdeg).ne' <|
      hnng.lt_of_ne' <| leadingCoeff_ne_zero.mpr <| ne_zero_of_degree_gt hdeg

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