probCharDual_apply

Mathlib.MeasureTheory.Measure.CharacteristicFunction

URI: https://scilib.ai/kg/mathlib#BoundedContinuousFunction.probCharDual_apply

English

If the integrals of char across w with respect to two finite measures P and P' agree, then P = P'.

Русский

Если интегралы характеристических функций по P и P' совпадают для всех w, то P = P'.

LaTeX

$$∀ w, ∫ v, char he hL w v ∂P = ∫ v, char he hL w v ∂P' ⇒ P = P'$$

Lean4

theorem probCharDual_apply (L : StrongDual ℝ F) (x : F) : probCharDual L x = exp (L x * I) :=
  rfl

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

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

Разделы

Аффилиация

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