English
If f and g are integrable on s and f ≤ g almost everywhere, then the same identity as above holds, namely the volume of the region between f and g equals the integral of g − f over s.
Русский
Если f и g интегрируемы на s и почти везде выполняется f ≤ g, то то же равенство: объем области между f и g над s равен интегралу по s от (g − f).
LaTeX
$$$\mu\times\mathrm{volume}(\mathrm{regionBetween}(f,g,s)) = \mathrm{ENNReal.ofReal}\left( \int_s (g - f) \, d\mu \right)$$$
Lean4
/-- If two functions are integrable on a measurable set, and one function is less than
or equal to the other on that set, then the volume of the region
between the two functions can be represented as an integral. -/
theorem volume_regionBetween_eq_integral [SigmaFinite μ] (f_int : IntegrableOn f s μ) (g_int : IntegrableOn g s μ)
(hs : MeasurableSet s) (hfg : ∀ x ∈ s, f x ≤ g x) :
μ.prod volume (regionBetween f g s) = ENNReal.ofReal (∫ y in s, (g - f) y ∂μ) :=
volume_regionBetween_eq_integral' f_int g_int hs ((ae_restrict_iff' hs).mpr (Eventually.of_forall hfg))
