English
If f and g are a.e.-measurable on s, then the volume of regionBetween f g s equals the lintegral over s of ENNReal.ofReal(g − f).
Русский
Если f и g измеримы почти всюду на s, то объём области между ними над s равен линегралу от g − f на s.
LaTeX
$$$\mu.\text{prod volume}(\text{regionBetween}(f,g,s)) = \int^{\infty}_{y \in s} \text{ENNReal.ofReal}(g(y)-f(y)) \; d\mu$$$
Lean4
/-- The volume of the region between two almost everywhere measurable functions on a measurable set
can be represented as a Lebesgue integral. -/
theorem volume_regionBetween_eq_lintegral [SFinite μ] (hf : AEMeasurable f (μ.restrict s))
(hg : AEMeasurable g (μ.restrict s)) (hs : MeasurableSet s) :
μ.prod volume (regionBetween f g s) = ∫⁻ y in s, ENNReal.ofReal ((g - f) y) ∂μ :=
by
have h₁ :
(fun y => ENNReal.ofReal ((g - f) y)) =ᵐ[μ.restrict s] fun y =>
ENNReal.ofReal ((AEMeasurable.mk g hg - AEMeasurable.mk f hf) y) :=
(hg.ae_eq_mk.sub hf.ae_eq_mk).fun_comp ENNReal.ofReal
have h₂ :
(μ.restrict s).prod volume (regionBetween f g s) =
(μ.restrict s).prod volume (regionBetween (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s) :=
by
apply measure_congr
apply EventuallyEq.rfl.inter
exact
((quasiMeasurePreserving_fst.ae_eq_comp hf.ae_eq_mk).comp₂ _ EventuallyEq.rfl).inter
(EventuallyEq.rfl.comp₂ _ <| quasiMeasurePreserving_fst.ae_eq_comp hg.ae_eq_mk)
rw [lintegral_congr_ae h₁, ← volume_regionBetween_eq_lintegral' hf.measurable_mk hg.measurable_mk hs]
convert h₂ using 1
· rw [Measure.restrict_prod_eq_prod_univ]
exact (Measure.restrict_eq_self _ (regionBetween_subset f g s)).symm
· rw [Measure.restrict_prod_eq_prod_univ]
exact (Measure.restrict_eq_self _ (regionBetween_subset (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s)).symm
