MeasureTheory.eLpNorm_truncCompl_le

lemma eLpNorm_truncCompl_le {q : ℝ≥0∞}    (q_ne_zero : ¬ q = 0) (q_ne_top : q ≠ ⊤) :    eLpNorm (truncCompl f t) q μ ^ q.toReal ≤    ∫⁻ x : α in {x | t < ‖f x‖ₑ}, ‖f x‖ₑ ^ q.toReal ∂μ := by  unfold eLpNorm eLpNorm'  have q_toReal_pos : 0 < q.toReal := toReal_pos q_ne_zero q_ne_top  split_ifs  calc  _ = ∫⁻ x : α in {x | t < ‖f x‖ₑ}, ‖(truncCompl f t) x‖ₑ ^ q.toReal ∂μ := by    rw [one_div, ENNReal.rpow_inv_rpow]    · apply (setLIntegral_eq_of_support_subset _).symm      unfold Function.support      intro x      rw [truncCompl_eq, mem_setOf_eq]      dsimp only [Pi.sub_apply]      split_ifs with is_a_lt_fx      · exact fun _ ↦ is_a_lt_fx      · contrapose; intro _; simpa [enorm_eq_nnnorm]    · exact q_toReal_pos.ne'  _ ≤ ∫⁻ x : α in {x | t < ‖f x‖ₑ}, ‖f x‖ₑ ^ q.toReal ∂μ := by    gcongr with x    exact trnc_le_func (j := ⊥)