MeasureTheory.exists_hasStrongType_real_interpolation_aux₂

lemma exists_hasStrongType_real_interpolation_aux₂ {f : α → E₁}    [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  let M := (@d _ E₁ _ p p₀ q₀ p₁ q₁ C₀ C₁ μ _ f).toReal  have q₀pos : 0 < q₀ := pos_of_rb_Ioc hp₀  have q₁pos : 0 < q₁ := pos_of_rb_Ioc hp₁  have p₀ne_top : p₀ ≠ ⊤ := ne_top_of_le_ne_top hq₀q₁.ne_top hp₀.2  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'  have p_eq_p₀ : p = p₀ := (interp_exp_eq hp₀p₁ ht hp).symm  rcases (eq_zero_or_pos (eLpNorm f p μ)) with hF | snorm_pos  · refine le_of_eq_of_le ?_ zero_le    apply exists_hasStrongType_real_interpolation_aux₀ (hp := hp) (hq := hq) <;> try assumption  · have hF : eLpNorm f p μ ∈ Ioo 0 ⊤ := ⟨snorm_pos, hf.2⟩    have M_pos : 0 < M := toReal_pos (d_pos hC₀ hC₁ hF).ne' (d_ne_top hC₀ hC₁ hF)    have coe_q : ENNReal.ofReal q.toReal = q :=    ofReal_toReal_eq_iff.mpr (interp_exp_ne_top hq₀q₁.ne ht hq)    nth_rw 1 [← coe_q]    rw [eLpNorm_eq_distribution (h₂T hf)        (interp_exp_toReal_pos ht q₀pos q₁pos hq₀q₁.ne hq)]    calc    (ENNReal.ofReal q.toReal *    ∫⁻ (t : ℝ) in Ioi 0, distribution (T f) (ENNReal.ofReal t) ν * ENNReal.ofReal (t ^ (q.toReal - 1))) ^ q.toReal⁻¹      ≤ (ENNReal.ofReal q.toReal * (        (∫⁻ (t : ℝ) in Ioo 0 M, distribution (T f) (ENNReal.ofReal t) ν * ENNReal.ofReal (t ^ (q.toReal - 1))) +        (∫⁻ (t : ℝ) in Ici M, distribution (T f) (ENNReal.ofReal t) ν * ENNReal.ofReal (t ^ (q.toReal - 1))))        ) ^ q.toReal⁻¹ := by      gcongr      rw [← Ioo_union_Ici_eq_Ioi (M_pos)]      apply lintegral_union_le _ (Ioo (0 : ℝ) (M : ℝ)) (Ici (M : ℝ))    _ ≤ (ENNReal.ofReal q.toReal *        ((∫⁻ (t : ℝ) in Ioo 0 M, C₀ ^ q₀.toReal *        eLpNorm f p μ ^ q₀.toReal * ENNReal.ofReal (t ^ (-q₀.toReal)) *        ENNReal.ofReal (t ^ (q.toReal - 1))) * (if q₀ = ⊤ then 0 else 1)+        (∫⁻ (t : ℝ) in Ici M, C₁ ^ q₁.toReal *        eLpNorm f p μ ^ q₁.toReal * ENNReal.ofReal (t ^ (-q₁.toReal)) *        ENNReal.ofReal (t ^ (q.toReal - 1))) * if q₁ = ⊤ then 0 else 1)) ^        q.toReal⁻¹ := by      apply ENNReal.rpow_le_rpow <;> try positivity      apply mul_le_mul_right      apply add_le_add      · split_ifs with is_q₀top        · contrapose! is_q₀top; exact hq₀q₁.ne_top        · rw [mul_one]          apply setLIntegral_mono' measurableSet_Ioo          intro t ⟨(ht₁ : 0 < t), _⟩          gcongr          rw [← ofReal_rpow_of_pos ht₁]          apply weaktype_estimate <;> try assumption          · exact (hq₀q₁.ne_top).lt_top          · rw [p_eq_p₀]; exact h₀T          · exact ofReal_pos.mpr ht₁      · split_ifs with is_q₁_top        · simp only [mul_zero, nonpos_iff_eq_zero]          have hf_0 : EqOn (fun t ↦ distribution (T f) (ENNReal.ofReal t) ν *              ENNReal.ofReal (t ^ (q.toReal - 1))) (fun x ↦ 0) (Ici M) := by            intro t ht            dsimp only            rw [weaktype_estimate_top] <;> try assumption            · simp            · rw [p_eq_p₀, hp₀p₁]; exact h₁T            · have p₀pos : 0 < p₀ := hp₀.1              have p₁pos : 0 < p₁ := hp₁.1              have q₀ne_top : q₀ ≠ ⊤ := hq₀q₁.ne_top              unfold M at ht              rw [d_eq_top_of_eq] at ht <;> try assumption              have : ENNReal.ofReal (C₁ * eLpNorm f p μ).toReal = C₁ * eLpNorm f p μ :=                ofReal_toReal_eq_iff.mpr (by finiteness)              rw [← this]              exact ofReal_le_ofReal ht          rw [setLIntegral_congr_fun measurableSet_Ici hf_0, lintegral_zero]        · rw [mul_one]          apply setLIntegral_mono' measurableSet_Ici          intro t ht          have ht' := lt_of_lt_of_le M_pos ht          gcongr          rw [← ofReal_rpow_of_pos ht']          apply weaktype_estimate <;> try assumption          · exact Ne.lt_top is_q₁_top          · rw [p_eq_p₀, hp₀p₁]; exact h₁T          · positivity    _ = (ENNReal.ofReal q.toReal *        ((C₀ * eLpNorm f p μ)^ q₀.toReal *        (∫⁻ (t : ℝ) in Ioo 0 M, ENNReal.ofReal (t ^ (q.toReal - q₀.toReal - 1))) *        (if q₀ = ⊤ then 0 else 1) +        ((C₁ * eLpNorm f p μ) ^ q₁.toReal *        ∫⁻ (t : ℝ) in Ici M,  ENNReal.ofReal (t ^ (q.toReal - q₁.toReal - 1))) *        if q₁ = ⊤ then 0 else 1)) ^        q.toReal⁻¹ := by      congr      · rw [← lintegral_const_mul]        · apply setLIntegral_congr_fun measurableSet_Ioo          intro t ⟨(ht₁ : 0 < t), _⟩          dsimp          rw [ENNReal.mul_rpow_of_nonneg] <;> try positivity          rw [mul_assoc, ← ofReal_mul] <;> try positivity          congr          rw [← Real.rpow_add ht₁]          congr 1; linarith        · refine Measurable.ennreal_ofReal ?_          exact Measurable.pow_const (fun ⦃t⦄ a ↦ a) (q.toReal - q₀.toReal - 1)      · rw [← lintegral_const_mul]        · apply setLIntegral_congr_fun measurableSet_Ici          intro t ht          dsimp only          have t_pos : 0 < t := lt_of_lt_of_le M_pos ht          rw [ENNReal.mul_rpow_of_nonneg] <;> try positivity          rw [mul_assoc, ← ofReal_mul] <;> try positivity          congr          rw [← Real.rpow_add] <;> try positivity          congr 1; linarith        · refine Measurable.ennreal_ofReal ?_          exact Measurable.pow_const (fun ⦃t⦄ a ↦ a) (q.toReal - q₁.toReal - 1)    _ = _ := by      apply exists_hasStrongType_real_interpolation_aux₁ <;> assumption