α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ (∫⁻ (x : α), ↑↑volume (Prod.mk x ⁻¹' regionBetween f g s) ∂μ) = ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ

α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ MeasurableSet (regionBetween f g s)
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ ↑↑(Measure.prod μ volume) (regionBetween f g s) = ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ
rw [Measure.prod_apply]
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
h : (fun x => ↑↑volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)}) = indicator s fun x => ofReal (g x - f x)
⊢ (∫⁻ (x : α), ↑↑volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} ∂μ) = ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
h : (fun x => ↑↑volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)}) = indicator s fun x => ofReal (g x - f x)
⊢ (∫⁻ (x : α), ↑↑volume (Prod.mk x ⁻¹' regionBetween f g s) ∂μ) = ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ
dsimp only [regionBetween, preimage_setOf_eq]
no goals
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
h : (fun x => ↑↑volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)}) = indicator s fun x => ofReal (g x - f x)
⊢ (∫⁻ (x : α), ↑↑volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} ∂μ) = ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ
rw [h, lintegral_indicator] <;> simp only [hs, Pi.sub_apply]
case h
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
x : α
⊢ ↑↑volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = indicator s (fun x => ofReal (g x - f x)) x
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ (fun x => ↑↑volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)}) = indicator s fun x => ofReal (g x - f x)
funext x
case h
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
x : α
⊢ ↑↑volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = if x ∈ s then ofReal (g x - f x) else 0
case h
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
x : α
⊢ ↑↑volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = indicator s (fun x => ofReal (g x - f x)) x
rw [indicator_apply]
case h.inl
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
x : α
h : x ∈ s
⊢ ↑↑volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = ofReal (g x - f x)

case h.inr
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
x : α
h : ¬x ∈ s
⊢ ↑↑volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = 0
case h
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
x : α
⊢ ↑↑volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = if x ∈ s then ofReal (g x - f x) else 0
split_ifs with h
case h.inl
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
x : α
h : x ∈ s
hx : {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = Ioo (f x) (g x)
⊢ ↑↑volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = ofReal (g x - f x)
case h.inl
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
x : α
h : x ∈ s
⊢ ↑↑volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = ofReal (g x - f x)
have hx : { a | x ∈ s ∧ a ∈ Ioo (f x) (g x) } = Ioo (f x) (g x) := by simp [h, Ioo]
no goals
case h.inl
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
x : α
h : x ∈ s
hx : {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = Ioo (f x) (g x)
⊢ ↑↑volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = ofReal (g x - f x)
simp only [hx, Real.volume_Ioo, sub_zero]
no goals
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
x : α
h : x ∈ s
⊢ {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = Ioo (f x) (g x)
simp [h, Ioo]
case h.inr
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
x : α
h : ¬x ∈ s
hx : {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = ∅
⊢ ↑↑volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = 0
case h.inr
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
x : α
h : ¬x ∈ s
⊢ ↑↑volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = 0
have hx : { a | x ∈ s ∧ a ∈ Ioo (f x) (g x) } = ∅ := by simp [h]
no goals
case h.inr
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
x : α
h : ¬x ∈ s
hx : {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = ∅
⊢ ↑↑volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = 0
simp only [hx, measure_empty]
no goals
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
x : α
h : ¬x ∈ s
⊢ {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = ∅
simp [h]
no goals
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ MeasurableSet (regionBetween f g s)
exact measurableSet_regionBetween hf hg hs