English
If f and g are integrable on a measurable set s and f ≤ g a.e., then the volume of the region between f and g over s equals the integral over s of (g − f).
Русский
Если 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
theorem volume_regionBetween_eq_integral' [SigmaFinite μ] (f_int : IntegrableOn f s μ) (g_int : IntegrableOn g s μ)
(hs : MeasurableSet s) (hfg : f ≤ᵐ[μ.restrict s] g) :
μ.prod volume (regionBetween f g s) = ENNReal.ofReal (∫ y in s, (g - f) y ∂μ) :=
by
have h : g - f =ᵐ[μ.restrict s] fun x => Real.toNNReal (g x - f x) :=
hfg.mono fun x hx => (Real.coe_toNNReal _ <| sub_nonneg.2 hx).symm
rw [volume_regionBetween_eq_lintegral f_int.aemeasurable g_int.aemeasurable hs, integral_congr_ae h,
lintegral_congr_ae, lintegral_coe_eq_integral _ ((integrable_congr h).mp (g_int.sub f_int))]
dsimp only
rfl
