two_sided_metric_carleson_hasLorentzType

theorem two_sided_metric_carleson_hasLorentzType [Countable (Θ X)] (ha : 4 ≤ a)  (hq : q ∈ Ioo 1 2)  (hT : ∀ r > 0, HasBoundedStrongType (czOperator K r) 2 2 volume volume (C_Ts a)) :    HasLorentzType (carlesonOperator K) q 1 q ⊤ volume volume (4 * (C10_0_1 a q) / q) := by  have hqq' := NNReal.HolderConjugate.conjExponent hq.1  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  apply (two_sided_metric_carleson_hasRestrictedWeakType ha (mem_Ioc_of_Ioo hq) hqq' hT).hasLorentzType    (by simpa) (by simp) (by simp) (C10_0_1_pos hq.1)  · intro f hf    apply (carlesonOperator_measurable _).aestronglyMeasurable    apply (hf.memLp _).locallyIntegrable <;> simp [hq.1.le]  · intro f g hf hg    filter_upwards with x    apply carlesonOperator_add_le_add_carlesonOperator    · apply (hf.memLp _).locallyIntegrable <;> simp [hq.1.le]    · apply (hg.memLp _).locallyIntegrable <;> simp [hq.1.le]  · intro a f    filter_upwards with x    rw [carlesonOperator_const_smul']    exact le_of_eq rfl  · intro f fs hf h_meas h_norm_monotone h_lim G    have hf : LocallyIntegrable f volume := by      apply (hf.memLp _).locallyIntegrable <;> simp [hq.1.le]    have bound {n : ℕ} : ∀ᵐ (a : X), ‖fs n a‖ ≤ ‖f a‖ := by      filter_upwards with x using (h_norm_monotone x).ge_of_tendsto (h_lim x).norm _    calc _      _ ≤ eLpNorm (fun x ↦ Filter.liminf (fun n ↦ carlesonOperator K (fs n) x) Filter.atTop) 1 (volume.restrict G) := by        apply eLpNorm_mono_enorm        intro x        apply carlesonOperator_le_liminf_carlesonOperator_of_tendsto (norm ∘ f)          (Filter.Eventually.of_forall h_meas) _ hf.norm (Filter.Eventually.of_forall h_lim)        filter_upwards; simpa      _ ≤ Filter.liminf (fun n ↦ eLpNorm (carlesonOperator K (fs n)) 1 (volume.restrict G)) Filter.atTop := by        rw [eLpNorm_one_eq_lintegral_enorm]        simp_rw [eLpNorm_one_eq_lintegral_enorm, enorm_eq_self]        apply lintegral_liminf_le        intro n        exact carlesonOperator_measurable (hf.mono (h_meas _) bound)    exact Filter.liminf_le_limsup  · simp  · intro f g hfg    filter_upwards with x    rw [carlesonOperator_congr_ae hfg]