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. Has value 2 ^ (442 * a ^ 3) / (q - 1) ^ 5 in the blueprint.

Equations
Instances For
    source
    theorem le_C2_0_2 {a : β„•} (ha : 4 ≀ a) {q : NNReal} (hq : q ∈ Set.Ioc 1 2) :
    C5_1_2 a q + C5_1_3 a q ≀ C2_0_2 a q
    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⁻¹