charFunDual — Mathlib

English

For a normed space E, the characteristic function of μ at a dual element L coincides with the dual-characteristic function evaluated at the dual map of L applied to the argument.

Русский

Для нормированного пространства E характеристическая функция меры μ в точке двойственного пространства совпадает с двойственной характеристической функцией, примененной к образу через двойную отображение L.

LaTeX

$$$\operatorname{charFun}(\mu)(L) = \operatorname{charFunDual}(\mu)(L\mapsto))$$$

Lean4

/-- The characteristic function of a measure in a normed space, function from `StrongDual ℝ E` to
`ℂ` with `charFunDual μ L = ∫ v, exp (L v * I) ∂μ`. -/
noncomputable def charFunDual (μ : Measure E) (L : StrongDual ℝ E) : ℂ :=
  ∫ v, probCharDual L v ∂μ

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