Documentation

Carleson.Discrete.ExceptionalSet

source
noncomputable def C5_2_9 (X : Type u_1) [MetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] (n : β„•) :
NNReal

The constant in Lemma 5.2.9, with value D ^ (1 - ΞΊ * Z * (n + 1))

Equations
Instances For
    source
    theorem third_exception_rearrangement {X : Type u_1} [MetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] :
    (βˆ‘' (n : β„•) (k : β„•), if k ≀ n then βˆ‘' (j : β„•), ↑(C5_2_9 X n) * 2 ^ (9 * ↑a - ↑j) * 2 ^ (n + k + 3) * MeasureTheory.volume G else 0) = βˆ‘' (k : β„•), 2 ^ (9 * a + 4 + 2 * k) * ↑(defaultD a) ^ (1 - defaultΞΊ a * ↑(defaultZ a) * (↑k + 1)) * MeasureTheory.volume G * βˆ‘' (n : β„•), if k ≀ n then (2 * ↑(defaultD a) ^ (-defaultΞΊ a * ↑(defaultZ a))) ^ (↑n - ↑k) else 0

    A rearrangement for Lemma 5.2.9 that does not require the tile structure.

    Section 5.2 and Lemma 5.1.1 #

    source
    theorem first_exception' {X : Type u_1} [MetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] :
    MeasureTheory.volume G₁ ≀ 2 ^ (-5) * MeasureTheory.volume G

    Lemma 5.2.1

    source
    theorem first_exception {X : Type u_1} [MetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] :
    MeasureTheory.volume G₁ ≀ 2 ^ (-4) * MeasureTheory.volume G
    source
    theorem dense_cover {X : Type u_1} [MetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (k : β„•) :
    MeasureTheory.volume (⋃ i ∈ 𝓒 k, ↑i) ≀ 2 ^ (k + 1) * MeasureTheory.volume G

    Lemma 5.2.2

    source
    theorem pairwiseDisjoint_E1 {X : Type u_1} [MetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {k n : β„•} :
    (𝔐 k n).PairwiseDisjoint E₁

    Lemma 5.2.3

    source
    theorem dyadic_union {X : Type u_1} [MetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {k n l : β„•} {x : X} (hx : x ∈ setA l k n) :
    βˆƒ (i : Grid X), x ∈ i ∧ ↑i βŠ† setA l k n

    Lemma 5.2.4

    source
    theorem iUnion_MsetA_eq_setA {X : Type u_1} [MetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {k n l : β„•} :
    ⋃ i ∈ MsetA l k n, ↑i = setA l k n
    source
    theorem john_nirenberg_aux1 {X : Type u_1} [MetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {k n l : β„•} {x : X} {L : Grid X} (mL : L ∈ Grid.maxCubes (MsetA l k n)) (mx : x ∈ setA (l + 1) k n) (mxβ‚‚ : x ∈ L) :
    2 ^ (n + 1) ≀ stackSize {q_1 : 𝔓 X | q_1 ∈ 𝔐 k n ∧ π“˜ q_1 ≀ L} x

    Equation (5.2.7) in the proof of Lemma 5.2.5.

    source
    theorem john_nirenberg_aux2 {X : Type u_1} [MetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {k n l : β„•} {L : Grid X} (mL : L ∈ Grid.maxCubes (MsetA l k n)) :
    2 * MeasureTheory.volume (setA (l + 1) k n ∩ ↑L) ≀ MeasureTheory.volume ↑L

    Equation (5.2.11) in the proof of Lemma 5.2.5.

    source
    theorem john_nirenberg {X : Type u_1} [MetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {k n l : β„•} :
    MeasureTheory.volume (setA l k n) ≀ 2 ^ (↑k + 1 - ↑l) * MeasureTheory.volume G

    Lemma 5.2.5

    source
    theorem second_exception {X : Type u_1} [MetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] :
    MeasureTheory.volume Gβ‚‚ ≀ 2 ^ (-2) * MeasureTheory.volume G

    Lemma 5.2.6

    source
    def layervol {X : Type u_1} [MetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (k n : β„•) (t : ℝ) :
    ENNReal

    The volume of a "layer" in the key function of Lemma 5.2.7.

    Equations
    Instances For
      source
      theorem indicator_sum_eq_natCast {X : Type u_1} [MetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {x : X} {s : Finset (𝔓 X)} :
      βˆ‘ m ∈ s, (↑(π“˜ m)).indicator 1 x = ↑(βˆ‘ m ∈ s, (↑(π“˜ m)).indicator 1 x)
      source
      theorem layervol_eq_zero_of_lt {X : Type u_1} [MetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {k n : β„•} {t : ℝ} (ht : ↑(𝔐 k n).toFinset.card < t) :
      layervol k n t = 0
      source
      theorem lintegral_Ioc_layervol_one {X : Type u_1} [MetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {k n l : β„•} :
      ∫⁻ (t : ℝ) in Set.Ioc (↑l) (↑l + 1), layervol k n t = layervol k n (↑l + 1)
      source
      theorem antitone_layervol {X : Type u_1} [MetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {k n : β„•} :
      Antitone fun (t : ℝ) => layervol k n t
      source
      theorem lintegral_Ioc_layervol_le {X : Type u_1} [MetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {k n a✝ b : β„•} :
      ∫⁻ (t : ℝ) in Set.Ioc ↑a✝ ↑b, layervol k n t ≀ ↑(b - a✝) * layervol k n (↑a✝ + 1)
      source
      theorem top_tiles_aux {X : Type u_1} [MetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {k n : β„•} :
      βˆ‘ m : 𝔓 X with m ∈ 𝔐 k n, MeasureTheory.volume ↑(π“˜ m) = ∫⁻ (t : ℝ) in Set.Ioc 0 (↑(𝔐 k n).toFinset.card * 2 ^ (n + 1)), layervol k n t
      source
      theorem top_tiles {X : Type u_1} [MetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {k n : β„•} :
      βˆ‘ m : 𝔓 X with m ∈ 𝔐 k n, MeasureTheory.volume ↑(π“˜ m) ≀ 2 ^ (n + k + 3) * MeasureTheory.volume G

      Lemma 5.2.7

      Definition of function π”˜(m) used in the proof of Lemma 5.2.8, and some properties of π”˜(m)

      source
      noncomputable def π”˜ {X : Type u_1} [MetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (k n j : β„•) (x : X) (m : 𝔓 X) :
      Finset (𝔓 X)

      The function π”˜(m) used in the proof of Lemma 5.2.8

      Equations
      Instances For
        source
        theorem tree_count {X : Type u_1} [MetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {k n j : β„•} {x : X} :
        ↑(stackSize (π”˜β‚ k n j) x) ≀ 2 ^ (9 * ↑a - ↑j) * ↑(stackSize (𝔐 k n) x)

        Lemma 5.2.8

        source
        theorem boundary_exception {X : Type u_1} [MetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {u : 𝔓 X} :
        MeasureTheory.volume (⋃ i ∈ 𝓛 n u, ↑i) ≀ ↑(C5_2_9 X n) * MeasureTheory.volume ↑(π“˜ u)

        Lemma 5.2.9

        source
        theorem third_exception_aux {X : Type u_1} [MetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {k n j : β„•} :
        MeasureTheory.volume (⋃ p ∈ 𝔏₄ k n j, ↑(π“˜ p)) ≀ ↑(C5_2_9 X n) * 2 ^ (9 * ↑a - ↑j) * 2 ^ (n + k + 3) * MeasureTheory.volume G
        source
        theorem third_exception {X : Type u_1} [MetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] :
        MeasureTheory.volume G₃ ≀ 2 ^ (-4) * MeasureTheory.volume G

        Lemma 5.2.10

        source
        theorem exceptional_set {X : Type u_1} [MetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] :
        MeasureTheory.volume G' ≀ 2 ^ (-1) * MeasureTheory.volume G

        Lemma 5.1.1