Theorems · Theorem · real analysis

expNegInvGlue.tendsto_polynomial_inv_mul_zero

∀ (p : Polynomial ℝ), Filter.Tendsto (fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x) (nhds 0) (nhds 0)

Our function tends to zero at zero faster than any $P(x^{-1})$, $P∈ℝ[X]$, tends to infinity.

Defined in

Mathlib.Analysis.SpecialFunctions.SmoothTransition

Cited by

1 results in Mathlib

Foundations

Depth 163 from the axioms · uses propext, Classical.choice, Quot.sound