Carleson operators #
theorem
bcs_of_measurable_of_le_indicator_f
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[PseudoMetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
{f : X → ℂ}
(hf : Measurable f)
(h2f : ∀ (x : X), ‖f x‖ ≤ F.indicator 1 x)
:
theorem
bcs_of_measurable_of_le_indicator_g
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[PseudoMetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
{g : X → ℂ}
(hg : Measurable g)
(h2g : ∀ (x : X), ‖g x‖ ≤ G.indicator 1 x)
:
noncomputable def
carlesonOn
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[PseudoMetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
(p : 𝔓 X)
(f : X → ℂ)
:
X → ℂ
The operator T_𝔭 defined in Proposition 2.0.2.
Equations
Instances For
theorem
measurable_carlesonOn
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[PseudoMetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{p : 𝔓 X}
{f : X → ℂ}
(measf : Measurable f)
:
Measurable (carlesonOn p f)
noncomputable def
carlesonSum
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[PseudoMetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
(ℭ : Set (𝔓 X))
(f : X → ℂ)
(x : X)
:
The operator T_ℭ f defined at the bottom of Section 7.4.
We will use this in other places of the formalization as well.
Equations
- carlesonSum ℭ f x = ∑ p : 𝔓 X with p ∈ ℭ, carlesonOn p f x
Instances For
theorem
measurable_carlesonSum
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[PseudoMetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{ℭ : Set (𝔓 X)}
{f : X → ℂ}
(measf : Measurable f)
:
Measurable (carlesonSum ℭ f)
theorem
MeasureTheory.AEStronglyMeasurable.carlesonOn
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[PseudoMetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{p : 𝔓 X}
{f : X → ℂ}
(hf : AEStronglyMeasurable f volume)
:
theorem
MeasureTheory.AEStronglyMeasurable.carlesonSum
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[PseudoMetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{ℭ : Set (𝔓 X)}
{f : X → ℂ}
(hf : AEStronglyMeasurable f volume)
:
theorem
support_carlesonOn_subset_E
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[PseudoMetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{p : 𝔓 X}
{f : X → ℂ}
:
Function.support (carlesonOn p f) ⊆ E p
theorem
support_carlesonSum_subset
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[PseudoMetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{ℭ : Set (𝔓 X)}
{f : X → ℂ}
:
Function.support (carlesonSum ℭ f) ⊆ ⋃ p ∈ ℭ, ↑(𝓘 p)
theorem
MeasureTheory.BoundedCompactSupport.bddAbove_norm_carlesonOn
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[PseudoMetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
(p : 𝔓 X)
{f : X → ℂ}
(hf : BoundedCompactSupport f volume)
:
BddAbove (Set.range fun (x : X) => ‖_root_.carlesonOn p f x‖)
theorem
MeasureTheory.BoundedCompactSupport.carlesonOn
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[PseudoMetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{p : 𝔓 X}
{f : X → ℂ}
(hf : BoundedCompactSupport f volume)
:
theorem
MeasureTheory.BoundedCompactSupport.bddAbove_norm_carlesonSum
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[PseudoMetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{ℭ : Set (𝔓 X)}
{f : X → ℂ}
(hf : BoundedCompactSupport f volume)
:
BddAbove (Set.range fun (x : X) => ‖_root_.carlesonSum ℭ f x‖)
theorem
MeasureTheory.BoundedCompactSupport.carlesonSum
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[PseudoMetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{ℭ : Set (𝔓 X)}
{f : X → ℂ}
(hf : BoundedCompactSupport f volume)
:
theorem
sum_carlesonSum_of_pairwiseDisjoint
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[PseudoMetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{ι : Type u_2}
{f : X → ℂ}
{x : X}
{A : ι → Set (𝔓 X)}
{s : Finset ι}
(hs : (↑s).PairwiseDisjoint A)
:
Adjoint operators #
noncomputable def
adjointCarleson
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
(p : 𝔓 X)
(f : X → ℂ)
(x : X)
:
The definition of Tₚ*g(x), defined above Lemma 7.4.1
Equations
Instances For
noncomputable def
adjointCarlesonSum
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
(ℭ : Set (𝔓 X))
(f : X → ℂ)
(x : X)
:
The definition of T_ℭ*g(x), defined at the bottom of Section 7.4
Equations
- adjointCarlesonSum ℭ f x = ∑ p : 𝔓 X with p ∈ ℭ, adjointCarleson p f x
Instances For
theorem
MeasureTheory.StronglyMeasurable.adjointCarleson
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{p : 𝔓 X}
{f : X → ℂ}
(hf : StronglyMeasurable f)
:
theorem
MeasureTheory.AEStronglyMeasurable.adjointCarleson
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{p : 𝔓 X}
{f : X → ℂ}
(hf : AEStronglyMeasurable f volume)
:
theorem
MeasureTheory.StronglyMeasurable.adjointCarlesonSum
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{f : X → ℂ}
{ℭ : Set (𝔓 X)}
(hf : StronglyMeasurable f)
:
theorem
MeasureTheory.AEStronglyMeasurable.adjointCarlesonSum
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{f : X → ℂ}
{ℭ : Set (𝔓 X)}
(hf : AEStronglyMeasurable f volume)
:
theorem
MeasureTheory.BoundedCompactSupport.bddAbove_norm_adjointCarleson
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
(p : 𝔓 X)
{f : X → ℂ}
(hf : BoundedCompactSupport f volume)
:
BddAbove (Set.range fun (x : X) => ‖_root_.adjointCarleson p f x‖)
theorem
MeasureTheory.BoundedCompactSupport.adjointCarleson
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{p : 𝔓 X}
{f : X → ℂ}
(hf : BoundedCompactSupport f volume)
:
theorem
MeasureTheory.BoundedCompactSupport.bddAbove_norm_adjointCarlesonSum
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{f : X → ℂ}
{ℭ : Set (𝔓 X)}
(hf : BoundedCompactSupport f volume)
:
BddAbove (Set.range fun (x : X) => ‖_root_.adjointCarlesonSum ℭ f x‖)
theorem
MeasureTheory.BoundedCompactSupport.adjointCarlesonSum
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{f : X → ℂ}
{ℭ : Set (𝔓 X)}
(hf : BoundedCompactSupport f volume)
:
theorem
adjointCarleson_adjoint
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{f g : X → ℂ}
(hf : MeasureTheory.BoundedCompactSupport f MeasureTheory.volume)
(hg : MeasureTheory.BoundedCompactSupport g MeasureTheory.volume)
(p : 𝔓 X)
:
∫ (x : X), (starRingEnd ℂ) (g x) * carlesonOn p f x = ∫ (y : X), (starRingEnd ℂ) (adjointCarleson p g y) * f y
adjointCarleson is the adjoint of carlesonOn.
theorem
adjointCarlesonSum_adjoint
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{f g : X → ℂ}
(hf : MeasureTheory.BoundedCompactSupport f MeasureTheory.volume)
(hg : MeasureTheory.BoundedCompactSupport g MeasureTheory.volume)
(ℭ : Set (𝔓 X))
:
∫ (x : X), (starRingEnd ℂ) (g x) * carlesonSum ℭ f x = ∫ (x : X), (starRingEnd ℂ) (adjointCarlesonSum ℭ g x) * f x
adjointCarlesonSum is the adjoint of carlesonSum.
theorem
integrable_adjointCarlesonSum
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
(s : Set (𝔓 X))
{f : X → ℂ}
(hf : MeasureTheory.BoundedCompactSupport f MeasureTheory.volume)
:
MeasureTheory.Integrable (fun (x : X) => adjointCarlesonSum s f x) MeasureTheory.volume