α : Type u_1
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
f g : α → ℝ
s : Set α
inst✝ : SigmaFinite μ
f_int : IntegrableOn f s
g_int : IntegrableOn g s
hs : MeasurableSet s
hfg : f ≤ᶠ[ae (Measure.restrict μ s)] g
h : g - f =ᶠ[ae (Measure.restrict μ s)] fun x => ↑(Real.toNNReal (g x - f x))
⊢ ↑↑(Measure.prod μ volume) (regionBetween f g s) = ENNReal.ofReal (∫ (y : α) in s, (g - f) y ∂μ)
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
f g : α → ℝ
s : Set α
inst✝ : SigmaFinite μ
f_int : IntegrableOn f s
g_int : IntegrableOn g s
hs : MeasurableSet s
hfg : f ≤ᶠ[ae (Measure.restrict μ s)] g
⊢ ↑↑(Measure.prod μ volume) (regionBetween f g s) = ENNReal.ofReal (∫ (y : α) in s, (g - f) y ∂μ)
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
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
f g : α → ℝ
s : Set α
inst✝ : SigmaFinite μ
f_int : IntegrableOn f s
g_int : IntegrableOn g s
hs : MeasurableSet s
hfg : f ≤ᶠ[ae (Measure.restrict μ s)] g
h : g - f =ᶠ[ae (Measure.restrict μ s)] fun x => ↑(Real.toNNReal (g x - f x))
⊢ (fun y => ENNReal.ofReal ((g - f) y)) =ᶠ[ae (Measure.restrict μ s)] fun a => ↑(Real.toNNReal (g a - f a))
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
f g : α → ℝ
s : Set α
inst✝ : SigmaFinite μ
f_int : IntegrableOn f s
g_int : IntegrableOn g s
hs : MeasurableSet s
hfg : f ≤ᶠ[ae (Measure.restrict μ s)] g
h : g - f =ᶠ[ae (Measure.restrict μ s)] fun x => ↑(Real.toNNReal (g x - f x))
⊢ ↑↑(Measure.prod μ volume) (regionBetween f g s) = ENNReal.ofReal (∫ (y : α) in s, (g - f) y ∂μ)
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))]
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
f g : α → ℝ
s : Set α
inst✝ : SigmaFinite μ
f_int : IntegrableOn f s
g_int : IntegrableOn g s
hs : MeasurableSet s
hfg : f ≤ᶠ[ae (Measure.restrict μ s)] g
h : g - f =ᶠ[ae (Measure.restrict μ s)] fun x => ↑(Real.toNNReal (g x - f x))
⊢ (fun y => ENNReal.ofReal ((g - f) y)) =ᶠ[ae (Measure.restrict μ s)] fun a => ↑(Real.toNNReal (g a - f a))
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
f g : α → ℝ
s : Set α
inst✝ : SigmaFinite μ
f_int : IntegrableOn f s
g_int : IntegrableOn g s
hs : MeasurableSet s
hfg : f ≤ᶠ[ae (Measure.restrict μ s)] g
h : g - f =ᶠ[ae (Measure.restrict μ s)] fun x => ↑(Real.toNNReal (g x - f x))
⊢ (fun y => ENNReal.ofReal ((g - f) y)) =ᶠ[ae (Measure.restrict μ s)] fun a => ↑(Real.toNNReal (g a - f a))
dsimp only
no goals
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
f g : α → ℝ
s : Set α
inst✝ : SigmaFinite μ
f_int : IntegrableOn f s
g_int : IntegrableOn g s
hs : MeasurableSet s
hfg : f ≤ᶠ[ae (Measure.restrict μ s)] g
h : g - f =ᶠ[ae (Measure.restrict μ s)] fun x => ↑(Real.toNNReal (g x - f x))
⊢ (fun y => ENNReal.ofReal ((g - f) y)) =ᶠ[ae (Measure.restrict μ s)] fun a => ↑(Real.toNNReal (g a - f a))
rfl