Documentation

Carleson.Discrete.ForestComplement

Section 5.5 and Lemma 5.1.3 #

source
def 𝔓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)] :
Set (𝔓 X)

The set 𝔓_{G\G'} in the blueprint

Equations
Instances For
    source
    theorem exists_mem_aux𝓒 {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)] {i : Grid X} (hi : 0 < MeasureTheory.volume (G ∩ ↑i)) :
    βˆƒ (k : β„•), i ∈ aux𝓒 (k + 1)
    source
    theorem exists_k_of_mem_𝔓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)] {p : 𝔓 X} (h : p ∈ 𝔓pos) :
    βˆƒ (k : β„•), p ∈ TilesAt k
    source
    theorem dens'_le_of_mem_𝔓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)] {k : β„•} {p : 𝔓 X} (h : p ∈ 𝔓pos) :
    dens' k {p} ≀ 2 ^ (-↑k)
    source
    theorem exists_Eβ‚‚_volume_pos_of_mem_𝔓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)] {p : 𝔓 X} (h : p ∈ 𝔓pos) :
    βˆƒ (r : β„•), 0 < MeasureTheory.volume (Eβ‚‚ (↑r) p)
    source
    theorem dens'_pos_of_mem_𝔓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)] {k : β„•} {p : 𝔓 X} (h : p ∈ 𝔓pos) (hp : p ∈ TilesAt k) :
    0 < dens' k {p}
    source
    theorem exists_k_n_of_mem_𝔓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)] {p : 𝔓 X} (h : p ∈ 𝔓pos) :
    βˆƒ (k : β„•) (n : β„•), p ∈ β„­ k n ∧ k ≀ n
    source
    theorem exists_k_n_j_of_mem_𝔓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)] {p : 𝔓 X} (h : p ∈ 𝔓pos) :
    βˆƒ (k : β„•) (n : β„•), k ≀ n ∧ (p ∈ 𝔏₀ k n ∨ βˆƒ j ≀ 2 * n + 3, p ∈ ℭ₁ k n j)
    source
    def β„œβ‚€ {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)] :
    Set (𝔓 X)

    The union occurring in the statement of Lemma 5.5.1 containing 𝔏₀

    Equations
    Instances For
      source
      def β„œβ‚ {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)] :
      Set (𝔓 X)

      The union occurring in the statement of Lemma 5.5.1 containing 𝔏₁

      Equations
      Instances For
        source
        def β„œβ‚‚ {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)] :
        Set (𝔓 X)

        The union occurring in the statement of Lemma 5.5.1 containing 𝔏₂

        Equations
        Instances For
          source
          def β„œβ‚ƒ {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)] :
          Set (𝔓 X)

          The union occurring in the statement of Lemma 5.5.1 containing 𝔏₃

          Equations
          Instances For
            source
            theorem mem_iUnion_iff_mem_of_mem_β„­ {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)] {k n : β„•} {p : 𝔓 X} {f : β„• β†’ β„• β†’ Set (𝔓 X)} (hp : p ∈ β„­ k n ∧ k ≀ n) (hf : βˆ€ (k n : β„•), f k n βŠ† β„­ k n) :
            p ∈ ⋃ (n : β„•), ⋃ (k : β„•), ⋃ (_ : k ≀ n), f k n ↔ p ∈ f k n

            Lemma allowing to peel ⋃ (n : β„•) (k ≀ n) from unions in the proof of Lemma 5.5.1.

            source
            theorem mem_iUnion_iff_mem_of_mem_ℭ₁ {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)] {k n j : β„•} {p : 𝔓 X} {f : β„• β†’ Set (𝔓 X)} (hp : p ∈ ℭ₁ k n j ∧ j ≀ 2 * n + 3) (hf : βˆ€ (j : β„•), f j βŠ† ℭ₁ k n j) :
            p ∈ ⋃ (j : β„•), ⋃ (_ : j ≀ 2 * n + 3), f j ↔ p ∈ f j

            Lemma allowing to peel ⋃ (j ≀ 2 * n + 3) from unions in the proof of Lemma 5.5.1.

            source
            theorem antichain_decomposition {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)] :
            𝔓pos ∩ π”“β‚αΆœ = β„œβ‚€ βˆͺ β„œβ‚ βˆͺ β„œβ‚‚ βˆͺ β„œβ‚ƒ

            Lemma 5.5.1

            source
            def 𝔏₀' {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)] (k n l : β„•) :
            Set (𝔓 X)

            The subset 𝔏₀(k, n, l) of 𝔏₀(k, n), given in Lemma 5.5.3. We use the name 𝔏₀' in Lean. The indexing is off-by-one w.r.t. the blueprint

            Equations
            Instances For
              source
              theorem ceil_log2_le_floor_four_add_log2 {l : ℝ} (hl : 2 ≀ l) :
              ⌈Real.logb 2 ((l + 6 / 5) / 5⁻¹)βŒ‰β‚Š ≀ ⌊4 + Real.logb 2 lβŒ‹β‚Š

              Logarithmic inequality used in the proof of Lemma 5.5.2.

              source
              def 𝔒 {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)] (p' : 𝔓 X) (l : NNReal) :
              Finset (𝔓 X)

              The set 𝔒 in the proof of Lemma 5.5.2.

              Equations
              Instances For
                source
                theorem card_𝔒 {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)] (p' : 𝔓 X) {l : NNReal} (hl : 2 ≀ l) :
                (𝔒 p' l).card ≀ ⌊2 ^ (4 * a) * l ^ aβŒ‹β‚Š
                source
                theorem lt_quotient_rearrange {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)] {n : β„•} {p' : 𝔓 X} {l : NNReal} (hl : 2 ≀ l) (qp' : 2 ^ (4 * ↑a - ↑n) < ↑l ^ (-↑a) * MeasureTheory.volume (Eβ‚‚ (↑l) p') / MeasureTheory.volume ↑(π“˜ p')) :
                ↑(2 ^ (4 * a) * l ^ a) * 2 ^ (-↑n) < MeasureTheory.volume (Eβ‚‚ (↑l) p') / MeasureTheory.volume ↑(π“˜ p')
                source
                theorem l_upper_bound {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)] {n : β„•} {p' : 𝔓 X} {l : NNReal} (hl : 2 ≀ l) (qp' : 2 ^ (4 * ↑a - ↑n) < ↑l ^ (-↑a) * MeasureTheory.volume (Eβ‚‚ (↑l) p') / MeasureTheory.volume ↑(π“˜ p')) :
                l < 2 ^ n
                source
                theorem exists_𝔒_with_le_quotient {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)] {n : β„•} {p' : 𝔓 X} {l : NNReal} (hl : 2 ≀ l) (qp' : 2 ^ (4 * ↑a - ↑n) < ↑l ^ (-↑a) * MeasureTheory.volume (Eβ‚‚ (↑l) p') / MeasureTheory.volume ↑(π“˜ p')) :
                βˆƒ b ∈ 𝔒 p' l, 2 ^ (-↑n) < MeasureTheory.volume (E₁ b) / MeasureTheory.volume ↑(π“˜ b)
                source
                theorem iUnion_L0' {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)] {k n : β„•} :
                ⋃ (l : β„•), ⋃ (_ : l ≀ n), 𝔏₀' k n l = 𝔏₀ k n

                Main part of Lemma 5.5.2.

                source
                theorem pairwiseDisjoint_L0' {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)] {k n : β„•} :
                Set.univ.PairwiseDisjoint (𝔏₀' k n)

                Part of Lemma 5.5.2

                source
                theorem antichain_L0' {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)] {k n l : β„•} :
                IsAntichain (fun (x1 x2 : 𝔓 X) => x1 ≀ x2) (𝔏₀' k n l)

                Part of Lemma 5.5.2

                source
                theorem antichain_L2 {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)] {k n j : β„•} :
                IsAntichain (fun (x1 x2 : 𝔓 X) => x1 ≀ x2) (𝔏₂ k n j)

                Lemma 5.5.3

                source
                theorem antichain_L1 {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)] {k n j l : β„•} :
                IsAntichain (fun (x1 x2 : 𝔓 X) => x1 ≀ x2) (𝔏₁ k n j l)

                Part of Lemma 5.5.4

                source
                theorem antichain_L3 {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)] {k n j l : β„•} :
                IsAntichain (fun (x1 x2 : 𝔓 X) => x1 ≀ x2) (𝔏₃ k n j l)

                Part of Lemma 5.5.4

                source
                def C5_1_3 (a : ℝ) (q : NNReal) :
                NNReal

                The constant used in Lemma 5.1.3, with value 2 ^ (210 * a ^ 3) / (q - 1) ^ 5

                Equations
                Instances For
                  source
                  theorem C5_1_3_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)] :
                  C5_1_3 (↑a) (nnq X) > 0
                  source
                  theorem forest_complement {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)] {f : X β†’ β„‚} (hf : βˆ€ (x : X), β€–f xβ€– ≀ F.indicator 1 x) :
                  ∫⁻ (x : X) in G \ G', ↑‖carlesonSum π”“β‚αΆœ f xβ€–β‚Š ≀ ↑(C5_1_3 (↑a) (nnq X)) * MeasureTheory.volume G ^ (1 - q⁻¹) * MeasureTheory.volume F ^ q⁻¹