hasDerivAt_sigmoid — Mathlib

English

For each x ∈ ℝ, the derivative of sigmoid at x is sigmoid(x) · (1 − sigmoid(x)).

Русский

Для каждого x ∈ ℝ производная сигмоиды по x равна сигмоид(x) · (1 − сигмоид(x)).

LaTeX

$$$\text{HasDerivAt}(\operatorname{sigmoid},\operatorname{sigmoid}(x)\cdot(1-\operatorname{sigmoid}(x)),x)$$$

Lean4

theorem hasDerivAt_sigmoid (x : ℝ) : HasDerivAt sigmoid (sigmoid x * (1 - sigmoid x)) x :=
  by
  convert (hasDerivAt_neg' x |>.exp.const_add 1 |>.inv <| by positivity) using 1
  rw [← sigmoid_neg, ← sigmoid_mul_rexp_neg x, sigmoid_def]
  field_simp [sq]

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