charFun — Mathlib

English

Let E be a real inner product space and μ a finite measure on E. The characteristic function χ_μ of μ is the function χ_μ: E → ℂ given by χ_μ(t) = ∫_E e^{i⟨x,t⟩} dμ(x). It is the Fourier transform of μ.

Русский

Пусть E — вещественное евклидово пространство, μ — конечная мера на 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

/-- The characteristic function of a measure in an inner product space. -/
noncomputable def charFun [Inner ℝ E] (μ : Measure E) (t : E) : ℂ :=
  ∫ x, exp (⟪x, t⟫ * I) ∂μ

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