coe_toWeakDualBCNN

Mathlib.MeasureTheory.Measure.ProbabilityMeasure

URI: https://scilib.ai/kg/mathlib#MeasureTheory.ProbabilityMeasure.coe_toWeakDualBCNN

English

For any μ, the evaluation of μ.toWeakDualBCNN on f equals the integration of f with respect to μ.

Русский

Для любого μ значение μ.toWeakDualBCNN на f равно интегралу f по μ.

LaTeX

$$$(\\text{toWeakDualBCNN}(\\mu))(f) = \\int_{\\Omega} f \\; d\\mu$$$

Lean4

@[simp]
theorem coe_toWeakDualBCNN (μ : ProbabilityMeasure Ω) : ⇑μ.toWeakDualBCNN = μ.toFiniteMeasure.testAgainstNN :=
  rfl

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

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

Разделы

Аффилиация

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