theorem
carlesonOperator_eq_biSup_Θ'_J102
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
{K : X → X → ℂ}
[KernelProofData a K]
{f : X → ℂ}
{x : X}
(mf : Measurable f)
(nf : (fun (x : X) => ‖f x‖) ≤ 1)
:
theorem
surjective_enumΘ'
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
{K : X → X → ℂ}
[KernelProofData a K]
(nΘ' : (Θ' X).Nonempty)
:
Function.Surjective (enumΘ' nΘ')
theorem
biSup_Θ'_eq_biSup_enumΘ'
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
{K : X → X → ℂ}
[KernelProofData a K]
(nΘ' : (Θ' X).Nonempty)
(g : Θ X → X → ENNReal)
{x : X}
:
def
enumΘ'ArgMax
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
{K : X → X → ℂ}
[KernelProofData a K]
(nΘ' : (Θ' X).Nonempty)
(g : Θ X → X → ENNReal)
(n : ℕ)
(x : X)
:
The argmax of g (enumΘ' nΘ' i) x over i ≤ n with lower indices winning ties.
Equations
- enumΘ'ArgMax nΘ' g n x = List.findIdx (fun (i : ℕ) => decide (∀ j ≤ n, g (↑(enumΘ' nΘ' j)) x ≤ g (↑(enumΘ' nΘ' i)) x)) (List.range (n + 1))
Instances For
theorem
enumΘ'ArgMax_mem_range
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
{K : X → X → ℂ}
[KernelProofData a K]
(nΘ' : (Θ' X).Nonempty)
(g : Θ X → X → ENNReal)
{n : ℕ}
{x : X}
:
theorem
enumΘ'ArgMax_eq_iff
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
{K : X → X → ℂ}
[KernelProofData a K]
(nΘ' : (Θ' X).Nonempty)
(g : Θ X → X → ENNReal)
{n i : ℕ}
{x : X}
(hi : i ≤ n)
:
The characterising property of enumΘ'ArgMax.
def
QΘ'
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
{K : X → X → ℂ}
[KernelProofData a K]
(nΘ' : (Θ' X).Nonempty)
{g : Θ X → X → ENNReal}
(mg : ∀ (θ : Θ X), Measurable (g θ))
(n : ℕ)
:
MeasureTheory.SimpleFunc X (Θ X)
The simple function corresponding to the blueprint's Q_n.
Equations
Instances For
theorem
biSup_enumΘ'_le_QΘ'
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
{K : X → X → ℂ}
[KernelProofData a K]
(nΘ' : (Θ' X).Nonempty)
{g : Θ X → X → ENNReal}
(mg : ∀ (θ : Θ X), Measurable (g θ))
{n : ℕ}
{x : X}
:
theorem
lowerSemicontinuous_LNT
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
{K : X → X → ℂ}
[KernelProofData a K]
{f : X → ℂ}
{Q : MeasureTheory.SimpleFunc X (Θ X)}
{θ : Θ X}
:
LowerSemicontinuous (linearizedNontangentialOperator (⇑Q) θ K f)
theorem
BST_LNT_of_BST_NT
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
{K : X → X → ℂ}
[KernelProofData a K]
{Q : MeasureTheory.SimpleFunc X (Θ X)}
(hT :
MeasureTheory.HasBoundedStrongType (fun (x1 : X → ℂ) (x2 : X) => nontangentialOperator K x1 x2) 2 2
MeasureTheory.volume MeasureTheory.volume ↑(C_Ts a))
(θ : Θ X)
:
MeasureTheory.HasBoundedStrongType (fun (x1 : X → ℂ) (x2 : X) => linearizedNontangentialOperator (⇑Q) θ K x1 x2) 2 2
MeasureTheory.volume MeasureTheory.volume ↑(C_Ts a)
theorem
metric_carleson
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
{q q' : NNReal}
{F G : Set X}
{K : X → X → ℂ}
[KernelProofData a K]
{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 :
MeasureTheory.HasBoundedStrongType (fun (x1 : X → ℂ) (x2 : X) => nontangentialOperator K x1 x2) 2 2
MeasureTheory.volume MeasureTheory.volume ↑(C_Ts a))
:
∫⁻ (x : X) in G, carlesonOperator K f x ≤ ↑(C1_0_2 a q) * MeasureTheory.volume G ^ (↑q')⁻¹ * MeasureTheory.volume F ^ (↑q)⁻¹
Theorem 1.1.1
theorem
metric_carleson'
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
{q q' : NNReal}
{F G : Set X}
{K : X → X → ℂ}
[KernelProofData a K]
{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 :
MeasureTheory.HasBoundedStrongType (fun (x1 : X → ℂ) (x2 : X) => nontangentialOperator K x1 x2) 2 2
MeasureTheory.volume MeasureTheory.volume ↑(C_Ts a))
: