MeasureTheory.eLorentzNorm_eq_eLpNorm

lemma eLorentzNorm_eq_eLpNorm {f : α → ε} (hf : AEStronglyMeasurable f μ) :  eLorentzNorm f p p μ = eLpNorm f p μ := by  by_cases p_zero : p = 0  · simp [p_zero]  by_cases p_eq_top : p = ∞  · simp [p_eq_top]  have p_eq : p = .ofReal p.toReal := by simp [p_eq_top]  simp only [eLorentzNorm, eLorentzNorm', p_zero, ↓reduceIte, p_eq_top]  calc _    _ = (ENNReal.ofReal p.toReal  * ∫⁻ t in Set.Ioi (0 : ℝ), distribution f (.ofReal t) μ *      ENNReal.ofReal t ^ (p.toReal - 1) ) ^ p⁻¹.toReal := by        rw [← p_eq, eLpNorm_eq_eLpNorm' p_zero p_eq_top, eLpNorm'_eq_lintegral_enorm,          ENNReal.mul_rpow_of_nonneg, lintegral_withDensity_eq_lintegral_mul_non_measurable]        · simp only [ENNReal.toReal_inv, enorm_eq_self, one_div]          congr 2          simp only [Pi.mul_apply]          rw [lintegral_nnreal_eq_lintegral_Ioi_ofReal            (f := fun x ↦ x⁻¹ * (x * distribution f x μ ^ p.toReal⁻¹)^ p.toReal)]          apply setLIntegral_congr_fun measurableSet_Ioi          intro t ht          simp only          rw [ENNReal.mul_rpow_of_nonneg _ _ (by simp), ← mul_assoc, ← ENNReal.rpow_neg_one,              ← ENNReal.rpow_add _ _ (by simpa) (by simp), mul_comm]          congr 2          · rw [← ENNReal.rpow_mul, inv_mul_cancel₀ (ENNReal.toReal_ne_zero.mpr ⟨p_zero, p_eq_top⟩),              ENNReal.rpow_one]          · exact neg_add_eq_sub 1 p.toReal        · exact Measurable.inv measurable_coe_nnreal_ennreal        · rw[Filter.eventually_iff_exists_mem]          use {x | x ≠ 0}          constructor          · simp [mem_ae_iff]          · intro x hx            rw [ENNReal.inv_lt_top, ENNReal.coe_pos]            exact pos_of_ne_zero hx        · simp    _ = (ENNReal.ofReal p.toReal  * ∫⁻ t in Set.Ioi (0 : ℝ), distribution f (.ofReal t) μ *      ENNReal.ofReal (t ^ (p.toReal - 1)) ) ^ p.toReal⁻¹ := by        rw [ENNReal.toReal_inv]        congr 2        apply setLIntegral_congr_fun measurableSet_Ioi        intro t ht        simp [ENNReal.ofReal_rpow_of_pos ht]    _ = eLpNorm f (.ofReal p.toReal) μ := (eLpNorm_eq_distribution hf (ENNReal.toReal_pos p_zero p_eq_top)).symm    _ = eLpNorm f p μ := by congr; exact p_eq.symm