MeasureTheory.distribution_lt_top

lemma distribution_lt_top (hf : MemLp f p μ) (p_pos : 0 < p) (p_ne_top : p ≠ ∞)    {t : ℝ≥0} (ht : 0 < t) :    distribution f t μ < ∞ := by  have := wnorm'_le_eLpNorm' hf.1 (toReal_pos p_pos.ne' p_ne_top)  rw [← eLpNorm_eq_eLpNorm' p_pos.ne' p_ne_top] at this  have := this.trans_lt hf.2  rw [wnorm', iSup_lt_iff] at this  rcases this with ⟨b,b_lt_top, h⟩  have := (h t).trans_lt b_lt_top  rw [mul_lt_top_iff] at this  rcases this with ⟨t_lt_top, h⟩| (t_zero| h)  · rwa [rpow_lt_top_iff_of_pos] at h    simp only [inv_pos]    exact toReal_pos p_pos.ne' p_ne_top  · rw [ENNReal.coe_eq_zero] at t_zero    exfalso    exact ht.ne' t_zero  · rw [ENNReal.rpow_eq_zero_iff_of_pos (by simp only [inv_pos]; exact toReal_pos p_pos.ne' p_ne_top)] at h    rw [h]    simp only [zero_lt_top]