charFun_dirac — Mathlib

English

For any r ∈ E and μ, χ_{μ map (r + ·)}(t) = χ_{μ}(t) e^{i⟪r,t⟫}.

Русский

Для любого r и меры μ выполняется χ_{μ∘(r+·)}(t) = χ_{μ}(t) e^{i⟪r,t⟫}.

LaTeX

$$$$\\chi_{\\mu \\mapsto (r + \\cdot)}(t) = \\chi_{\\mu}(t) e^{i \\langle r,t \\rangle}.$$$$

Lean4

@[simp]
theorem charFun_dirac [OpensMeasurableSpace E] {x : E} (t : E) : charFun (Measure.dirac x) t = cexp (⟪x, t⟫ * I) := by
  rw [charFun_apply, integral_dirac]

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