MeasureTheory.eLorentzNorm'_eq_integral_distribution_rpow

lemma eLorentzNorm'_eq_integral_distribution_rpow {_ : MeasurableSpace α} {f : α → ε}  {μ : Measure α} :    eLorentzNorm' f p 1 μ = p * ∫⁻ (t : ℝ≥0), distribution f t μ ^ p.toReal⁻¹ := by  unfold eLorentzNorm'  simp only [inv_one, ENNReal.toReal_one, ENNReal.rpow_one, ENNReal.toReal_inv]  congr  rw [eLpNorm_eq_lintegral_rpow_enorm_toReal (by norm_num) (by norm_num)]  rw [lintegral_withDensity_eq_lintegral_mul₀' (by measurability)    (by apply aeMeasurable_withDensity_inv; apply AEMeasurable.pow_const; apply AEStronglyMeasurable.enorm; apply      aestronglyMeasurable_iff_aemeasurable.mpr; apply Measurable.aemeasurable; measurability)]  simp only [enorm_eq_self, ENNReal.toReal_one, ENNReal.rpow_one, Pi.mul_apply, ne_eq, one_ne_zero,    not_false_eq_true, div_self]  rw [lintegral_nnreal_eq_lintegral_toNNReal_Ioi, lintegral_nnreal_eq_lintegral_toNNReal_Ioi]  apply setLIntegral_congr_fun measurableSet_Ioi  intro x hx  simp only  rw [← mul_assoc, ENNReal.inv_mul_cancel, one_mul]  · rw [ENNReal.coe_ne_zero]    symm    apply ne_of_lt    rw [Real.toNNReal_pos]    exact hx  · exact ENNReal.coe_ne_top