MeasureTheory.wnorm_eq_zero_iff

lemma wnorm_eq_zero_iff [ENorm ε] {f : α → ε} {p : ℝ≥0∞} (hp : p ≠ 0) :    wnorm f p μ = 0 ↔ (fun x ↦ ‖f x‖ₑ) =ᵐ[μ] 0 := by  unfold wnorm  split_ifs with h₀  · rw [← eLpNorm_exponent_top, ← eLpNorm_enorm f]    exact eLpNormEssSup_eq_zero_iff  · refine Iff.trans ⟨?_, ?_⟩ eLpNormEssSup_eq_zero_iff <;> intro h    · have iSup_wnorm := iSup_eq_zero.mp h      by_contra h₁      have : 0 < eLpNormEssSup f μ := pos_iff_ne_zero.mpr h₁      unfold eLpNormEssSup at this      rw [essSup_eq_sInf] at this      let b := (min (sInf {a : ℝ≥0∞ | μ {x | a < ‖f x‖ₑ} = 0}) 1) / 2      have b_lt_inf : b < min (sInf {a : ℝ≥0∞ | μ {x | a < ‖f x‖ₑ} = 0}) 1 :=        ENNReal.half_lt_self (lt_min this zero_lt_one).ne'          (lt_of_le_of_lt (min_le_right _ 1) one_lt_top).ne      have meas_ne_zero : μ {x | b < ‖f x‖ₑ} ≠ 0 := by        intro h        have obs : sInf {a | μ {x | a < ‖f x‖ₑ} = 0} ≤ b := csInf_le' h        contrapose! obs        calc        _ < _ := b_lt_inf        _ ≤ _ := min_le_left ..      have b_ne_0 : b ≠ 0 := (ENNReal.half_pos (lt_min this zero_lt_one).ne').ne'      have p_toReal_inv_pos : 0 < p.toReal⁻¹ := inv_pos_of_pos (toReal_pos hp h₀)      have coe_b : ENNReal.ofNNReal b.toNNReal = b := coe_toNNReal b_lt_inf.ne_top      have : distribution f b μ = 0 := by        refine (rpow_eq_zero_iff_of_pos p_toReal_inv_pos).mp ?_        refine eq_zero_of_ne_zero_of_mul_left_eq_zero b_ne_0 ?_        rw [← coe_b]        exact iSup_wnorm b.toNNReal      exact meas_ne_zero this    · refine iSup_eq_zero.mpr fun t ↦ mul_eq_zero.mpr        (Or.inr ((rpow_eq_zero_iff_of_pos (inv_pos_of_pos (toReal_pos hp h₀))).mpr (nonpos_iff_eq_zero.mp ?_)))      calc        _ ≤ distribution f 0 μ := by gcongr; exact zero_le        _ = distribution f (eLpNormEssSup f μ) μ := by congr; exact h.symm        _ = 0 := distribution_eLpNormEssSup