mulExpNegMulSq — Mathlib

English

The function F(ε,x) = x e^{-(ε x^2)} defines a damping of x by a Gaussian factor.

Русский

Функция F(ε,x) = x e^{-(ε x^2)} задаёт затухание x гауссовым коэффициентом.

LaTeX

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

Lean4

/-- Mapping `fun ε x => x * Real.exp (- (ε * x * x))`. By composition, it can be used to transform
functions into bounded functions.
-/
noncomputable def mulExpNegMulSq (ε x : ℝ) :=
  x * exp (-(ε * x * x))

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