MeasureTheory.exists_hasStrongType_real_interpolation

theorem exists_hasStrongType_real_interpolation {p₀ p₁ q₀ q₁ p q : ℝ≥0∞}    [TopologicalSpace E₁] [ESeminormedAddMonoid E₁]    [TopologicalSpace E₂] [ContinuousENorm E₂]    (hp₀ : p₀ ∈ Ioc 0 q₀) (hp₁ : p₁ ∈ Ioc 0 q₁) (hq₀q₁ : q₀ ≠ q₁)    {C₀ C₁ A : ℝ≥0} (hA : 1 ≤ A) (ht : t ∈ Ioo 0 1) (hC₀ : 0 < C₀) (hC₁ : 0 < C₁)    (hp : p⁻¹ = (1 - t) / p₀ + t / p₁) (hq : q⁻¹ = (1 - t) / q₀ + t / q₁)    (hmT : ∀ f, MemLp f p μ → AEStronglyMeasurable (T f) ν)    (hT : AESubadditiveOn T (fun f ↦ MemLp f p₀ μ ∨ MemLp f p₁ μ) A ν)    (h₀T : HasWeakType T p₀ q₀ μ ν C₀) (h₁T : HasWeakType T p₁ q₁ μ ν C₁) :    HasStrongType T p q μ ν (C_realInterpolation p₀ p₁ q₀ q₁ q C₀ C₁ A t) := by  intro f hf  refine ⟨hmT f hf, ?_⟩  have hp' : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹ := by rw [hp]; congr  have hq' : q⁻¹ = (1 - t) * q₀⁻¹ + t * q₁⁻¹ := by rw [hq]; congr  have obs : SubadditiveTrunc T A f ν :=    Subadditive_trunc_from_SubadditiveOn_Lp₀p₁ hp₀.1 hp₁.1 hA ht hp' hT hf  rw [coe_C_realInterpolation hp₀ hp₁ hq₀q₁] <;> try assumption  have : 0 < A := lt_of_lt_of_le (by norm_num) hA  apply exists_hasStrongType_real_interpolation_aux₄ <;> assumption