MeasureTheory.MemWLp.ae_ne_top

@[aesop (rule_sets := [finiteness]) unsafe apply]theorem MemWLp.ae_ne_top [TopologicalSpace ε] (hf : MemWLp f p μ) : ∀ᵐ x ∂μ, ‖f x‖ₑ ≠ ∞ := by  by_cases hp_inf : p = ∞  · rw [hp_inf] at hf    simp_rw [← lt_top_iff_ne_top]    exact ae_lt_of_essSup_lt hf.2  by_cases hp_zero : p = 0  · exact (MemWLp_zero <| hp_zero ▸ hf).elim  set A := {x | ‖f x‖ₑ = ∞} with hA  simp only [MemWLp, wnorm, wnorm', hp_inf] at hf  rw [Filter.eventually_iff, mem_ae_iff]  simp only [ne_eq, compl_def, mem_setOf_eq, Decidable.not_not, ← hA]  have hp_toReal_zero := toReal_ne_zero.mpr ⟨hp_zero, hp_inf⟩  have h1 (t : ℝ≥0) : μ A ≤ distribution f t μ := by    refine μ.mono ?_    simp_all only [setOf_subset_setOf, coe_lt_top, implies_true, A]  set C := ⨆ t : ℝ≥0, t * distribution f t μ ^ p.toReal⁻¹  by_cases hC_zero : C = 0  · simp only [ENNReal.iSup_eq_zero, mul_eq_zero, ENNReal.rpow_eq_zero_iff, inv_neg'', C] at hC_zero    specialize hC_zero 1    simp only [one_ne_zero, ENNReal.coe_one, toReal_nonneg.not_gt, and_false, or_false,      false_or] at hC_zero    exact measure_mono_null (setOf_subset_setOf.mpr fun x hx => hx ▸ one_lt_top) hC_zero.1  by_contra h  have h2 : C < ∞ := by aesop  have h3 (t : ℝ≥0) : distribution f t μ ≤ (C / t) ^ p.toReal := by    rw [← rpow_inv_rpow hp_toReal_zero (distribution ..)]    refine rpow_le_rpow ?_ toReal_nonneg    rw [ENNReal.le_div_iff_mul_le (Or.inr hC_zero) (Or.inl coe_ne_top), mul_comm]    exact le_iSup_iff.mpr fun _ a ↦ a t  have h4 (t : ℝ≥0) : μ A ≤ (C / t) ^ p.toReal := (h1 t).trans (h3 t)  have h5 : μ A ≤ μ A / 2 := by    convert h4 (C * (2 / μ A) ^ p.toReal⁻¹).toNNReal    rw [coe_toNNReal (by finiteness)]    nth_rw 1 [← mul_one C]    rw [ENNReal.mul_div_mul_left _ _ hC_zero h2.ne_top, div_rpow_of_nonneg _ _ toReal_nonneg,      ENNReal.rpow_inv_rpow hp_toReal_zero, ENNReal.one_rpow, one_div,        ENNReal.inv_div (Or.inr ofNat_ne_top) (Or.inr (NeZero.ne' 2).symm)]  have h6 : μ A = 0 := by    convert (fun hh ↦ ENNReal.half_lt_self hh (ne_top_of_le_ne_top      (rpow_ne_top_of_nonneg toReal_nonneg ((div_one C).symm ▸ h2.ne_top))      (h4 1))).mt h5.not_gt    tauto  exact h h6