English
Let P be a nonzero polynomial over a normed field. Then f(x) = eval x P is asymptotically equivalent to leadingCoeff(P) x^{deg P} as x → ∞.
Русский
Пусть P — ненулевой многочлен над нормированным полем. Тогда f(x) = eval x P асимптотически эквивалентна leadingCoeff(P) x^{deg P} при x → ∞.
LaTeX
$$$$f(x) = P(x) \sim \text{lc}(P)\, x^{\deg P} \quad \text{as } x \to \infty.$$$$
Lean4
theorem isEquivalent_atTop_lead : (fun x => eval x P) ~[atTop] fun x => P.leadingCoeff * x ^ P.natDegree :=
by
by_cases h : P = 0
· simp [h, IsEquivalent.refl]
· simp only [Polynomial.eval_eq_sum_range, sum_range_succ]
exact
IsLittleO.add_isEquivalent
(IsLittleO.sum fun i hi =>
IsLittleO.const_mul_left
((IsLittleO.const_mul_right fun hz => h <| leadingCoeff_eq_zero.mp hz) <|
isLittleO_pow_pow_atTop_of_lt (mem_range.mp hi))
_)
IsEquivalent.refl
