tendsto_atTop_iff_leadingCoeff_nonneg

English

A polynomial P satisfies Tendsto atTop of eval to atTop iff deg(P) > 0 and leadingCoeff(P) ≥ 0.

Русский

Сходимость eval x P к бесконечности при x→∞ эквивалентна deg(P) > 0 и lc(P) ≥ 0.

LaTeX

$$$$\text{Tendsto}_{x\to\infty} \; P(x) = \infty \quad\Longleftrightarrow\quad \deg(P)>0 \text{ и } \operatorname{lc}(P) \ge 0.$$$$

Lean4

theorem tendsto_atTop_iff_leadingCoeff_nonneg :
    Tendsto (fun x => eval x P) atTop atTop ↔ 0 < P.degree ∧ 0 ≤ P.leadingCoeff :=
  by
  refine ⟨fun h => ?_, fun h => tendsto_atTop_of_leadingCoeff_nonneg P h.1 h.2⟩
  have : Tendsto (fun x => P.leadingCoeff * x ^ P.natDegree) atTop atTop := (isEquivalent_atTop_lead P).tendsto_atTop h
  rw [tendsto_const_mul_pow_atTop_iff, ← pos_iff_ne_zero, natDegree_pos_iff_degree_pos] at this
  exact ⟨this.1, this.2.le⟩

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