Theorems · Definition · measure theory

MeasureTheory.FiniteMeasure.testAgainstNN

{Ω : Type u_1} →
  [inst : MeasurableSpace Ω] →
    [inst_1 : TopologicalSpace Ω] → MeasureTheory.FiniteMeasure Ω → BoundedContinuousFunction Ω NNReal → NNReal

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.

Defined in

Mathlib.MeasureTheory.Measure.FiniteMeasure

Cited by

27 results in Mathlib

Foundations

Depth 175 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasurableSpaceTopologicalSpace