MeasureTheory.eLpNorm_truncCompl_anti

lemma eLpNorm_truncCompl_anti (hf : eLpNorm f 1 μ ≠ ⊤) (mf : AEStronglyMeasurable f μ) :    Antitone (fun s ↦ eLpNorm (truncCompl f s) p μ) := by  intro a _b hab  have : ∀ᵐ x ∂μ, ‖f x‖ₑ ≠ ⊤ := by    rw [eLpNorm_one_eq_lintegral_enorm] at hf    simp_rw [ae_iff, not_ne_iff]; exact measure_eq_top_of_lintegral_ne_top mf.enorm hf  have : ∀ᵐ x ∂μ, ‖trunc f a x‖ₑ ≠ ⊤ := by    refine this.mono fun x hx ↦ ?_    rw [trunc]    split_ifs; exacts [hx, by simp]  exact eLpNorm_mono_enorm_ae <| this.mono fun x hx ↦ truncCompl_anti hab hx