MeasureTheory.ae_eq_zero_of_eLorentzNorm'_eq_zero

theorem ae_eq_zero_of_eLorentzNorm'_eq_zero {f : α → ε} (p_ne_zero : p ≠ 0) (p_ne_top : p ≠ ⊤)  (q_ne_zero : q ≠ 0) (h : eLorentzNorm' f p q μ = 0) :    f =ᵐ[μ] 0 := by  rw [eLorentzNorm', mul_eq_zero, eLpNorm_eq_zero_iff (by fun_prop) q_ne_zero] at h  contrapose! h  constructor  · simp [p_ne_zero]  rw [withDensity_ae_eq (by fun_prop) (by simp)]  simp_rw [← Measure.measure_support_eq_zero_iff]  simp only [ENNReal.toReal_inv, Function.support_mul, Function.support_ofNNReal]  rw [Function.support_rpow_of_pos (by rw [inv_pos]; apply ENNReal.toReal_pos p_ne_zero p_ne_top)]  have : (fun (x : ℝ≥0) ↦ distribution f x μ) = (fun x ↦ distribution f x μ) ∘ ENNReal.ofNNReal := by    ext x    simp  rw [this, Function.support_comp_eq_preimage, support_distribution, ENNReal.ofNNReal_preimage,      Set.sdiff_singleton_eq_self (by simp), ENNReal.toNNReal_Iio]  split_ifs with h'  · simp only [Set.inter_univ, ne_eq]    rw [NNReal.volume_Ioi]    simp  · rw [Set.Ioi_inter_Iio, NNReal.volume_Ioo]    simp only [ENNReal.coe_zero, tsub_zero, ENNReal.coe_eq_zero, ne_eq]    rw [ENNReal.toNNReal_eq_zero_iff]    simp only [eLpNormEssSup_eq_zero_iff, not_or]    use h