linearized_metric_carleson

theorem linearized_metric_carleson [IsCancellative X (defaultτ a)]    (hq : q ∈ Ioc 1 2) (hqq' : q.HolderConjugate q') (mF : MeasurableSet F) (mG : MeasurableSet G)    (mf : Measurable f) (nf : (‖f ·‖) ≤ F.indicator 1)    (hT : ∀ θ : Θ X, HasBoundedStrongType (linearizedNontangentialOperator Q θ K · ·)      2 2 volume volume (C_Ts a)) :    ∫⁻ x in G, linearizedCarlesonOperator Q K f x ≤    C1_0_2 a q * volume G ^ (q' : ℝ)⁻¹ * volume F ^ (q : ℝ)⁻¹ := by  have nf' : (‖f ·‖) ≤ 1 := nf.trans (indicator_le_self' (by simp))  calc    _ = ∫⁻ x, ⨆ n, G.indicator (lcoConvergent K Q f n) x := by      rw [← lintegral_indicator mG]; congr! 2 with x      rw [← iSup_apply, iSup_indicator rfl monotone_lcoConvergent monotone_const, iUnion_const,        iSup_lcoConvergent]    _ = ⨆ n, ∫⁻ x, G.indicator (lcoConvergent K Q f n) x :=      lintegral_iSup (fun _ ↦ (measurable_lcoConvergent mf nf').indicator mG)        (fun _ _ hl ↦ indicator_mono (monotone_lcoConvergent hl))    _ ≤ _ := by      refine iSup_le fun n ↦ ?_      unfold lcoConvergent; rw [lintegral_indicator mG]      exact R_truncation hq hqq' mF mG mf nf rfl hT