MeasureTheory.exists_hasStrongType_real_interpolation_aux₁

lemma exists_hasStrongType_real_interpolation_aux₁ {f : α → E₁}    [TopologicalSpace E₁] [ESeminormedAddMonoid 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₁)    (hF : eLpNorm f p μ ∈ Ioo 0 ⊤) :    (ENNReal.ofReal q.toReal *        ((C₀ * eLpNorm f p μ)^ q₀.toReal *        (∫⁻ (t : ℝ) in Ioo 0 (@d _ E₁ _ p p₀ q₀ p₁ q₁ C₀ C₁ μ _ f).toReal,        ENNReal.ofReal (t ^ (q.toReal - q₀.toReal - 1))) * (if q₀ = ⊤ then 0 else 1) +        ((C₁ * eLpNorm f p μ) ^ q₁.toReal *        ∫⁻ (t : ℝ) in Ici (@d _ E₁ _ p p₀ q₀ p₁ q₁ C₀ C₁ μ _ f).toReal,        ENNReal.ofReal (t ^ (q.toReal - q₁.toReal - 1))) * if q₁ = ⊤ then 0 else 1)) ^        q.toReal⁻¹ =    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    let M := @d _ E₁ _ p p₀ q₀ p₁ q₁ C₀ C₁ μ _ f    have hq₀q₁' : q₀ ≠ q₁ := hq₀q₁.ne    have q₀pos : 0 < q₀ := pos_of_rb_Ioc hp₀    have q₁pos : 0 < q₁ := pos_of_rb_Ioc hp₁    have q₀lt_q_toReal : q₀.toReal < q.toReal :=      preservation_inequality_of_lt₀ ht q₀pos q₁pos hq hq₀q₁    have q_toReal_ne_zero : q.toReal ≠ 0 :=      (interp_exp_toReal_pos' ht q₀pos q₁pos hq (Or.inl hq₀q₁.ne_top)).ne'    -- lemma below proves the same, but for M.toReal    have M_pos : 0 < M := by      apply d_pos <;> assumption    have M_ne_top : M ≠ ∞ := by finiteness    have : 0 < M.toReal := toReal_pos M_pos.ne' M_ne_top    have : ENNReal.ofReal M.toReal = M := by rw [ofReal_toReal M_ne_top]    have coe_q : ENNReal.ofReal q.toReal = q :=      ofReal_toReal_eq_iff.mpr (interp_exp_ne_top hq₀q₁.ne ht hq)    -- type mismatches, ℝ vs ℝ≥0∞    have eq :        (ENNReal.ofReal q.toReal *        ((((↑C₀ * eLpNorm f p μ) ^ q₀.toReal * ∫⁻ (t : ℝ) in Ioo 0 M.toReal,            ENNReal.ofReal (t ^ (q.toReal - q₀.toReal - 1))) *            if q₀ = ⊤ then 0 else 1) +          ((↑C₁ * eLpNorm f p μ) ^ q₁.toReal * ∫⁻ (t : ℝ) in Ici M.toReal,            ENNReal.ofReal (t ^ (q.toReal - q₁.toReal - 1))) *            if q₁ = ⊤ then 0 else 1)) ^        q.toReal⁻¹ = (ENNReal.ofReal q.toReal *            (↑C₀ ^ ((1 - t).toReal * q.toReal) * ↑C₁ ^ (t.toReal * q.toReal) * eLpNorm f p μ ^ q.toReal *              ENNReal.ofReal |q.toReal - q₀.toReal|⁻¹ * (if q₀ = ⊤ then 0 else 1) +            ↑C₀ ^ ((1 - t).toReal * q.toReal) * ↑C₁ ^ (t.toReal * q.toReal) * eLpNorm f p μ ^ q.toReal *                ENNReal.ofReal |q.toReal - q₁.toReal|⁻¹ * if q₁ = ⊤ then 0 else 1)) ^            q.toReal⁻¹ := by      congr 3      · rw [lintegral_rpow_of_gt_abs, sub_add_cancel, ENNReal.ofReal_div_of_pos,            div_eq_mul_inv, ← ofReal_inv_of_pos, ← ENNReal.ofReal_rpow_of_pos] <;> try positivity        rw [← mul_assoc, simplify_factor₄ (ht := ht) (hC₁ := hC₁) (hq₀' := hq₀q₁.ne_top)]            <;> try assumption        · linarith      · split_ifs with is_q₁top        · rw [mul_zero, mul_zero]        · have q_lt_q₁toReal : q.toReal < q₁.toReal :=            preservation_inequality_of_lt₁ ht q₀pos q₁pos hq hq₀q₁ is_q₁top          rw [mul_one, mul_one, setLIntegral_congr (Filter.EventuallyEq.symm Ioi_ae_eq_Ici),          lintegral_Ioi_rpow_of_lt_abs, sub_add_cancel, ENNReal.ofReal_div_of_pos,            div_eq_mul_inv, ← ofReal_inv_of_pos, ← ENNReal.ofReal_rpow_of_pos] <;> try positivity          rw [← mul_assoc, simplify_factor₅ (hC₀ := hC₀) (ht := ht) (q₀ := q₀) (q₁ := q₁) (p₀ := p₀)              (p₁ := p₁)] <;> try assumption          · rw [abs_of_neg] <;> linarith          · rw [abs_of_neg] <;> linarith          · linarith    rw [eq, coe_q]    nth_rw 1 [mul_assoc]    nth_rw 3 [mul_assoc]    rw [← mul_add]    have obs : q.toReal⁻¹ ≥ 0 := by positivity    repeat rw [ENNReal.mul_rpow_of_nonneg _ _ obs]    rw [ENNReal.rpow_rpow_inv, ← ENNReal.rpow_mul, ← ENNReal.rpow_mul, mul_assoc (1 - t).toReal,        mul_inv_cancel₀, mul_assoc t.toReal, mul_inv_cancel₀, mul_one, mul_one] <;> try positivity    ring