exact hm
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
no goals