charFunDual_apply

Mathlib.MeasureTheory.Measure.CharacteristicFunction

URI: https://scilib.ai/kg/mathlib#MeasureTheory.charFunDual_apply

English

The dual characteristic function at L is the integral of exp(i L(v)) with respect to μ.

Русский

Характеристическая функция двойственной меры в точке L равна интегралу exp(i L(v)) по μ.

LaTeX

$$$\\operatorname{charFunDual}(\\mu)(L) = \\int v\\, e^{i\\,L(v)} \\, d\\mu(v)$$$

Lean4

theorem charFunDual_apply (L : StrongDual ℝ E) : charFunDual μ L = ∫ v, exp (L v * I) ∂μ :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru