charFun_apply — Mathlib

English

For any inner product space E over ℝ and any measure μ on E, the characteristic function χ_μ evaluated at t is χ_μ(t) = ∫_E e^{i⟪x,t⟫} dμ(x).

Русский

Для любой меры μ на евклидовом пространстве E над ℝ верна формула χ_μ(t) = ∫_E e^{i⟪x,t⟫} dμ(x).

LaTeX

$$$$\\chi_{\\mu}(t) = \\int_E e^{i \\langle x,t \\rangle} \\, d\\mu(x).$$$$

Lean4

theorem charFun_apply [Inner ℝ E] (t : E) : charFun μ t = ∫ x, exp (⟪x, t⟫ * I) ∂μ :=
  rfl

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