MeasureTheory.eLorentzNorm'_eq_wnorm

lemma eLorentzNorm'_eq_wnorm (p_ne_top : p ≠ ∞) {f : α → ε} {μ : Measure α} :    eLorentzNorm' f p ∞ μ = wnorm f p μ := by  rw [wnorm_ne_top p_ne_top]  unfold eLorentzNorm' wnorm'  simp only [ENNReal.inv_top, ENNReal.toReal_zero, ENNReal.rpow_zero, ENNReal.toReal_inv,    eLpNorm_exponent_top, one_mul]  rw [eLpNormEssSup_withDensity (by fun_prop) (by simp)]  apply eLpNormEssSup_nnreal_eq_iSup_nnreal (f := fun t ↦ t * distribution f t μ ^ p.toReal⁻¹)  intro a x ha  apply ContinuousWithinAt.ennreal_mul continuous_id'.continuousWithinAt    ((continuousWithinAt_distribution _).ennrpow_const _)  · rw [or_iff_not_imp_left]    push Not    intro h    exfalso    rw [h] at ha    simp at ha  · right    simp