abs_div_tendsto_atTop_of_degree_gt

English

If deg Q < deg P and P.leadingCoeff / Q.leadingCoeff ≤ 0, then P(x)/Q(x) → −∞ as x → ∞.

Русский

Если deg Q < deg P и отношение ведущих коэффициентов не положительно, то P(x)/Q(x) → −∞ при x → ∞.

LaTeX

$$$$\deg Q < \deg P,\; Q \neq 0,\; \frac{\text{leadingCoeff}(P)}{\text{leadingCoeff}(Q)} \le 0 \Rightarrow \lim_{x\to\infty} \frac{P(x)}{Q(x)} = -\infty.$$$$

Lean4

theorem abs_div_tendsto_atTop_of_degree_gt (hdeg : Q.degree < P.degree) (hQ : Q ≠ 0) :
    Tendsto (fun x => |eval x P / eval x Q|) atTop atTop :=
  by
  by_cases h : 0 ≤ P.leadingCoeff / Q.leadingCoeff
  · exact tendsto_abs_atTop_atTop.comp (P.div_tendsto_atTop_of_degree_gt Q hdeg hQ h)
  · push_neg at h
    exact tendsto_abs_atBot_atTop.comp (P.div_tendsto_atBot_of_degree_gt Q hdeg hQ h.le)

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