two_sided_metric_carleson_hasRestrictedWeakType

theorem two_sided_metric_carleson_hasRestrictedWeakType [Countable (Θ X)] (ha : 4 ≤ a) (hq : q ∈ Ioc 1 2)  (hqq' : q.HolderConjugate q')  (hT : ∀ r > 0, HasBoundedStrongType (czOperator K r) 2 2 volume volume (C_Ts a)) :      HasRestrictedWeakType (carlesonOperator K) q q' volume volume (C10_0_1 a q) := by  unfold HasRestrictedWeakType  intro F G hF F_finite hG G_finite  constructor  · 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 (carlesonOperator_measurable _).aestronglyMeasurable    apply (locallyIntegrable_const _).indicator hF  rw [eLpNorm_one_eq_lintegral_enorm, mul_assoc, mul_comm (volume _ ^ _), ← mul_assoc]  simp_rw [enorm_eq_self]  simp only [toReal_inv, coe_toReal]  apply two_sided_metric_carleson ha hq hqq' hF hG hT  · exact (measurable_indicator_const_iff 1).mpr hF  · intro x    unfold indicator    split_ifs <;> simp