dslope_sub_smul — Mathlib

English

The slope of the function x ↦ (x − a) f(x) at a equals the function update of f at a by the derivative of x ↦ (x − a) f(x) evaluated at a.

Русский

У slope функции x ↦ (x − a) f(x) в точке a равен функция обновления f в точке a значением производной x ↦ (x − a) f(x) в a.

LaTeX

$$$\mathrm{dslope}\bigl(x \mapsto (x - a) \cdot f(x)\bigr)\ a = \mathrm{update}\ f\ a\Bigl( \mathrm{deriv}\bigl(x \mapsto (x - a) \cdot f(x)\bigr) a \Bigr)$$$

Lean4

theorem dslope_sub_smul [DecidableEq 𝕜] (f : 𝕜 → E) (a : 𝕜) :
    dslope (fun x => (x - a) • f x) a = update f a (deriv (fun x => (x - a) • f x) a) :=
  eq_update_iff.2 ⟨dslope_same _ _, eqOn_dslope_sub_smul f a⟩

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