deriv_sigmoid

Mathlib.Analysis.SpecialFunctions.Sigmoid

URI: https://scilib.ai/kg/mathlib#Real.deriv_sigmoid

English

The derivative of sigmoid is sigmoid(x) · (1 − sigmoid(x)).

Русский

Производная сигмоиды равна сигмоид(x) · (1 − сигмоид(x)).

LaTeX

$$$\dfrac{d}{dx}\big( \operatorname{sigmoid}(x) \big) = \operatorname{sigmoid}(x) \cdot (1 - \operatorname{sigmoid}(x))$$$

Lean4

theorem deriv_sigmoid : deriv sigmoid = fun x => sigmoid x * (1 - sigmoid x) :=
  funext fun x => (hasDerivAt_sigmoid x).deriv

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru