MeasureTheory.exists_hasStrongType_real_interpolation_aux₄

lemma exists_hasStrongType_real_interpolation_aux₄ {p₀ p₁ q₀ q₁ p q : ℝ≥0∞} {A : ℝ≥0} (hA : 0 < A)    [TopologicalSpace E₁] [ESeminormedAddMonoid E₁]    [TopologicalSpace E₂] [ContinuousENorm E₂]    (hp₀ : p₀ ∈ Ioc 0 q₀) (hp₁ : p₁ ∈ Ioc 0 q₁) (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₁)    (hT : SubadditiveTrunc T A f ν) (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 ν ≤    (if p₀ = p₁ then 1 else ENNReal.ofReal (2 * A)) * q ^ q⁻¹.toReal *    (((if q₁ < ⊤ then 1 else 0) * ENNReal.ofReal |q.toReal - q₁.toReal|⁻¹ +    (if q₀ < ⊤ then 1 else 0) * ENNReal.ofReal |q.toReal - q₀.toReal|⁻¹)) ^ q⁻¹.toReal *    C₀ ^ (1 - t).toReal * C₁ ^ t.toReal * eLpNorm f p μ := by  let M := if p₀ = p₁ then 1 else ENNReal.ofReal (2 * A)  have hM : M = if p₀ = p₁ then 1 else ENNReal.ofReal (2 * A) := rfl  rw [← hM]  split_ifs at hM with are_ps_eq  · rw [hM, one_mul]    have p_eq_p₀ : p = p₀ := (interp_exp_eq are_ps_eq ht hp).symm    calc    _ ≤ 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      apply exists_hasStrongType_real_interpolation_aux₃ <;> try assumption    _ = _ := by      rw [p_eq_p₀]      congr 4      · rw [toReal_inv]      · rw [add_comm]        congr 2        · rw [mul_comm]          have : (q₁ < ⊤) ↔ (q₁ ≠ ⊤):= lt_top_iff_ne_top          split_ifs <;> tauto        · rw [mul_comm]          have : (q₀ < ⊤) ↔ (q₀ ≠ ⊤):= lt_top_iff_ne_top          split_ifs <;> tauto        · rw [toReal_inv]  · rcases (lt_or_gt_of_ne are_ps_eq) with p₀lt_p₁ | p₁lt_p₀    · rw [hM]      apply exists_hasStrongType_real_interpolation_aux <;> try assumption    · have (a b c d e f : ℝ≥0∞) : a * b * c * d * e * f = a * b * c * e * d * f := by ring      rw [hM, 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)          (hq₀q₁ := hq₀q₁.symm) <;> assumption