internlm/Lean-Github huggingface dataset:
Theorem: mean_squeeze
Proof state before:
case refine_1
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 ∈ t, f x ≤ (fun x => m) x
Tactic:
intro y yt
Proof state after:
case refine_1
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
y : X
yt : y ∈ t
⊢ f y ≤ (fun x => m) y
Theorem: mean_squeeze
Proof state before:
case refine_1
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
y : X
yt : y ∈ t
⊢ f y ≤ (fun x => m) y
Tactic:
rw [← ht] at yt
Proof state after:
case refine_1
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
y : X
yt : y ∈ s ∩ ball x e
⊢ f y ≤ (fun x => m) y
Theorem: mean_squeeze
Proof state before:
case refine_1
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
y : X
yt : y ∈ s ∩ ball x e
⊢ f y ≤ (fun x => m) y
Tactic:
simp at ht yt
Proof state after:
case refine_1
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
y : X
yt : y ∈ s ∧ dist y x < e
⊢ f y ≤ (fun x => m) y
Theorem: mean_squeeze
Proof state before:
case refine_1
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
y : X
yt : y ∈ s ∧ dist y x < e
⊢ f y ≤ (fun x => m) y
Tactic:
specialize he y yt.left yt.right
Proof state after:
case refine_1
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
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
y : X
yt : y ∈ s ∧ dist y x < e
he : dist (f y) (f x) < (b - f x) / 2
⊢ f y ≤ (fun x => m) y
Theorem: mean_squeeze
Proof state before:
case refine_1
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
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
y : X
yt : y ∈ s ∧ dist y x < e
he : dist (f y) (f x) < (b - f x) / 2
⊢ f y ≤ (fun x => m) y
Tactic:
simp [Real.dist_eq] at he
Proof state after:
case refine_1
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
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
y : X
yt : y ∈ s ∧ dist y x < e
he : |f y - f x| < (b - f x) / 2
⊢ f y ≤ (fun x => m) y
Theorem: mean_squeeze
Proof state before:
case refine_1
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
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
y : X
yt : y ∈ s ∧ dist y x < e
he : |f y - f x| < (b - f x) / 2
⊢ f y ≤ (fun x => m) y
Tactic:
calc f y
  _ = f x + (f y - f x) := by ring
  _ ≤ f x + |f y - f x| := by bound
  _ ≤ f x + (b - f x) / 2 := by bound
  _ = (b + f x) / 2 := by ring
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
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
y : X
yt : y ∈ s ∧ dist y x < e
he : |f y - f x| < (b - f x) / 2
⊢ f y = f x + (f y - f x)
Tactic:
ring
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
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
y : X
yt : y ∈ s ∧ dist y x < e
he : |f y - f x| < (b - f x) / 2
⊢ f x + (f y - f x) ≤ f x + |f y - f x|
Tactic:
bound
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
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
y : X
yt : y ∈ s ∧ dist y x < e
he : |f y - f x| < (b - f x) / 2
⊢ f x + |f y - f x| ≤ f x + (b - f x) / 2
Tactic:
bound
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
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
y : X
yt : y ∈ s ∧ dist y x < e
he : |f y - f x| < (b - f x) / 2
⊢ f x + (b - f x) / 2 = (b + f x) / 2
Tactic:
ring
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 < ⊤
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
i1 : ∫ (x : X) in t, f x ≤ vt * m
⊢ (∫ (x : X) in s \ t, f x) + ∫ (x : X) in t, f x ≤ (vs - vt) * b + vt * m
Tactic:
bound
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 < ⊤
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
i1 : ∫ (x : X) in t, f x ≤ vt * m
⊢ (vs - vt) * b + vt * m = vs * b - vt * (b - m)
Tactic:
ring
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 < ⊤
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
i1 : ∫ (x : X) in t, f x ≤ vt * m
⊢ 0 < vt * (b - m)
Tactic:
bound
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 < ⊤
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
i1 : ∫ (x : X) in t, f x ≤ vt * m
⊢ vs * b - 0 = b * vs
Tactic:
ring
Proof state after:
no goals
Theorem: mean_squeeze
Proof state before:
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
Tactic:
rw [disjoint_comm]
Proof state after:
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 t (s \ t)
Theorem: mean_squeeze
Proof state before:
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 t (s \ t)
Tactic:
exact Set.disjoint_sdiff_right
Proof state after:
no goals
Theorem: mean_squeeze
Proof state before:
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
Tactic:
exact tm
Proof state after:
no goals