MeasureTheory.Subadditive_trunc_from_SubadditiveOn_Lp₀p₁

lemma Subadditive_trunc_from_SubadditiveOn_Lp₀p₁ {p₀ p₁ p : ℝ≥0∞}    [TopologicalSpace E₁] [ESeminormedAddMonoid E₁]    [TopologicalSpace E₂] [ContinuousENorm E₂]    (hp₀ : 0 < p₀) (hp₁ : 0 < p₁)    {A : ℝ≥0} (hA : 1 ≤ A) (ht : t ∈ Ioo 0 1)    (hp : p⁻¹ = (1 - t) / p₀ + t / p₁)    (hT : AESubadditiveOn T (fun f ↦ MemLp f p₀ μ ∨ MemLp f p₁ μ) A ν)    (hf : MemLp f p μ) :    SubadditiveTrunc T A f ν := by  intro a a_pos  by_cases ha : a = ∞  · rw [ha]    simp only [trunc_top, truncCompl_top]    filter_upwards with x    nth_rw 1 [← one_mul ‖T (f + fun x ↦ 0) x‖ₑ]    gcongr    · exact one_le_coe_iff.mpr hA    · apply le_trans (add_zero _).symm.le      gcongr      · apply le_of_eq        congr        · ext x; simp      · simp  apply hT  · rcases lt_trichotomy p₀ p₁ with p₀lt_p₁ | (p₀eq_p₁ | p₁lt_p₀)    · refine Or.inr (trunc_Lp_Lq_higher (p := p) ?_ hf ha)      exact ⟨interpolated_pos' hp₀ hp₁ (ne_top_of_Ioo ht) hp, (interp_exp_between hp₀ hp₁ p₀lt_p₁ ht hp).2.le⟩    · exact Or.inl <| interp_exp_eq p₀eq_p₁ ht hp ▸ hf.trunc    · refine Or.inl (trunc_Lp_Lq_higher (p := p) ?_ hf ha)      exact ⟨interpolated_pos' hp₀ hp₁ (ne_top_of_Ioo ht) hp,        (interp_exp_between hp₁ hp₀ p₁lt_p₀ (mem_sub_Ioo one_ne_top ht)          (switch_exponents ht hp)).2.le⟩  · rcases lt_trichotomy p₀ p₁ with p₀lt_p₁ | (p₀eq_p₁ | p₁lt_p₀)    · refine Or.inl (truncCompl_Lp_Lq_lower (p := p) (interp_exp_ne_top p₀lt_p₁.ne ht hp)        ⟨hp₀, (interp_exp_between hp₀ hp₁ p₀lt_p₁ ht hp).1.le⟩ a_pos hf)    · exact Or.inl <| interp_exp_eq p₀eq_p₁ ht hp ▸ hf.truncCompl    · refine Or.inr <| truncCompl_Lp_Lq_lower (p := p) ?_ ?_ a_pos hf      · exact interp_exp_ne_top p₁lt_p₀.ne (mem_sub_Ioo one_ne_top ht) (switch_exponents ht hp)      · exact ⟨hp₁, (interp_exp_between hp₁ hp₀ p₁lt_p₀ (mem_sub_Ioo one_ne_top ht)          (switch_exponents ht hp)).1.le⟩