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) : MeasureTheory.BoundedCompactSupport f MeasureTheory.volume

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) : MeasureTheory.BoundedCompactSupport g MeasureTheory.volume

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

• carlesonOn p f = (E p).indicator fun (x : X) => ∫ (y : X), Complex.exp (Complex.I * (↑((Q x) y) - ↑((Q x) x))) * Ks (𝔰 p) x y * f y

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

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) : AEStronglyMeasurable (_root_.carlesonOn p 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) : AEStronglyMeasurable (_root_.carlesonSum ℭ f) volume

theorem carlesonOn_def' {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 → ℂ) : carlesonOn p f = (E p).indicator fun (x : X) => ∫ (y : X), Ks (𝔰 p) x y * f y * Complex.exp (Complex.I * (↑((Q x) y) - ↑((Q x) x)))

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) : BoundedCompactSupport (_root_.carlesonOn p 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) : BoundedCompactSupport (_root_.carlesonSum ℭ f) volume

theorem carlesonSum_inter_add_inter_compl {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)] {f : X → ℂ} {x : X} (A B : Set (𝔓 X)) : carlesonSum (A ∩ B) f x + carlesonSum (A ∩ Bᶜ) f x = carlesonSum A f x

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) : ∑ i ∈ s, carlesonSum (A i) f x = carlesonSum (⋃ i ∈ s, A i) f x

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

• adjointCarleson p f x = ∫ (y : X) in E p, (starRingEnd ℂ) (Ks (𝔰 p) y x) * Complex.exp (Complex.I * (↑((Q y) y) - ↑((Q y) x))) * f y

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

theorem adjointCarlesonSum_inter {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)] {A B : Set (𝔓 X)} {f : X → ℂ} {x : X} : adjointCarlesonSum (A ∩ B) f x = adjointCarlesonSum A f x - adjointCarlesonSum (A \ B) f x

A helper lemma used in Lemma 7.5.10.

theorem adjoint_eq_adjoint_indicator {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 p' : 𝔓 X} {f : X → ℂ} (h : E p ⊆ ↑(𝓘 p')) : adjointCarleson p f = adjointCarleson p ((↑(𝓘 p')).indicator f)

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) : StronglyMeasurable (_root_.adjointCarleson p 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) : AEStronglyMeasurable (_root_.adjointCarleson p 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) : StronglyMeasurable (_root_.adjointCarlesonSum ℭ 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) : AEStronglyMeasurable (_root_.adjointCarlesonSum ℭ 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) : BoundedCompactSupport (_root_.adjointCarleson p 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) : BoundedCompactSupport (_root_.adjointCarlesonSum ℭ 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