internlm/Lean-Github huggingface dataset:
Theorem: mean_squeeze
Proof state before:
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
⊢ (b - f x) / 2 > 0
Tactic:
linarith
Proof state after:
no goals
Theorem: mean_squeeze
Proof state before:
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
⊢ t ⊆ s
Tactic:
rw [← ht]
Proof state after:
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
⊢ s ∩ ball x e ⊆ s
Theorem: mean_squeeze
Proof state before:
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
⊢ s ∩ ball x e ⊆ s
Tactic:
exact Set.inter_subset_left _ _
Proof state after:
no goals
Theorem: mean_squeeze
Proof state before:
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 < ⊤
⊢ MeasurableSet t
Tactic:
rw [← ht]
Proof state after:
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 < ⊤
⊢ MeasurableSet (s ∩ ball x e)
Theorem: mean_squeeze
Proof state before:
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 < ⊤
⊢ MeasurableSet (s ∩ ball x e)
Tactic:
exact MeasurableSet.inter sn.measurable measurableSet_ball
Proof state after:
no goals
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 s).toReal⁻¹ * ((∫ (x : X) in s \ t, f x) + ∫ (x : X) in t, f x) < b
Tactic:
set m := (b + f x) / 2
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
m : ℝ := (b + f x) / 2
⊢ (↑volume s).toReal⁻¹ * ((∫ (x : X) in s \ t, f x) + ∫ (x : X) in t, f x) < b
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
m : ℝ := (b + f x) / 2
⊢ (↑volume s).toReal⁻¹ * ((∫ (x : X) in s \ t, f x) + ∫ (x : X) in t, f x) < b
Tactic:
set vs := (volume s).toReal
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
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
⊢ vs⁻¹ * ((∫ (x : X) in s \ t, f x) + ∫ (x : X) in t, f x) < b
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
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
⊢ vs⁻¹ * ((∫ (x : X) in s \ t, f x) + ∫ (x : X) in t, f x) < b
Tactic:
set vt := (volume t).toReal
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
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
⊢ vs⁻¹ * ((∫ (x : X) in s \ t, f x) + ∫ (x : X) in t, f x) < b
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
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
⊢ vs⁻¹ * ((∫ (x : X) in s \ t, f x) + ∫ (x : X) in t, f x) < b
Tactic:
have vsp : vs > 0 := sn.real_pos
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
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
⊢ vs⁻¹ * ((∫ (x : X) in s \ t, f x) + ∫ (x : X) in t, f x) < b
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
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
⊢ vs⁻¹ * ((∫ (x : X) in s \ t, f x) + ∫ (x : X) in t, f x) < b
Tactic:
have vtp : vt > 0 := ENNReal.toReal_pos (vtp'.ne') (lt_top_iff_ne_top.mp tf)
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
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
⊢ vs⁻¹ * ((∫ (x : X) in s \ t, f x) + ∫ (x : X) in t, f x) < b
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
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
⊢ vs⁻¹ * ((∫ (x : X) in s \ t, f x) + ∫ (x : X) in t, f x) < b
Tactic:
rw [inv_mul_lt_iff' vsp]
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
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
⊢ (∫ (x : X) in s \ t, f x) + ∫ (x : X) in t, f x < b * vs
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
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
⊢ (∫ (x : X) in s \ t, f x) + ∫ (x : X) in t, f x < b * vs
Tactic:
have mb : m < b := by
  calc (b + f x) / 2
    _ < (b + b) / 2 := (div_lt_div_right (by norm_num)).mpr (by bound)
    _ = b := by ring
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
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
mb : m < b
⊢ (∫ (x : X) in s \ t, f x) + ∫ (x : X) in t, f x < b * vs
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
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
mb : m < b
⊢ (∫ (x : X) in s \ t, f x) + ∫ (x : X) in t, f x < b * vs
Tactic:
have i0 : ∫ x in s \ t, f x ≤ (vs - vt) * b := by
  have df : volume (s \ t) < ⊤ := lt_of_le_of_lt (measure_mono (Set.diff_subset _ _)) sn.finite
  have dm : MeasurableSet (s \ t) := MeasurableSet.diff sn.measurable tm
  have fb := @setIntegral_mono_on _ _ volume f (fun _ ↦ b) (s \ t)
    (fi.mono (Set.diff_subset _ _) (le_refl _)) (integrableOn_const.mpr (Or.inr df)) dm ?_
  simp [measure_diff ts tm (lt_top_iff_ne_top.mp tf),
    ENNReal.toReal_sub_of_le (measure_mono ts) (lt_top_iff_ne_top.mp sn.finite)] at fb
  exact fb
  intro y yd; simp at yd; exact hi y yd.left
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
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
mb : m < b
i0 : ∫ (x : X) in s \ t, f x ≤ (vs - vt) * b
⊢ (∫ (x : X) in s \ t, f x) + ∫ (x : X) in t, f x < b * vs