sigmoid_mul_rexp_neg

Mathlib.Analysis.SpecialFunctions.Sigmoid

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

English

sigmoid(x) · exp(−x) = sigmoid(−x).

Русский

sigmoid(x) · exp(−x) = sigmoid(−x).

LaTeX

$$$\operatorname{sigmoid}(x) \cdot e^{-x} = \operatorname{sigmoid}(-x)$$$

Lean4

theorem sigmoid_mul_rexp_neg (x : ℝ) : sigmoid x * exp (-x) = sigmoid (-x) :=
  by
  rw [sigmoid_neg, sigmoid_def]
  field_simp
  ring

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

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

Разделы

Аффилиация

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