MeasureTheory.trunc_Lp_Lq_higher

lemma trunc_Lp_Lq_higher (hpq : p ∈ Ioc 0 q) {f : α → ε} (hf : MemLp f p μ) (ht : t ≠ ∞) :    MemLp (trnc ⊤ f t) q μ := by  refine ⟨aestronglyMeasurable_trnc hf.1, ?_⟩  rcases (eq_or_ne q ⊤) with q_eq_top | q_ne_top  · rw [q_eq_top, eLpNorm_exponent_top]    simp only [trnc]    calc _      _ ≤ max 0 t := trunc_eLpNormEssSup_le t      _ < ∞ := by finiteness  · have p_ne_top := ne_top_of_le_ne_top q_ne_top hpq.2    rw [← rpow_lt_top_iff_of_pos (toReal_pos (hpq.1.trans_le hpq.2).ne' q_ne_top)]    apply lt_of_le_of_lt (estimate_eLpNorm_trunc q_ne_top hpq hf.1)    apply mul_lt_top ?_ ?_    · by_cases ht'' : t = 0      · rw [ht'']        apply ENNReal.rpow_lt_top_of_nonneg (h := by finiteness)        simp only [sub_nonneg]        rw [toReal_le_toReal p_ne_top q_ne_top]        exact hpq.2      · finiteness    · exact (rpow_lt_top_iff_of_pos (toReal_pos hpq.1.ne' p_ne_top)).mpr hf.2