Documentation

Carleson.Discrete.MainTheorem

Proposition 2.0.2 #

source
noncomputable def C2_0_2 (a : ℕ) (q : NNReal) :
NNReal

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

Equations
Instances For
    source
    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] :
    0 < C2_0_2 a (nnq X)
    source
    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⁻¹