internlm/Lean-Github huggingface dataset:
Theorem: existsBoundsOn_integral_measure
Proof state before:
case hp_eq
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_pos : 0 < z
p : Measure ℝ
hp : (↑z)⁻¹ • q = p
hp_one : IsProbabilityMeasure (Measure.restrict p s)
⊢ ∫ (x : ℝ) in s, f x ∂p = (∫ (x : ℝ) in s, f x ∂q) / ↑z

case mk.inr
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_pos : 0 < z
p : Measure ℝ
hp : (↑z)⁻¹ • q = p
hp_one : IsProbabilityMeasure (Measure.restrict p s)
hp_eq : ∫ (x : ℝ) in s, f x ∂p = (∫ (x : ℝ) in s, f x ∂q) / ↑z
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)
Tactic:
. rw [← hp]
  simp
  simp [ENNReal.toReal_inv]
  rw [inv_mul_eq_div]
Proof state after:
case mk.inr
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_pos : 0 < z
p : Measure ℝ
hp : (↑z)⁻¹ • q = p
hp_one : IsProbabilityMeasure (Measure.restrict p s)
hp_eq : ∫ (x : ℝ) in s, f x ∂p = (∫ (x : ℝ) in s, f x ∂q) / ↑z
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)
Theorem: existsBoundsOn_integral_measure
Proof state before:
case mk.inr
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_pos : 0 < z
p : Measure ℝ
hp : (↑z)⁻¹ • q = p
hp_one : IsProbabilityMeasure (Measure.restrict p s)
hp_eq : ∫ (x : ℝ) in s, f x ∂p = (∫ (x : ℝ) in s, f x ∂q) / ↑z
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)
Tactic:
have hp_int : Integrable f (p.restrict s)
Proof state after:
case hp_int
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_pos : 0 < z
p : Measure ℝ
hp : (↑z)⁻¹ • q = p
hp_one : IsProbabilityMeasure (Measure.restrict p s)
hp_eq : ∫ (x : ℝ) in s, f x ∂p = (∫ (x : ℝ) in s, f x ∂q) / ↑z
⊢ Integrable f

case mk.inr
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_pos : 0 < z
p : Measure ℝ
hp : (↑z)⁻¹ • q = p
hp_one : IsProbabilityMeasure (Measure.restrict p s)
hp_eq : ∫ (x : ℝ) in s, f x ∂p = (∫ (x : ℝ) in s, f x ∂q) / ↑z
hp_int : Integrable f
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)
Theorem: existsBoundsOn_integral_measure
Proof state before:
case hp_int
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_pos : 0 < z
p : Measure ℝ
hp : (↑z)⁻¹ • q = p
hp_one : IsProbabilityMeasure (Measure.restrict p s)
hp_eq : ∫ (x : ℝ) in s, f x ∂p = (∫ (x : ℝ) in s, f x ∂q) / ↑z
⊢ Integrable f

case mk.inr
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_pos : 0 < z
p : Measure ℝ
hp : (↑z)⁻¹ • q = p
hp_one : IsProbabilityMeasure (Measure.restrict p s)
hp_eq : ∫ (x : ℝ) in s, f x ∂p = (∫ (x : ℝ) in s, f x ∂q) / ↑z
hp_int : Integrable f
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)
Tactic:
. rw [← hp]
  simp  apply Integrable.smul_measure h_int
  simp
  apply hz_pos.ne'
Proof state after:
case mk.inr
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_pos : 0 < z
p : Measure ℝ
hp : (↑z)⁻¹ • q = p
hp_one : IsProbabilityMeasure (Measure.restrict p s)
hp_eq : ∫ (x : ℝ) in s, f x ∂p = (∫ (x : ℝ) in s, f x ∂q) / ↑z
hp_int : Integrable f
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)
Theorem: existsBoundsOn_integral_measure
Proof state before:
case mk.inr
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_pos : 0 < z
p : Measure ℝ
hp : (↑z)⁻¹ • q = p
hp_one : IsProbabilityMeasure (Measure.restrict p s)
hp_eq : ∫ (x : ℝ) in s, f x ∂p = (∫ (x : ℝ) in s, f x ∂q) / ↑z
hp_int : Integrable f
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)
Tactic:
have hp_meas_compl : p.restrict s sᶜ = 0
Proof state after:
case hp_meas_compl
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_pos : 0 < z
p : Measure ℝ
hp : (↑z)⁻¹ • q = p
hp_one : IsProbabilityMeasure (Measure.restrict p s)
hp_eq : ∫ (x : ℝ) in s, f x ∂p = (∫ (x : ℝ) in s, f x ∂q) / ↑z
hp_int : Integrable f
⊢ ↑↑(Measure.restrict p s) sᶜ = 0

case mk.inr
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_pos : 0 < z
p : Measure ℝ
hp : (↑z)⁻¹ • q = p
hp_one : IsProbabilityMeasure (Measure.restrict p s)
hp_eq : ∫ (x : ℝ) in s, f x ∂p = (∫ (x : ℝ) in s, f x ∂q) / ↑z
hp_int : Integrable f
hp_meas_compl : ↑↑(Measure.restrict p s) sᶜ = 0
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)
Theorem: existsBoundsOn_integral_measure
Proof state before:
case hp_meas_compl
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_pos : 0 < z
p : Measure ℝ
hp : (↑z)⁻¹ • q = p
hp_one : IsProbabilityMeasure (Measure.restrict p s)
hp_eq : ∫ (x : ℝ) in s, f x ∂p = (∫ (x : ℝ) in s, f x ∂q) / ↑z
hp_int : Integrable f
⊢ ↑↑(Measure.restrict p s) sᶜ = 0

case mk.inr
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_pos : 0 < z
p : Measure ℝ
hp : (↑z)⁻¹ • q = p
hp_one : IsProbabilityMeasure (Measure.restrict p s)
hp_eq : ∫ (x : ℝ) in s, f x ∂p = (∫ (x : ℝ) in s, f x ∂q) / ↑z
hp_int : Integrable f
hp_meas_compl : ↑↑(Measure.restrict p s) sᶜ = 0
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)
Tactic:
. rw [Measure.restrict_apply (MeasurableSet.compl hs_meas)]
  simp
Proof state after:
case mk.inr
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_pos : 0 < z
p : Measure ℝ
hp : (↑z)⁻¹ • q = p
hp_one : IsProbabilityMeasure (Measure.restrict p s)
hp_eq : ∫ (x : ℝ) in s, f x ∂p = (∫ (x : ℝ) in s, f x ∂q) / ↑z
hp_int : Integrable f
hp_meas_compl : ↑↑(Measure.restrict p s) sᶜ = 0
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)
Theorem: existsBoundsOn_integral_measure
Proof state before:
case mk.inr
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_pos : 0 < z
p : Measure ℝ
hp : (↑z)⁻¹ • q = p
hp_one : IsProbabilityMeasure (Measure.restrict p s)
hp_eq : ∫ (x : ℝ) in s, f x ∂p = (∫ (x : ℝ) in s, f x ∂q) / ↑z
hp_int : Integrable f
hp_meas_compl : ↑↑(Measure.restrict p s) sᶜ = 0
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)
Tactic:
have h_lb := @exists_not_mem_null_le_integral _ _ _ _ _ hp_one hp_int hp_meas_compl
Proof state after:
case mk.inr
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_pos : 0 < z
p : Measure ℝ
hp : (↑z)⁻¹ • q = p
hp_one : IsProbabilityMeasure (Measure.restrict p s)
hp_eq : ∫ (x : ℝ) in s, f x ∂p = (∫ (x : ℝ) in s, f x ∂q) / ↑z
hp_int : Integrable f
hp_meas_compl : ↑↑(Measure.restrict p s) sᶜ = 0
h_lb : ∃ x ∉ sᶜ, f x ≤ ∫ (a : ℝ) in s, f a ∂p
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)
Theorem: existsBoundsOn_integral_measure
Proof state before:
case mk.inr
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_pos : 0 < z
p : Measure ℝ
hp : (↑z)⁻¹ • q = p
hp_one : IsProbabilityMeasure (Measure.restrict p s)
hp_eq : ∫ (x : ℝ) in s, f x ∂p = (∫ (x : ℝ) in s, f x ∂q) / ↑z
hp_int : Integrable f
hp_meas_compl : ↑↑(Measure.restrict p s) sᶜ = 0
h_lb : ∃ x ∉ sᶜ, f x ≤ ∫ (a : ℝ) in s, f a ∂p
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)
Tactic:
have h_ub := @exists_not_mem_null_integral_le _ _ _ _ _ hp_one hp_int hp_meas_compl
Proof state after:
case mk.inr
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_pos : 0 < z
p : Measure ℝ
hp : (↑z)⁻¹ • q = p
hp_one : IsProbabilityMeasure (Measure.restrict p s)
hp_eq : ∫ (x : ℝ) in s, f x ∂p = (∫ (x : ℝ) in s, f x ∂q) / ↑z
hp_int : Integrable f
hp_meas_compl : ↑↑(Measure.restrict p s) sᶜ = 0
h_lb : ∃ x ∉ sᶜ, f x ≤ ∫ (a : ℝ) in s, f a ∂p
h_ub : ∃ x ∉ sᶜ, ∫ (a : ℝ) in s, f a ∂p ≤ f x
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)
Theorem: existsBoundsOn_integral_measure
Proof state before:
case mk.inr
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_pos : 0 < z
p : Measure ℝ
hp : (↑z)⁻¹ • q = p
hp_one : IsProbabilityMeasure (Measure.restrict p s)
hp_eq : ∫ (x : ℝ) in s, f x ∂p = (∫ (x : ℝ) in s, f x ∂q) / ↑z
hp_int : Integrable f
hp_meas_compl : ↑↑(Measure.restrict p s) sᶜ = 0
h_lb : ∃ x ∉ sᶜ, f x ≤ ∫ (a : ℝ) in s, f a ∂p
h_ub : ∃ x ∉ sᶜ, ∫ (a : ℝ) in s, f a ∂p ≤ f x
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)
Tactic:
simp at h_lb
Proof state after:
case mk.inr
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_pos : 0 < z
p : Measure ℝ
hp : (↑z)⁻¹ • q = p
hp_one : IsProbabilityMeasure (Measure.restrict p s)
hp_eq : ∫ (x : ℝ) in s, f x ∂p = (∫ (x : ℝ) in s, f x ∂q) / ↑z
hp_int : Integrable f
hp_meas_compl : ↑↑(Measure.restrict p s) sᶜ = 0
h_ub : ∃ x ∉ sᶜ, ∫ (a : ℝ) in s, f a ∂p ≤ f x
h_lb : ∃ x ∈ s, f x ≤ ∫ (a : ℝ) in s, f a ∂p
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)
Theorem: existsBoundsOn_integral_measure
Proof state before:
case mk.inr
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_pos : 0 < z
p : Measure ℝ
hp : (↑z)⁻¹ • q = p
hp_one : IsProbabilityMeasure (Measure.restrict p s)
hp_eq : ∫ (x : ℝ) in s, f x ∂p = (∫ (x : ℝ) in s, f x ∂q) / ↑z
hp_int : Integrable f
hp_meas_compl : ↑↑(Measure.restrict p s) sᶜ = 0
h_ub : ∃ x ∉ sᶜ, ∫ (a : ℝ) in s, f a ∂p ≤ f x
h_lb : ∃ x ∈ s, f x ≤ ∫ (a : ℝ) in s, f a ∂p
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)
Tactic:
simp at h_ub
Proof state after:
case mk.inr
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_pos : 0 < z
p : Measure ℝ
hp : (↑z)⁻¹ • q = p
hp_one : IsProbabilityMeasure (Measure.restrict p s)
hp_eq : ∫ (x : ℝ) in s, f x ∂p = (∫ (x : ℝ) in s, f x ∂q) / ↑z
hp_int : Integrable f
hp_meas_compl : ↑↑(Measure.restrict p s) sᶜ = 0
h_lb : ∃ x ∈ s, f x ≤ ∫ (a : ℝ) in s, f a ∂p
h_ub : ∃ x ∈ s, ∫ (a : ℝ) in s, f a ∂p ≤ f x
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)
Theorem: existsBoundsOn_integral_measure
Proof state before:
case mk.inr
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_pos : 0 < z
p : Measure ℝ
hp : (↑z)⁻¹ • q = p
hp_one : IsProbabilityMeasure (Measure.restrict p s)
hp_eq : ∫ (x : ℝ) in s, f x ∂p = (∫ (x : ℝ) in s, f x ∂q) / ↑z
hp_int : Integrable f
hp_meas_compl : ↑↑(Measure.restrict p s) sᶜ = 0
h_lb : ∃ x ∈ s, f x ≤ ∫ (a : ℝ) in s, f a ∂p
h_ub : ∃ x ∈ s, ∫ (a : ℝ) in s, f a ∂p ≤ f x
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)
Tactic:
rcases h_lb with ⟨m, ⟨hm_mem, hm⟩⟩
Proof state after:
case mk.inr.intro.intro
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_pos : 0 < z
p : Measure ℝ
hp : (↑z)⁻¹ • q = p
hp_one : IsProbabilityMeasure (Measure.restrict p s)
hp_eq : ∫ (x : ℝ) in s, f x ∂p = (∫ (x : ℝ) in s, f x ∂q) / ↑z
hp_int : Integrable f
hp_meas_compl : ↑↑(Measure.restrict p s) sᶜ = 0
h_ub : ∃ x ∈ s, ∫ (a : ℝ) in s, f a ∂p ≤ f x
m : ℝ
hm_mem : m ∈ s
hm : f m ≤ ∫ (a : ℝ) in s, f a ∂p
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)
Theorem: existsBoundsOn_integral_measure
Proof state before:
case mk.inr.intro.intro
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_pos : 0 < z
p : Measure ℝ
hp : (↑z)⁻¹ • q = p
hp_one : IsProbabilityMeasure (Measure.restrict p s)
hp_eq : ∫ (x : ℝ) in s, f x ∂p = (∫ (x : ℝ) in s, f x ∂q) / ↑z
hp_int : Integrable f
hp_meas_compl : ↑↑(Measure.restrict p s) sᶜ = 0
h_ub : ∃ x ∈ s, ∫ (a : ℝ) in s, f a ∂p ≤ f x
m : ℝ
hm_mem : m ∈ s
hm : f m ≤ ∫ (a : ℝ) in s, f a ∂p
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)
Tactic:
rcases h_ub with ⟨M, ⟨hM_mem, hM⟩⟩
Proof state after:
case mk.inr.intro.intro.intro.intro
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_pos : 0 < z
p : Measure ℝ
hp : (↑z)⁻¹ • q = p
hp_one : IsProbabilityMeasure (Measure.restrict p s)
hp_eq : ∫ (x : ℝ) in s, f x ∂p = (∫ (x : ℝ) in s, f x ∂q) / ↑z
hp_int : Integrable f
hp_meas_compl : ↑↑(Measure.restrict p s) sᶜ = 0
m : ℝ
hm_mem : m ∈ s
hm : f m ≤ ∫ (a : ℝ) in s, f a ∂p
M : ℝ
hM_mem : M ∈ s
hM : ∫ (a : ℝ) in s, f a ∂p ≤ f M
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)
Theorem: existsBoundsOn_integral_measure
Proof state before:
case mk.inr.intro.intro.intro.intro
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_pos : 0 < z
p : Measure ℝ
hp : (↑z)⁻¹ • q = p
hp_one : IsProbabilityMeasure (Measure.restrict p s)
hp_eq : ∫ (x : ℝ) in s, f x ∂p = (∫ (x : ℝ) in s, f x ∂q) / ↑z
hp_int : Integrable f
hp_meas_compl : ↑↑(Measure.restrict p s) sᶜ = 0
m : ℝ
hm_mem : m ∈ s
hm : f m ≤ ∫ (a : ℝ) in s, f a ∂p
M : ℝ
hM_mem : M ∈ s
hM : ∫ (a : ℝ) in s, f a ∂p ≤ f M
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)
Tactic:
exists m
Proof state after:
case mk.inr.intro.intro.intro.intro
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_pos : 0 < z
p : Measure ℝ
hp : (↑z)⁻¹ • q = p
hp_one : IsProbabilityMeasure (Measure.restrict p s)
hp_eq : ∫ (x : ℝ) in s, f x ∂p = (∫ (x : ℝ) in s, f x ∂q) / ↑z
hp_int : Integrable f
hp_meas_compl : ↑↑(Measure.restrict p s) sᶜ = 0
m : ℝ
hm_mem : m ∈ s
hm : f m ≤ ∫ (a : ℝ) in s, f a ∂p
M : ℝ
hM_mem : M ∈ s
hM : ∫ (a : ℝ) in s, f a ∂p ≤ f M
⊢ ∃ M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)
Theorem: existsBoundsOn_integral_measure
Proof state before:
case mk.inr.intro.intro.intro.intro
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_pos : 0 < z
p : Measure ℝ
hp : (↑z)⁻¹ • q = p
hp_one : IsProbabilityMeasure (Measure.restrict p s)
hp_eq : ∫ (x : ℝ) in s, f x ∂p = (∫ (x : ℝ) in s, f x ∂q) / ↑z
hp_int : Integrable f
hp_meas_compl : ↑↑(Measure.restrict p s) sᶜ = 0
m : ℝ
hm_mem : m ∈ s
hm : f m ≤ ∫ (a : ℝ) in s, f a ∂p
M : ℝ
hM_mem : M ∈ s
hM : ∫ (a : ℝ) in s, f a ∂p ≤ f M
⊢ ∃ M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)
Tactic:
exists M
Proof state after:
case mk.inr.intro.intro.intro.intro
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_pos : 0 < z
p : Measure ℝ
hp : (↑z)⁻¹ • q = p
hp_one : IsProbabilityMeasure (Measure.restrict p s)
hp_eq : ∫ (x : ℝ) in s, f x ∂p = (∫ (x : ℝ) in s, f x ∂q) / ↑z
hp_int : Integrable f
hp_meas_compl : ↑↑(Measure.restrict p s) sᶜ = 0
m : ℝ
hm_mem : m ∈ s
hm : f m ≤ ∫ (a : ℝ) in s, f a ∂p
M : ℝ
hM_mem : M ∈ s
hM : ∫ (a : ℝ) in s, f a ∂p ≤ f M
⊢ (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)
Theorem: existsBoundsOn_integral_measure
Proof state before:
case mk.inr.intro.intro.intro.intro
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_pos : 0 < z
p : Measure ℝ
hp : (↑z)⁻¹ • q = p
hp_one : IsProbabilityMeasure (Measure.restrict p s)
hp_eq : ∫ (x : ℝ) in s, f x ∂p = (∫ (x : ℝ) in s, f x ∂q) / ↑z
hp_int : Integrable f
hp_meas_compl : ↑↑(Measure.restrict p s) sᶜ = 0
m : ℝ
hm_mem : m ∈ s
hm : f m ≤ ∫ (a : ℝ) in s, f a ∂p
M : ℝ
hM_mem : M ∈ s
hM : ∫ (a : ℝ) in s, f a ∂p ≤ f M
⊢ (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)
Tactic:
apply And.intro ⟨hm_mem, hM_mem⟩
Proof state after:
case mk.inr.intro.intro.intro.intro
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_pos : 0 < z
p : Measure ℝ
hp : (↑z)⁻¹ • q = p
hp_one : IsProbabilityMeasure (Measure.restrict p s)
hp_eq : ∫ (x : ℝ) in s, f x ∂p = (∫ (x : ℝ) in s, f x ∂q) / ↑z
hp_int : Integrable f
hp_meas_compl : ↑↑(Measure.restrict p s) sᶜ = 0
m : ℝ
hm_mem : m ∈ s
hm : f m ≤ ∫ (a : ℝ) in s, f a ∂p
M : ℝ
hM_mem : M ∈ s
hM : ∫ (a : ℝ) in s, f a ∂p ≤ f M
⊢ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)
Theorem: existsBoundsOn_integral_measure
Proof state before:
case mk.inr.intro.intro.intro.intro
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_pos : 0 < z
p : Measure ℝ
hp : (↑z)⁻¹ • q = p
hp_one : IsProbabilityMeasure (Measure.restrict p s)
hp_eq : ∫ (x : ℝ) in s, f x ∂p = (∫ (x : ℝ) in s, f x ∂q) / ↑z
hp_int : Integrable f
hp_meas_compl : ↑↑(Measure.restrict p s) sᶜ = 0
m : ℝ
hm_mem : m ∈ s
hm : f m ≤ ∫ (a : ℝ) in s, f a ∂p
M : ℝ
hM_mem : M ∈ s
hM : ∫ (a : ℝ) in s, f a ∂p ≤ f M
⊢ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)
Tactic:
simp
Proof state after:
case mk.inr.intro.intro.intro.intro
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_pos : 0 < z
p : Measure ℝ
hp : (↑z)⁻¹ • q = p
hp_one : IsProbabilityMeasure (Measure.restrict p s)
hp_eq : ∫ (x : ℝ) in s, f x ∂p = (∫ (x : ℝ) in s, f x ∂q) / ↑z
hp_int : Integrable f
hp_meas_compl : ↑↑(Measure.restrict p s) sᶜ = 0
m : ℝ
hm_mem : m ∈ s
hm : f m ≤ ∫ (a : ℝ) in s, f a ∂p
M : ℝ
hM_mem : M ∈ s
hM : ∫ (a : ℝ) in s, f a ∂p ≤ f M
⊢ f m ≤ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ≤ f M
Theorem: existsBoundsOn_integral_measure
Proof state before:
case mk.inr.intro.intro.intro.intro
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_pos : 0 < z
p : Measure ℝ
hp : (↑z)⁻¹ • q = p
hp_one : IsProbabilityMeasure (Measure.restrict p s)
hp_eq : ∫ (x : ℝ) in s, f x ∂p = (∫ (x : ℝ) in s, f x ∂q) / ↑z
hp_int : Integrable f
hp_meas_compl : ↑↑(Measure.restrict p s) sᶜ = 0
m : ℝ
hm_mem : m ∈ s
hm : f m ≤ ∫ (a : ℝ) in s, f a ∂p
M : ℝ
hM_mem : M ∈ s
hM : ∫ (a : ℝ) in s, f a ∂p ≤ f M
⊢ f m ≤ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ≤ f M
Tactic:
apply And.intro
Proof state after:
case mk.inr.intro.intro.intro.intro.left
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_pos : 0 < z
p : Measure ℝ
hp : (↑z)⁻¹ • q = p
hp_one : IsProbabilityMeasure (Measure.restrict p s)
hp_eq : ∫ (x : ℝ) in s, f x ∂p = (∫ (x : ℝ) in s, f x ∂q) / ↑z
hp_int : Integrable f
hp_meas_compl : ↑↑(Measure.restrict p s) sᶜ = 0
m : ℝ
hm_mem : m ∈ s
hm : f m ≤ ∫ (a : ℝ) in s, f a ∂p
M : ℝ
hM_mem : M ∈ s
hM : ∫ (a : ℝ) in s, f a ∂p ≤ f M
⊢ f m ≤ (∫ (x : ℝ) in s, f x ∂q) / ↑z

case mk.inr.intro.intro.intro.intro.right
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_pos : 0 < z
p : Measure ℝ
hp : (↑z)⁻¹ • q = p
hp_one : IsProbabilityMeasure (Measure.restrict p s)
hp_eq : ∫ (x : ℝ) in s, f x ∂p = (∫ (x : ℝ) in s, f x ∂q) / ↑z
hp_int : Integrable f
hp_meas_compl : ↑↑(Measure.restrict p s) sᶜ = 0
m : ℝ
hm_mem : m ∈ s
hm : f m ≤ ∫ (a : ℝ) in s, f a ∂p
M : ℝ
hM_mem : M ∈ s
hM : ∫ (a : ℝ) in s, f a ∂p ≤ f M
⊢ (∫ (x : ℝ) in s, f x ∂q) / ↑z ≤ f M