MeasureTheory.wnorm'_le_eLpNorm'

lemma wnorm'_le_eLpNorm' (hf : AEStronglyMeasurable f μ) {p : ℝ} (p0 : 0 < p) :    wnorm' f p μ ≤ eLpNorm' f p μ := by  refine iSup_le (fun t ↦ ?_)  simp_rw [distribution, eLpNorm']  have p0' : 0 ≤ 1 / p := (div_pos one_pos p0).le  have set_eq : {x | ofNNReal t < ‖f x‖ₑ} = {x | ofNNReal t ^ p < ‖f x‖ₑ ^ p} := by    simp [ENNReal.rpow_lt_rpow_iff p0]  have : ofNNReal t = (ofNNReal t ^ p) ^ (1 / p) := by simp [p0.ne']  nth_rewrite 1 [inv_eq_one_div p, this, ← mul_rpow_of_nonneg _ _ p0', set_eq]  refine rpow_le_rpow ?_ p0'  refine le_trans ?_ <| mul_meas_ge_le_lintegral₀ (hf.enorm.pow_const p) (ofNNReal t ^ p)  gcongr  exact fun x ↦ le_of_lt x