Theorem: mean_squeeze
Proof state before:
case intro.intro.intro.intro
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
⊢ (↑(volume.restrict s) Set.univ).toReal⁻¹ * ∫ (x : X) in s \ t ∪ t, f x < b
Tactic:
rw [integral_union]
Proof state after:
case intro.intro.intro.intro
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
⊢ (↑(volume.restrict s) Set.univ).toReal⁻¹ * ((∫ (x : X) in s \ t, f x) + ∫ (x : X) in t, f x) < b

case intro.intro.intro.intro.hst
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
⊢ Disjoint (s \ t) t

case intro.intro.intro.intro.ht
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
⊢ MeasurableSet t

case intro.intro.intro.intro.hfs
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
⊢ IntegrableOn (fun x => f x) (s \ t) volume

case intro.intro.intro.intro.hft
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
⊢ IntegrableOn (fun x => f x) t volume