internlm/Lean-Github huggingface dataset:
Theorem: existsBoundsOn_integral_measure
Proof state before:
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
Tactic:
. rw [hp_eq] at hm
  exact hm
Proof state after:
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
Theorem: existsBoundsOn_integral_measure
Proof state before:
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
Tactic:
. rw [hp_eq] at hM
  exact hM
Proof state after:
no goals
Theorem: existsBoundsOn_integral_measure
Proof state before:
case hp_one
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
⊢ IsProbabilityMeasure (Measure.restrict p s)
Tactic:
constructor
Proof state after:
case hp_one.measure_univ
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
⊢ ↑↑(Measure.restrict p s) Set.univ = 1
Theorem: existsBoundsOn_integral_measure
Proof state before:
case hp_one.measure_univ
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
⊢ ↑↑(Measure.restrict p s) Set.univ = 1
Tactic:
rw [← hp]
Proof state after:
case hp_one.measure_univ
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
⊢ ↑↑(Measure.restrict ((↑z)⁻¹ • q) s) Set.univ = 1
Theorem: existsBoundsOn_integral_measure
Proof state before:
case hp_one.measure_univ
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
⊢ ↑↑(Measure.restrict ((↑z)⁻¹ • q) s) Set.univ = 1
Tactic:
simp
Proof state after:
case hp_one.measure_univ
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
⊢ (↑z)⁻¹ * ↑↑q s = 1
Theorem: existsBoundsOn_integral_measure
Proof state before:
case hp_one.measure_univ
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
⊢ (↑z)⁻¹ * ↑↑q s = 1
Tactic:
rw [hz']
Proof state after:
case hp_one.measure_univ
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
⊢ (↑z)⁻¹ * ↑z = 1
Theorem: existsBoundsOn_integral_measure
Proof state before:
case hp_one.measure_univ
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
⊢ (↑z)⁻¹ * ↑z = 1
Tactic:
rw [← ENNReal.div_eq_inv_mul]
Proof state after:
case hp_one.measure_univ
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
⊢ ↑z / ↑z = 1
Theorem: existsBoundsOn_integral_measure
Proof state before:
case hp_one.measure_univ
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
⊢ ↑z / ↑z = 1
Tactic:
rw [ENNReal.div_eq_one_iff]
Proof state after:
case hp_one.measure_univ.hb₀
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
⊢ ↑z ≠ 0

case hp_one.measure_univ.hb₁
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
⊢ ↑z ≠ ⊤
Theorem: existsBoundsOn_integral_measure
Proof state before:
case hp_one.measure_univ.hb₀
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
⊢ ↑z ≠ 0

case hp_one.measure_univ.hb₁
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
⊢ ↑z ≠ ⊤
Tactic:
. simp; exact hz_pos.ne'
Proof state after:
case hp_one.measure_univ.hb₁
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
⊢ ↑z ≠ ⊤
Theorem: existsBoundsOn_integral_measure
Proof state before:
case hp_one.measure_univ.hb₁
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
⊢ ↑z ≠ ⊤
Tactic:
. simp
Proof state after:
no goals
Theorem: existsBoundsOn_integral_measure
Proof state before:
case hp_one.measure_univ.hb₀
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
⊢ ↑z ≠ 0
Tactic:
simp
Proof state after:
case hp_one.measure_univ.hb₀
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
⊢ ¬z = 0
Theorem: existsBoundsOn_integral_measure
Proof state before:
case hp_one.measure_univ.hb₀
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
⊢ ¬z = 0
Tactic:
exact hz_pos.ne'
Proof state after:
no goals
Theorem: existsBoundsOn_integral_measure
Proof state before:
case hp_one.measure_univ.hb₁
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
⊢ ↑z ≠ ⊤
Tactic:
simp
Proof state after:
no goals
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
Tactic:
rw [← hp]
Proof state after:
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 ∂(↑z)⁻¹ • q = (∫ (x : ℝ) in s, f x ∂q) / ↑z
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 ∂(↑z)⁻¹ • q = (∫ (x : ℝ) in s, f x ∂q) / ↑z
Tactic:
simp
Proof state after:
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)
⊢ ENNReal.toReal (↑z)⁻¹ * ∫ (x : ℝ) in s, f x ∂q = (∫ (x : ℝ) in s, f x ∂q) / ↑z
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)
⊢ ENNReal.toReal (↑z)⁻¹ * ∫ (x : ℝ) in s, f x ∂q = (∫ (x : ℝ) in s, f x ∂q) / ↑z
Tactic:
simp [ENNReal.toReal_inv]
Proof state after:
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)
⊢ (↑z)⁻¹ * ∫ (x : ℝ) in s, f x ∂q = (∫ (x : ℝ) in s, f x ∂q) / ↑z
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)
⊢ (↑z)⁻¹ * ∫ (x : ℝ) in s, f x ∂q = (∫ (x : ℝ) in s, f x ∂q) / ↑z
Tactic:
rw [inv_mul_eq_div]
Proof state after:
no goals
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
Tactic:
apply Integrable.smul_measure h_int
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
⊢ (↑z)⁻¹ ≠ ⊤
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
⊢ (↑z)⁻¹ ≠ ⊤
Tactic:
simp
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
⊢ ¬z = 0
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
⊢ ¬z = 0
Tactic:
apply hz_pos.ne'
Proof state after:
no goals
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
Tactic:
rw [Measure.restrict_apply (MeasurableSet.compl hs_meas)]
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
⊢ ↑↑p (sᶜ ∩ s) = 0
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
⊢ ↑↑p (sᶜ ∩ s) = 0
Tactic:
simp
Proof state after:
no goals
Theorem: existsBoundsOn_integral_measure
Proof state before:
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
Tactic:
rw [hp_eq] at hm
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 ≤ (∫ (x : ℝ) in s, f x ∂q) / ↑z
M : ℝ
hM_mem : M ∈ s
hM : ∫ (a : ℝ) in s, f a ∂p ≤ f M
⊢ f m ≤ (∫ (x : ℝ) in s, f x ∂q) / ↑z
Theorem: existsBoundsOn_integral_measure
Proof state before:
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 ≤ (∫ (x : ℝ) in s, f x ∂q) / ↑z
M : ℝ
hM_mem : M ∈ s
hM : ∫ (a : ℝ) in s, f a ∂p ≤ f M
⊢ f m ≤ (∫ (x : ℝ) in s, f x ∂q) / ↑z
Tactic:
exact hm
Proof state after:
no goals
Theorem: existsBoundsOn_integral_measure
Proof state before:
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
Tactic:
rw [hp_eq] at hM
Proof state after:
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 : (∫ (x : ℝ) in s, f x ∂q) / ↑z ≤ f M
⊢ (∫ (x : ℝ) in s, f x ∂q) / ↑z ≤ f M
Theorem: existsBoundsOn_integral_measure
Proof state before:
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 : (∫ (x : ℝ) in s, f x ∂q) / ↑z ≤ f M
⊢ (∫ (x : ℝ) in s, f x ∂q) / ↑z ≤ f M
Tactic:
exact hM
Proof state after:
no goals
Theorem: existsBoundsOn_integral_mul_nonneg
Proof state before:
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x * g x ∂μ) / ∫ (x : ℝ) in s, g x ∂μ ∈ Set.Icc (f m) (f M)
Tactic:
have h_ae_eq : (fun x => f x * g x) =ᵐ[μ.restrict s] (fun x => ‖g x‖₊ • f x)
Proof state after:
case h_ae_eq
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
⊢ (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x

f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x * g x ∂μ) / ∫ (x : ℝ) in s, g x ∂μ ∈ Set.Icc (f m) (f M)
Theorem: existsBoundsOn_integral_mul_nonneg
Proof state before:
case h_ae_eq
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
⊢ (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x

f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x * g x ∂μ) / ∫ (x : ℝ) in s, g x ∂μ ∈ Set.Icc (f m) (f M)
Tactic:
. simp [NNReal.smul_def]
  apply Filter.Eventually.mp hg_nonneg
  simp
  apply Filter.eventually_of_forall
  intro x hx
  rw [mul_comm]
  rw [abs_eq_self.mpr hx]
Proof state after:
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x * g x ∂μ) / ∫ (x : ℝ) in s, g x ∂μ ∈ Set.Icc (f m) (f M)
Theorem: existsBoundsOn_integral_mul_nonneg
Proof state before:
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x * g x ∂μ) / ∫ (x : ℝ) in s, g x ∂μ ∈ Set.Icc (f m) (f M)
Tactic:
generalize hq : μ.withDensity (fun x => ‖g x‖₊) = q
Proof state after:
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x * g x ∂μ) / ∫ (x : ℝ) in s, g x ∂μ ∈ Set.Icc (f m) (f M)