testAgainstNN — Mathlib

English

The product-measure map from pairs of finite measures to measures on the product space is measurable.

Русский

Отображение произведения мер распространяется на пары конечных мер и является измеримым на произведённом пространстве.

LaTeX

$$$\Measurable(\lambda (\mu, \nu) \mapsto \mu.toMeasure.prod \nu.toMeasure)$$$

Lean4

/-- The pairing of a finite (Borel) measure `μ` with a nonnegative bounded continuous
function is obtained by (Lebesgue) integrating the (test) function against the measure.
This is `MeasureTheory.FiniteMeasure.testAgainstNN`. -/
def testAgainstNN (μ : FiniteMeasure Ω) (f : Ω →ᵇ ℝ≥0) : ℝ≥0 :=
  (∫⁻ ω, f ω ∂(μ : Measure Ω)).toNNReal

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