differentiable_polynomial_eval_inv_mul

English

For a polynomial p and real x, the derivative of x ↦ p(x^{-1}) expNegInvGlue x is given by an explicit formula involving p, its derivative, and expNegInvGlue.

Русский

Для многочлена p и вещественного x производная функции x ↦ p(x^{-1}) expNegInvGlue x задается явной формулой, зависящей от p, его производной и expNegInvGlue.

LaTeX

$$$\text{HasDerivAt}\bigl( x\mapsto p(x^{-1}) \exp(-1/x)\bigr) = \text{(explicit)}$$$

Lean4

theorem differentiable_polynomial_eval_inv_mul (p : ℝ[X]) : Differentiable ℝ (fun x ↦ p.eval x⁻¹ * expNegInvGlue x) :=
  fun x ↦ (hasDerivAt_polynomial_eval_inv_mul p x).differentiableAt

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