internlm/Lean-Github huggingface dataset:
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
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
Tactic:
have i1 : ∫ x in t, f x ≤ vt * m := by
  have fm := @setIntegral_mono_on _ _ volume f (fun _ ↦ m) t (fi.mono ts (le_refl _))
    (integrableOn_const.mpr (Or.inr tf)) tm ?_
  simp at fm; exact fm
  intro y yt
  rw [← ht] at yt; simp at ht yt
  specialize he y yt.left yt.right
  simp [Real.dist_eq] at he
  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:
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
i1 : ∫ (x : X) in t, f x ≤ vt * m
⊢ (∫ (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
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 < b * vs
Tactic:
calc (∫ x : X in s \ t, f x) + ∫ x : X in t, f x
  _ ≤ (vs - vt) * b + vt * m := by bound
  _ = vs * b - vt * (b - m) := by ring
  _ < vs * b - 0 := (sub_lt_sub_left (by bound) _)
  _ = b * vs := 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
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
⊢ m < b
Tactic:
calc (b + f x) / 2
  _ < (b + b) / 2 := (div_lt_div_right (by norm_num)).mpr (by bound)
  _ = b := 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
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
⊢ 0 < 2
Tactic:
norm_num
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
⊢ b + f x < b + b
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
⊢ (b + b) / 2 = b
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
⊢ ∫ (x : X) in s \ t, f x ≤ (vs - vt) * b
Tactic:
have df : volume (s \ t) < ⊤ := lt_of_le_of_lt (measure_mono (Set.diff_subset _ _)) sn.finite
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 < ⊤
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
df : ↑volume (s \ t) < ⊤
⊢ ∫ (x : X) in s \ t, f x ≤ (vs - vt) * b
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
df : ↑volume (s \ t) < ⊤
⊢ ∫ (x : X) in s \ t, f x ≤ (vs - vt) * b
Tactic:
have dm : MeasurableSet (s \ t) := MeasurableSet.diff sn.measurable tm
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 < ⊤
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
df : ↑volume (s \ t) < ⊤
dm : MeasurableSet (s \ t)
⊢ ∫ (x : X) in s \ t, f x ≤ (vs - vt) * b
Theorem: mean_squeeze
Proof state before:
case refine_2
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
df : ↑volume (s \ t) < ⊤
dm : MeasurableSet (s \ t)
fb : ∫ (x : X) in s \ t, f x ≤ ((↑volume s).toReal - (↑volume t).toReal) * b
⊢ ∫ (x : X) in s \ t, f x ≤ (vs - vt) * b

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
df : ↑volume (s \ t) < ⊤
dm : MeasurableSet (s \ t)
⊢ ∀ x ∈ s \ t, f x ≤ (fun x => b) x
Tactic:
exact fb
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
df : ↑volume (s \ t) < ⊤
dm : MeasurableSet (s \ t)
⊢ ∀ x ∈ s \ t, f x ≤ (fun x => b) x
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
df : ↑volume (s \ t) < ⊤
dm : MeasurableSet (s \ t)
⊢ ∀ x ∈ s \ t, f x ≤ (fun x => b) x
Tactic:
intro y yd
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
df : ↑volume (s \ t) < ⊤
dm : MeasurableSet (s \ t)
y : X
yd : y ∈ s \ t
⊢ f y ≤ (fun x => b) 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
df : ↑volume (s \ t) < ⊤
dm : MeasurableSet (s \ t)
y : X
yd : y ∈ s \ t
⊢ f y ≤ (fun x => b) y
Tactic:
simp at yd
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
df : ↑volume (s \ t) < ⊤
dm : MeasurableSet (s \ t)
y : X
yd : y ∈ s ∧ y ∉ t
⊢ f y ≤ (fun x => b) 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
df : ↑volume (s \ t) < ⊤
dm : MeasurableSet (s \ t)
y : X
yd : y ∈ s ∧ y ∉ t
⊢ f y ≤ (fun x => b) y
Tactic:
exact hi y yd.left
Proof state after:
no goals
Theorem: mean_squeeze
Proof state before:
case refine_2
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
fm : ∫ (x : X) in t, f x ≤ (↑volume t).toReal * m
⊢ ∫ (x : X) in t, f x ≤ vt * m

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:
exact fm
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
⊢ ∀ x ∈ t, f x ≤ (fun x => m) x