English
For measurable f and g and a measurable set s, the volume (with respect to μ × volume) of the region between f and g over s equals the lintegral over s of ENNReal.ofReal(g − f).
Русский
Для измеримых f и g и измеримого множества s объём области между f и g над s равен линегралу по s от ENNReal.ofReal(g − f).
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
theorem volume_regionBetween_eq_lintegral' (hf : Measurable f) (hg : Measurable g) (hs : MeasurableSet s) :
μ.prod volume (regionBetween f g s) = ∫⁻ y in s, ENNReal.ofReal ((g - f) y) ∂μ := by
classical
rw [Measure.prod_apply]
· have h : (fun x => volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)}) = s.indicator fun x => ENNReal.ofReal (g x - f x) :=
by
funext x
rw [indicator_apply]
split_ifs with h
· have hx : {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = Ioo (f x) (g x) := by simp [h, Ioo]
simp only [hx, Real.volume_Ioo]
· have hx : {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = ∅ := by simp [h]
simp only [hx, measure_empty]
dsimp only [regionBetween, preimage_setOf_eq]
rw [h, lintegral_indicator] <;> simp only [hs, Pi.sub_apply]
· exact measurableSet_regionBetween hf hg hs
