toWeakDualBCNN — Mathlib

English

Probability measures yield elements of the WeakDual NNReal (BoundedContinuousFunction Ω NNReal) by integration with respect to the measure.

Русский

Вероятности дают элементы слабого двойственного пространства NNReal(BoundedContinuousFunction Ω NNReal) через интегрирование по мере.

LaTeX

$$$\\text{toWeakDualBCNN}: \\text{ProbabilityMeasure } \\Omega \\to \\text{WeakDual NNReal (} \\Omega \\to\\!\\!\\!\\!{\\text{BoundedContinuousFunction }\\Omega\\; NNReal)}$$$

Lean4

/-- Probability measures yield elements of the `WeakDual` of bounded continuous nonnegative
functions via `MeasureTheory.FiniteMeasure.testAgainstNN`, i.e., integration. -/
def toWeakDualBCNN : ProbabilityMeasure Ω → WeakDual ℝ≥0 (Ω →ᵇ ℝ≥0) :=
  FiniteMeasure.toWeakDualBCNN ∘ toFiniteMeasure

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