English
If levyProkhorovEDist μ ν < ε and f is a bounded continuous function with finite integral, then the expected value of f under μ is controlled by the ν-measure of thickened sublevel sets of f plus ε times the bound of f.
Русский
Если расстояние Леви–Прокхоров меньше ε и f ограничена непрерывна, то Eμ[f] контролируется через ν-измеримость размытых подмножеств f и ε, умноженное на предел f.
LaTeX
$$$\\int f\,dμ ≤ \\int_{0}^{‖f‖} ν(\\mathrm{thickening}(ε, \\{x: t ≤ f(x)\\}))\,dt + ε‖f‖.$$$
Lean4
/-- 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. -/
theorem integral_eq_integral_meas_le {α : Type*} [MeasurableSpace α] [TopologicalSpace α] [OpensMeasurableSpace α]
(f : α →ᵇ ℝ) (μ : Measure α) [IsFiniteMeasure μ] (f_nn : 0 ≤ᵐ[μ] f) :
∫ ω, f ω ∂μ = ∫ t in Ioc 0 ‖f‖, μ.real {a : α | t ≤ f a} :=
integral_eq_integral_meas_le_of_hasFiniteIntegral _ _ f_nn (f.integrable μ).2
