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)
:
A monotone sequence of functions converging to linearizedCarlesonOperator.
Equations
Instances For
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 → ℂ}
:
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