charFunDual_dirac — Mathlib

English

The dual characteristic function of a Dirac measure at x is exp(L x · i).

Русский

Характеристическая функция двойственной меры Дирака в точке x равна exp(i L x).

LaTeX

$$$\operatorname{charFunDual}(\operatorname{Measure.dirac} x)(L) = e^{i\,L(x)}$$$

Lean4

@[simp]
theorem charFunDual_dirac [OpensMeasurableSpace E] {x : E} (L : StrongDual ℝ E) :
    charFunDual (Measure.dirac x) L = cexp (L x * I) := by rw [charFunDual_apply, integral_dirac]

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