noncomputable def lcoConvergent {X : Type u_1} {a : ℕ} [MetricSpace X] (K : X → X → ℂ) [KernelProofData a K] (Q : MeasureTheory.SimpleFunc X (Θ X)) (f : X → ℂ) (n : ℕ) (x : X) : ENNReal

A monotone sequence of functions converging to linearizedCarlesonOperator.

Equations

• lcoConvergent K Q f n x = ⨆ R₁ ∈ Set.Ioo (2 ^ n)⁻¹ (2 ^ n), ⨆ R₂ ∈ Set.Ioo R₁ (2 ^ n), ‖T_R K Q R₁ R₂ (2 ^ n) f x‖ₑ

theorem monotone_lcoConvergent {X : Type u_1} {a : ℕ} [MetricSpace X] {K : X → X → ℂ} [KernelProofData a K] {Q : MeasureTheory.SimpleFunc X (Θ X)} {f : X → ℂ} : Monotone (lcoConvergent K Q f)

theorem iSup_lcoConvergent {X : Type u_1} {a : ℕ} [MetricSpace X] {K : X → X → ℂ} [KernelProofData a K] {Q : MeasureTheory.SimpleFunc X (Θ X)} {f : X → ℂ} : ⨆ (n : ℕ), lcoConvergent K Q f n = linearizedCarlesonOperator (⇑Q) K f

theorem measurable_lcoConvergent {X : Type u_1} {a : ℕ} [MetricSpace X] {K : X → X → ℂ} [KernelProofData a K] {Q : MeasureTheory.SimpleFunc X (Θ X)} {f : X → ℂ} {n : ℕ} (mf : Measurable f) (nf : (fun (x : X) => ‖f x‖) ≤ 1) : Measurable (lcoConvergent K Q f n)

theorem linearized_metric_carleson {X : Type u_1} {a : ℕ} [MetricSpace X] {q q' : NNReal} {F G : Set X} {K : X → X → ℂ} [KernelProofData a K] {Q : MeasureTheory.SimpleFunc X (Θ X)} {f : X → ℂ} [IsCancellative X (defaultτ a)] (hq : q ∈ Set.Ioc 1 2) (hqq' : q.HolderConjugate q') (mF : MeasurableSet F) (mG : MeasurableSet G) (mf : Measurable f) (nf : (fun (x : X) => ‖f x‖) ≤ F.indicator 1) (hT : ∀ (θ : Θ X), MeasureTheory.HasBoundedStrongType (fun (x1 : X → ℂ) (x2 : X) => linearizedNontangentialOperator (⇑Q) θ K x1 x2) 2 2 MeasureTheory.volume MeasureTheory.volume ↑(C_Ts a)) : ∫⁻ (x : X) in G, linearizedCarlesonOperator (⇑Q) K f x ≤ ↑(C1_0_2 a q) * MeasureTheory.volume G ^ (↑q')⁻¹ * MeasureTheory.volume F ^ (↑q)⁻¹

Theorem 1.1.2

theorem linearized_metric_carleson_check : LinearizedMetricCarleson