hasStrictDerivAt — Mathlib

English

The aeval map has a strict derivative given by aeval x (derivative q) translated through the algebra map.

Русский

Функция aeval имеет строгую производную, соответствующую производной q через алгебраическое отображение.

LaTeX

$$$HasStrictDerivAt\$x \\mapsto aeval x q\\, aeval x (derivative q)\\, x\$$$$

Lean4

/-- The derivative (in the analysis sense) of a polynomial `p` is given by `p.derivative`. -/
protected theorem hasStrictDerivAt (x : 𝕜) : HasStrictDerivAt (fun x => p.eval x) (p.derivative.eval x) x := by
  induction p using Polynomial.induction_on' with
  | add p q hp hq => simpa using hp.add hq
  | monomial n a => simpa [mul_assoc, derivative_monomial] using (hasStrictDerivAt_pow n x).const_mul a

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