two_sided_metric_carleson_hasStrongType

theorem two_sided_metric_carleson_hasStrongType  [Countable (Θ X)] (ha : 4 ≤ a) (hq : q ∈ Ioo 1 2)    (hT : ∀ r > 0, HasBoundedStrongType (czOperator K r) 2 2 volume volume (C_Ts a)) :      HasStrongType (carlesonOperator K) q q volume volume        (C_carleson_hasStrongType a q) := by  --TODO: change parameters of constant to something reasonable  set q₀ := (q + 2) / 2  set q₁ := (q + 1) / 2  set t := (interpolation_param q₀⁻¹ q₁⁻¹ q⁻¹).toNNReal  have one_eq : (1 : ℝ≥0) = 1 / 2 + 1 / 2 := by rw [← add_div]; simp  have two_eq : (2 : ℝ≥0) = 3 / 2 + 1 / 2 := by rw [← add_div]; refine NNReal.eq ?_; norm_num  have hq₀ : q₀ ∈ Ioo 1 2 := by    unfold q₀    rw [add_div]    constructor    · norm_num      exact zero_lt_one.trans hq.1    · norm_num      nth_rw 2 [← one_add_one_eq_two]      gcongr      rw [← div_self_of_invertible 2]      gcongr      exact hq.2  have hq₁ : q₁ ∈ Ioo 1 2 := by    unfold q₁    rw [add_div]    constructor    · nth_rw 1 [one_eq]      gcongr      exact hq.1    · nth_rw 3 [two_eq]      gcongr      apply hq.2.trans      norm_num  have q₀_ne_q₁ : q₀ ≠ q₁ := by    unfold q₀ q₁    rw [ne_eq, div_eq_div_iff (by norm_num) (by norm_num)]    simp  have q_pos : 0 < q := lt_trans zero_lt_one hq.1  have q₀_pos : 0 < q₀ := lt_trans zero_lt_one hq₀.1  have q₁_pos : 0 < q₁ := lt_trans zero_lt_one hq₁.1  have h : interpolation_param (↑q₀)⁻¹ (↑q₁)⁻¹ (↑q)⁻¹ ∈ Ioo 0 1 := by    apply interpolation_param_mem_Ioo    simp only [mem_Ioo]    rw [← NNReal.coe_inv, ← NNReal.coe_inv, ← NNReal.coe_inv]    rw [NNReal.coe_lt_coe, NNReal.coe_lt_coe, inv_lt_inv₀ q₀_pos q_pos, inv_lt_inv₀ q_pos q₁_pos]    constructor    · unfold q₀      rw [lt_div_iff₀ zero_lt_two, mul_two]      gcongr      exact hq.2    · unfold q₁      rw [div_lt_iff₀ zero_lt_two, mul_two]      gcongr      exact hq.1  have ht : t ∈ Ioo 0 1 := by    unfold t    simp only [mem_Ioo, Real.toNNReal_pos, Real.toNNReal_lt_one]    rwa [← mem_Ioo]  have hqq₀q₁ : q⁻¹ = (1 - t) / q₀ + t / q₁ := by    have : q⁻¹.toReal = ((1 - t) / q₀ + t / q₁).toReal := by      push_cast      rw [NNReal.coe_sub ht.2.le, Real.coe_toNNReal _ h.1.le]      exact @interpolation_param_interpolation q₀⁻¹ q₁⁻¹ q⁻¹ (by simpa)    rwa [← Real.toNNReal_eq_toNNReal_iff (by simp) (by positivity),      Real.toNNReal_coe, Real.toNNReal_coe] at this  have lorentzType_q₀ :      HasLorentzType (carlesonOperator K) q₀ 1 q₀ ⊤ volume volume (4 * (C10_0_1 a q₀) / q₀) := by    apply two_sided_metric_carleson_hasLorentzType ha hq₀ hT  have lorentzType_q₁ :      HasLorentzType (carlesonOperator K) q₁ 1 q₁ ⊤ volume volume (4 * (C10_0_1 a q₁) / q₁) := by    apply two_sided_metric_carleson_hasLorentzType ha hq₁ hT  have helper {p : ℝ≥0} (hp : 0 < p): (4 * (C10_0_1 a p) / p) = ENNReal.ofNNReal (4 * (C10_0_1 a p) / p) := by    norm_cast    rw [ENNReal.coe_div hp.ne']  rw [helper q₀_pos] at lorentzType_q₀  rw [helper q₁_pos] at lorentzType_q₁  -- use interpolation for Lorentz spaces  rename_i m kernel cf cancel count  have : IsOneSidedKernel a K := by infer_instance  set kpd : KernelProofData a K := KernelProofData.mk d ha cf this  rw [hasStrongType_iff_hasLorentzType]  unfold C_carleson_hasStrongType  convert exists_hasLorentzType_real_interpolation _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ lorentzType_q₀ lorentzType_q₁ _ _  · simp [hq₀.1.le]  · simp [hq₁.1.le]  · rfl  · rfl  · simp [hq₀.1.le]  · simp [hq₁.1.le]  · exact OrderTop.le_top 1  · exact OrderTop.le_top 1  · rw [coe_ne_coe]    exact q₀_ne_q₁  · rw [coe_ne_coe]    exact q₀_ne_q₁  · exact zero_lt_one' ℝ≥0  · exact ht  · apply div_pos _ q₀_pos    apply _root_.mul_pos    · norm_num    apply C10_0_1_pos hq₀.1  · apply div_pos _ q₁_pos    apply _root_.mul_pos    · norm_num    apply C10_0_1_pos hq₁.1  · norm_cast    rw [← ENNReal.coe_div q₁_pos.ne', ← ENNReal.coe_div q₀_pos.ne',        ← ENNReal.coe_inv q_pos.ne', ← ENNReal.coe_add]    norm_cast  · norm_cast    rw [← ENNReal.coe_div q₀_pos.ne', ← ENNReal.coe_div q₁_pos.ne', ← ENNReal.coe_inv q_pos.ne', ← ENNReal.coe_add]    norm_cast  · intro f hf    apply (carlesonOperator_measurable _).aestronglyMeasurable    apply (hf.memLp _).locallyIntegrable <;> simp [hq.1.le, q_pos]  · unfold AESubadditiveOn    intro f g hf hg    simp only [enorm_eq_self, coe_one, one_mul]    apply Filter.Eventually.of_forall    intro x    apply carlesonOperator_add_le_add_carlesonOperator    · rcases hf with hf | hf      · apply (hf.memLp _).locallyIntegrable <;> simp [hq₀.1.le]      · apply (hf.memLp _).locallyIntegrable <;> simp [hq₁.1.le]    · rcases hg with hg | hg      · apply (hg.memLp _).locallyIntegrable <;> simp [hq₀.1.le]      · apply (hg.memLp _).locallyIntegrable <;> simp [hq₁.1.le]  · simp only [coe_pos]    exact lt_trans (zero_lt_one' ℝ≥0) hq.1