MeasureTheory.exists_hasStrongType_real_interpolation_aux₃

lemma exists_hasStrongType_real_interpolation_aux₃ {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₁) (hp₀p₁ : p₀ = p₁) (hq₀q₁ : q₀ ≠ q₁)    {C₀ C₁ : ℝ≥0} (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₁)    (h₀T : HasWeakType T p₀ q₀ μ ν C₀) (h₁T : HasWeakType T p₁ q₁ μ ν C₁)    (h₂T : PreservesAEStrongMeasurability (μ := μ) (ν := ν) T p)    (hf : MemLp f p μ) :    eLpNorm (T f) q ν ≤    q ^ q.toReal⁻¹ * (ENNReal.ofReal |q.toReal - q₀.toReal|⁻¹ * (if q₀ = ⊤ then 0 else 1) +      ENNReal.ofReal |q.toReal - q₁.toReal|⁻¹ * (if q₁ = ⊤ then 0 else 1)) ^ q.toReal⁻¹ *    ↑C₀ ^ ((1 - t).toReal) * ↑C₁ ^ t.toReal * eLpNorm f p μ := by  rcases lt_or_gt_of_ne hq₀q₁ with q₀lt_q₁ | q₁lt_q₀  · apply exists_hasStrongType_real_interpolation_aux₂ <;> assumption  · have (a b c d : ℝ≥0∞) : a * b * c * d = a * c * b * d := by ring    rw [this, add_comm]    have hp' := switch_exponents ht hp    have hq' := switch_exponents ht hq    nth_rw 1 [← one_sub_one_sub_eq ht]    apply exists_hasStrongType_real_interpolation_aux₂ (ht := mem_sub_Ioo one_ne_top ht)        (hp₀p₁ := hp₀p₁.symm) (hq₀q₁ := q₁lt_q₀) <;> assumption