α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
⊢ (∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ) =
    ENNReal.ofReal p * ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (t ^ (p - 1))
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
p : ℝ
p_pos : 0 < p
⊢ (∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ) =
    ENNReal.ofReal p * ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (t ^ (p - 1))
have one_lt_p : -1 < p - 1 := by linarith
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
obs : ∀ (x : ℝ), (∫ (t : ℝ) in 0 ..x, t ^ (p - 1)) = x ^ p / p
⊢ (∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ) =
    ENNReal.ofReal p * ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (t ^ (p - 1))
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
⊢ (∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ) =
    ENNReal.ofReal p * ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (t ^ (p - 1))
have obs : ∀ x : ℝ, (∫ t : ℝ in (0)..x, t ^ (p - 1)) = x ^ p / p := by
  intro x
  rw [integral_rpow (Or.inl one_lt_p)]
  simp [Real.zero_rpow p_pos.ne.symm]
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g✝ : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : ℝ → ℝ := fun t => t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
⊢ (∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ) =
    ENNReal.ofReal p * ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (t ^ (p - 1))
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
obs : ∀ (x : ℝ), (∫ (t : ℝ) in 0 ..x, t ^ (p - 1)) = x ^ p / p
⊢ (∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ) =
    ENNReal.ofReal p * ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (t ^ (p - 1))
set g := fun t : ℝ => t ^ (p - 1)
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g✝ : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : ℝ → ℝ := fun t => t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
⊢ (∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ) =
    ENNReal.ofReal p * ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (t ^ (p - 1))
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g✝ : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : ℝ → ℝ := fun t => t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
⊢ (∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ) =
    ENNReal.ofReal p * ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (t ^ (p - 1))
have g_nn : ∀ᵐ t ∂volume.restrict (Ioi (0 : ℝ)), 0 ≤ g t := by
  filter_upwards [self_mem_ae_restrict (measurableSet_Ioi : MeasurableSet (Ioi (0 : ℝ)))]
  intro t t_pos
  exact Real.rpow_nonneg_of_nonneg (mem_Ioi.mp t_pos).le (p - 1)
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g✝ : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : ℝ → ℝ := fun t => t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
⊢ (∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ) =
    ENNReal.ofReal p * ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (t ^ (p - 1))
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g✝ : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : ℝ → ℝ := fun t => t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
⊢ (∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ) =
    ENNReal.ofReal p * ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (t ^ (p - 1))
have g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t := fun _ _ =>
  intervalIntegral.intervalIntegrable_rpow' one_lt_p
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g✝ : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : ℝ → ℝ := fun t => t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
key :
  (∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ) =
    ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)
⊢ (∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ) =
    ENNReal.ofReal p * ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (t ^ (p - 1))
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g✝ : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : ℝ → ℝ := fun t => t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
⊢ (∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ) =
    ENNReal.ofReal p * ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (t ^ (p - 1))
have key := lintegral_comp_eq_lintegral_meas_le_mul μ f_nn f_mble g_intble g_nn
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g✝ : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : ℝ → ℝ := fun t => t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
key :
  (∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ) =
    ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)
⊢ (∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ) = ∫⁻ (a : α), ENNReal.ofReal p * ENNReal.ofReal (f a ^ p / p) ∂μ

α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g✝ : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : ℝ → ℝ := fun t => t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
key :
  (∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ) =
    ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)
⊢ Measurable fun ω => ENNReal.ofReal (f ω ^ p / p)
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g✝ : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : ℝ → ℝ := fun t => t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
key :
  (∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ) =
    ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)
⊢ (∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ) =
    ENNReal.ofReal p * ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (t ^ (p - 1))
rw [← key, ← lintegral_const_mul (ENNReal.ofReal p)] <;> simp_rw [obs]
no goals
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
p : ℝ
p_pos : 0 < p
⊢ -1 < p - 1
linarith
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
x : ℝ
⊢ (∫ (t : ℝ) in 0 ..x, t ^ (p - 1)) = x ^ p / p
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
⊢ ∀ (x : ℝ), (∫ (t : ℝ) in 0 ..x, t ^ (p - 1)) = x ^ p / p
intro x
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
x : ℝ
⊢ (x ^ (p - 1 + 1) - 0 ^ (p - 1 + 1)) / (p - 1 + 1) = x ^ p / p
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
x : ℝ
⊢ (∫ (t : ℝ) in 0 ..x, t ^ (p - 1)) = x ^ p / p
rw [integral_rpow (Or.inl one_lt_p)]
no goals
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
x : ℝ
⊢ (x ^ (p - 1 + 1) - 0 ^ (p - 1 + 1)) / (p - 1 + 1) = x ^ p / p
simp [Real.zero_rpow p_pos.ne.symm]
case h
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g✝ : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : ℝ → ℝ := fun t => t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
⊢ ∀ (a : ℝ), a ∈ Ioi 0 → 0 ≤ a ^ (p - 1)
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g✝ : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : ℝ → ℝ := fun t => t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
⊢ ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
filter_upwards [self_mem_ae_restrict (measurableSet_Ioi : MeasurableSet (Ioi (0 : ℝ)))]
case h
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g✝ : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : ℝ → ℝ := fun t => t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
t : ℝ
t_pos : t ∈ Ioi 0
⊢ 0 ≤ t ^ (p - 1)
case h
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g✝ : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : ℝ → ℝ := fun t => t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
⊢ ∀ (a : ℝ), a ∈ Ioi 0 → 0 ≤ a ^ (p - 1)
intro t t_pos
no goals
case h
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g✝ : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : ℝ → ℝ := fun t => t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
t : ℝ
t_pos : t ∈ Ioi 0
⊢ 0 ≤ t ^ (p - 1)
exact Real.rpow_nonneg_of_nonneg (mem_Ioi.mp t_pos).le (p - 1)
case e_f.h
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g✝ : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : ℝ → ℝ := fun t => t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
key :
  (∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ) =
    ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)
ω : α
⊢ ENNReal.ofReal (f ω ^ p) = ENNReal.ofReal p * ENNReal.ofReal (f ω ^ p / p)
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g✝ : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : ℝ → ℝ := fun t => t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
key :
  (∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ) =
    ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)
⊢ (∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ) = ∫⁻ (a : α), ENNReal.ofReal p * ENNReal.ofReal (f a ^ p / p) ∂μ
congr with ω
no goals
case e_f.h
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g✝ : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : ℝ → ℝ := fun t => t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
key :
  (∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ) =
    ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)
ω : α
⊢ ENNReal.ofReal (f ω ^ p) = ENNReal.ofReal p * ENNReal.ofReal (f ω ^ p / p)
rw [← ENNReal.ofReal_mul p_pos.le, mul_div_cancel' (f ω ^ p) p_pos.ne.symm]
no goals
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g✝ : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : ℝ → ℝ := fun t => t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
key :
  (∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ) =
    ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)
⊢ Measurable fun ω => ENNReal.ofReal (f ω ^ p / p)
exact ((f_mble.pow measurable_const).div_const p).ennreal_ofReal