Theorem: existsBoundsOn_integral_measure (ForML/IntegralMeanValue.lean)

State before:
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_fin : IsFiniteMeasure (Measure.restrict q s)
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ENNReal.toReal (↑↑q s) ∈ Set.Icc (f m) (f M)
Tactic:
rw [ENNReal.toReal]
State after:
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_fin : IsFiniteMeasure (Measure.restrict q s)
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑(ENNReal.toNNReal (↑↑q s)) ∈ Set.Icc (f m) (f M)

State before:
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_fin : IsFiniteMeasure (Measure.restrict q s)
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑(ENNReal.toNNReal (↑↑q s)) ∈ Set.Icc (f m) (f M)
Tactic:
generalize hz : ENNReal.toNNReal (q s) = z
State after:
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_fin : IsFiniteMeasure (Measure.restrict q s)
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)

State before:
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_fin : IsFiniteMeasure (Measure.restrict q s)
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)
Tactic:
rcases hq_fin with ⟨hq_fin⟩
State after:
case mk
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 : ↑↑(Measure.restrict q s) Set.univ < ⊤
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)

State before:
case mk
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 : ↑↑(Measure.restrict q s) Set.univ < ⊤
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)
Tactic:
simp at hq_fin
State after:
case mk
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 < ⊤
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)

State before:
case mk
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 < ⊤
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)
Tactic:
have hz' : q s = z
State after:
case hz'
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 < ⊤
⊢ ↑↑q s = ↑z

case mk
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
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)

State before:
case hz'
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 < ⊤
⊢ ↑↑q s = ↑z

case mk
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
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)
Tactic:
. rw [← hz]
  rw [ENNReal.coe_toNNReal hq_fin.ne]
State after:
case mk
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
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)

State before:
case mk
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
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)
Tactic:
cases eq_or_gt_of_le (zero_le z) with
| inl hz_zero =>
  exfalso
  rw [hz_zero] at hz
  rw [ENNReal.toNNReal_eq_zero_iff] at hz
  cases hz with
  | inl _ => contradiction
  | inr h => exact ne_of_lt hq_fin h
| inr hz_pos =>
  generalize hp : (z : ENNReal)⁻¹ • q = p
  have hp_one : IsProbabilityMeasure (p.restrict s)
  . constructor
    rw [← hp]
    simp
    rw [hz']
    rw [← ENNReal.div_eq_inv_mul]
    rw [ENNReal.div_eq_one_iff]
    . simp; exact hz_pos.ne'
    . simp
  have hp_eq : ∫ x in s, f x ∂p = (∫ x in s, f x ∂q) / (z : ℝ)
  . rw [← hp]
    simp
    simp [ENNReal.toReal_inv]
    rw [inv_mul_eq_div]
  have hp_int : Integrable f (p.restrict s)
  . rw [← hp]
    simp  apply Integrable.smul_measure h_int
    simp
    apply hz_pos.ne'
  have hp_meas_compl : p.restrict s sᶜ = 0
  . rw [Measure.restrict_apply (MeasurableSet.compl hs_meas)]
    simp
  have h_lb := @exists_not_mem_null_le_integral _ _ _ _ _ hp_one hp_int hp_meas_compl
  have h_ub := @exists_not_mem_null_integral_le _ _ _ _ _ hp_one hp_int hp_meas_compl
  simp at h_lb
  simp at h_ub
  rcases h_lb with ⟨m, ⟨hm_mem, hm⟩⟩
  rcases h_ub with ⟨M, ⟨hM_mem, hM⟩⟩
  exists m
  exists M
  apply And.intro ⟨hm_mem, hM_mem⟩
  simp
  apply And.intro
  . rw [hp_eq] at hm
    exact hm
  . rw [hp_eq] at hM
    exact hM
State after:
no goals

State before:
case hz'
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 < ⊤
⊢ ↑↑q s = ↑z
Tactic:
rw [← hz]
State after:
case hz'
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 < ⊤
⊢ ↑↑q s = ↑(ENNReal.toNNReal (↑↑q s))

State before:
case hz'
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 < ⊤
⊢ ↑↑q s = ↑(ENNReal.toNNReal (↑↑q s))
Tactic:
rw [ENNReal.coe_toNNReal hq_fin.ne]
State after:
no goals

State before:
case mk.inl
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_zero : z = 0
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)
Tactic:
exfalso
State after:
case mk.inl
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_zero : z = 0
⊢ False

State before:
case mk.inl
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_zero : z = 0
⊢ False
Tactic:
rw [hz_zero] at hz
State after:
case mk.inl
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) = 0
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_zero : z = 0
⊢ False

State before:
case mk.inl
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) = 0
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_zero : z = 0
⊢ False
Tactic:
rw [ENNReal.toNNReal_eq_zero_iff] at hz
State after:
case mk.inl
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ↑↑q s = 0 ∨ ↑↑q s = ⊤
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_zero : z = 0
⊢ False

State before:
case mk.inl
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ↑↑q s = 0 ∨ ↑↑q s = ⊤
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_zero : z = 0
⊢ False
Tactic:
cases hz with
| inl _ => contradiction
| inr h => exact ne_of_lt hq_fin h
State after:
no goals

State before:
case mk.inl.inl
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_zero : z = 0
h✝ : ↑↑q s = 0
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
case mk.inl.inr
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_zero : z = 0
h : ↑↑q s = ⊤
⊢ False
Tactic:
exact ne_of_lt hq_fin h
State after:
no goals

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
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)
Tactic:
generalize hp : (z : ENNReal)⁻¹ • q = p
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
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)

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
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)
Tactic:
have hp_one : IsProbabilityMeasure (p.restrict s)
State after:
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)

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)
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)

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)

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)
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)
Tactic:
. constructor
  rw [← hp]
  simp
  rw [hz']
  rw [← ENNReal.div_eq_inv_mul]
  rw [ENNReal.div_eq_one_iff]
  . simp; exact hz_pos.ne'
  . simp
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)
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)

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)
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)
Tactic:
have hp_eq : ∫ x in s, f x ∂p = (∫ x in s, f x ∂q) / (z : ℝ)
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 ∂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)

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]
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)

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)
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)

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'
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)

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
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)

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
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)

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
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)

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
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)

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
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)

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
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)

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⟩⟩
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)

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⟩⟩
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)

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
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)

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
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)

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⟩
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)

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
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

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
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

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
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

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
State after:
no goals

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
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

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]
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

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
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

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']
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

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]
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

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]
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 ≠ ⊤

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'
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 ≠ ⊤

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
State after:
no goals

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
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

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'
State after:
no goals

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
State after:
no goals

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]
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

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
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

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]
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

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]
State after:
no goals

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
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)⁻¹ ≠ ⊤

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
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

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'
State after:
no goals

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)]
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

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
State after:
no goals

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
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

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
State after:
no goals

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
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

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
State after:
no goals