Proposition 2.0.2

noncomputable def C2_0_2 (a : ℝ) (q : NNReal) : NNReal

The constant used in Proposition 2.0.2, which has value 2 ^ (440 * a ^ 3) / (q - 1) ^ 5 in the blueprint.

Equations

• C2_0_2 a q = C5_1_2 a q + C5_1_3 a q

theorem C2_0_2_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_2 (↑a) (nnq X) > 0

theorem discrete_carleson (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), 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', ↑‖carlesonSum Set.univ f x‖₊ ≤ ↑(C2_0_2 (↑a) (nnq X)) * MeasureTheory.volume G ^ (1 - q⁻¹) * MeasureTheory.volume F ^ q⁻¹