delta — Mathlib

English

The Dirac delta distribution assigns to a function its value at a point via evaluation as a distribution.

Русский

Распределение Дирака приписывает функции значение в точке посредством оценки как распределения.

LaTeX

$$$$ \\delta_x : f \\mapsto f(x). $$$$

Lean4

/-- The Dirac delta distribution -/
def delta (x : E) : 𝓢(E, F) →L[𝕜] F :=
  (BoundedContinuousFunction.evalCLM 𝕜 x).comp (toBoundedContinuousFunctionCLM 𝕜 E F)

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