MeasureTheory.memLp_of_memLp_le_of_memLp_ge

lemma memLp_of_memLp_le_of_memLp_ge {f : α → ε} [ContinuousAdd ε]    {r : ℝ≥0∞} (hp : 0 < p) (hr' : q ∈ Icc p r)    (hf : MemLp f p μ) (hf' : MemLp f r μ) : MemLp f q μ := by  by_cases p_ne_top : p = ⊤  · rw [p_ne_top] at hf    convert hf    rw [eq_top_iff]    convert hr'.1    exact p_ne_top.symm  set C := (1 : ℝ≥0∞)  have h : MemLp (trnc ⊤ f C) q μ := trunc_Lp_Lq_higher ⟨hp, hr'.1⟩ hf (by norm_num)  have h' : MemLp (trnc ⊥ f C) q μ := by    by_cases hr : r = ⊤    · exact memLp_truncCompl_of_memLp_top (hr ▸ hf') <| distribution_lt_top hf hp p_ne_top (by norm_num)    exact truncCompl_Lp_Lq_lower hr ⟨hp.trans_le hr'.1, hr'.2⟩ (by norm_num) hf'  have : f = (trnc ⊤ f C) + (trnc ⊥ f C) := trunc_add_truncCompl.symm  rw [this]  exact h.add h'