Theorems · Theorem · probability

MeasureTheory.BoundedContinuousFunction.integral_eq_integral_meas_le

∀ {α : Type u_2} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] [OpensMeasurableSpace α]
  (f : BoundedContinuousFunction α ℝ) (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ],
  0 ≤ᵐ[μ] ⇑f → ∫ (ω : α), f ω ∂μ = ∫ (t : ℝ) in Set.Ioc 0 ‖f‖, μ.real {a | t ≤ f a}

A version of the layer cake formula for bounded continuous functions and finite measures: ∫ f dμ = ∫ t in (0, ‖f‖], μ {x | f(x) ≥ t} dt.

Defined in

Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Cited by

2 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceTopologicalSpaceOpensMeasurableSpaceMeasureTheory.IsFiniteMeasure