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
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