mulExpNegSq_apply

Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq

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

English

The value of mulExpNegMulSq ε x is by definition x e^{-(ε x^2)}.

Русский

Значение mulExpNegMulSq ε x определяется как x e^{-(ε x^2)}.

LaTeX

$$$\mulExpNegMulSq(\varepsilon, x) = x \exp(-\varepsilon x^2)$$$

Lean4

theorem mulExpNegSq_apply (ε x : ℝ) : mulExpNegMulSq ε x = x * exp (-(ε * x * x)) :=
  rfl

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

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

Разделы

Аффилиация

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