theorem integrable_tile_sum_operator {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ σ₂ F G] {f : X → ℂ} (hf : Measurable f) (h2f : ∀ (x : X), ‖f x‖ ≤ F.indicator 1 x) {x : X} {s : ℤ} : MeasureTheory.Integrable (fun (y : X) => Ks s x y * f y * Complex.exp (Complex.I * (↑((Q x) y) - ↑((Q x) x)))) MeasureTheory.volume

theorem exists_Grid {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)] {x : X} (hx : x ∈ G) {s : ℤ} (hs : s ∈ (Set.Icc (σ₁ x) (σ₂ x)).toFinset) : ∃ (I : Grid X), GridStructure.s I = s ∧ x ∈ I

theorem tile_sum_operator {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)] {G' : Set X} {f : X → ℂ} {x : X} (hx : x ∈ G \ G') : ∑ p : 𝔓 X, carlesonOn p f x = ∑ s ∈ (Set.Icc (σ₁ x) (σ₂ x)).toFinset, ∫ (y : X), Ks s x y * f y * Complex.exp (Complex.I * (↑((Q x) y) - ↑((Q x) x)))

Lemma 4.0.3

noncomputable def C2_0_1 (a : ℕ) (q : NNReal) : NNReal

The constant used in Proposition 2.0.1. Has value 2 ^ (442 * a ^ 3) / (q - 1) ^ 5 in the blueprint.

Equations

• C2_0_1 a q = C2_0_2 a q

theorem C2_0_1_pos {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)] : C2_0_1 a (nnq X) > 0

theorem finitary_carleson (X : Type u_1) {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ σ₂ F G] : ∃ (G' : Set X), MeasurableSet G' ∧ 2 * MeasureTheory.volume G' ≤ MeasureTheory.volume G ∧ ∀ (f : X → ℂ), Measurable f → (∀ (x : X), ‖f x‖ ≤ F.indicator 1 x) → ∫⁻ (x : X) in G \ G', ‖∑ s ∈ (Set.Icc (σ₁ x) (σ₂ x)).toFinset, ∫ (y : X), Ks s x y * f y * Complex.exp (Complex.I * ↑((Q x) y))‖ₑ ≤ ↑(C2_0_1 a (nnq X)) * MeasureTheory.volume G ^ (1 - q⁻¹) * MeasureTheory.volume F ^ q⁻¹

Proposition 2.0.1