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_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)] {k n : β„•} {p : 𝔓 X} (h : p ∈ 𝔓pos) (mp : p ∈ β„­ k n) (hkn : k ≀ n) :
    p ∈ 𝔏₀ k n ∨ βˆƒ j ≀ 2 * n + 3, p ∈ ℭ₁ k n j
    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 nmem_β„­β‚…_iff_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} (hkn : k ≀ n) (hj : j ≀ 2 * n + 3) (h : p ∈ 𝔓pos) (mc2 : p ∈ β„­β‚‚ k n j) (ml2 : p βˆ‰ 𝔏₂ k n j) :
            p βˆ‰ β„­β‚… k n j ↔ p ∈ ⋃ (l : β„•), ⋃ (_ : l ≀ defaultZ a * (n + 1)), 𝔏₃ k n j l
            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.

            We will not use the lemma in this form, as to decompose the Carleson sum it is also crucial that the union is disjoint. This is easier to formalize by decomposing into successive terms, taking advantage of disjointess at each step, instead of doing everything in one go. Still, we keep this lemma as it corresponds to the blueprint, and the key steps of its proof will also be the key steps when doing the successive decompositions.

            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.

            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
                theorem carlesonSum_𝔓₁_compl_eq_𝔓pos_inter {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 β†’ β„‚) :
                βˆ€α΅ (x : X), x ∈ G \ G' β†’ carlesonSum π”“β‚αΆœ f x = carlesonSum (𝔓pos ∩ π”“β‚αΆœ) f x

                The Carleson sum over π”“β‚αΆœ and 𝔓pos ∩ π”“β‚αΆœ coincide at ae every point of G \ G'.

                source
                theorem carlesonSum_𝔓pos_eq_sum {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 β†’ β„‚} {x : X} :
                carlesonSum (𝔓pos ∩ π”“β‚αΆœ) f x = βˆ‘ n ∈ Finset.Iic (maxβ„­ X), βˆ‘ k ∈ Finset.Iic n, carlesonSum (𝔓pos ∩ π”“β‚αΆœ ∩ β„­ k n) f x

                The Carleson sum over 𝔓pos ∩ π”“β‚αΆœ can be decomposed as a sum over the intersections of this set with various β„­ k n.

                source
                theorem carlesonSum_𝔓pos_inter_β„­_eq_add_sum {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 : β„•} {f : X β†’ β„‚} {x : X} (hkn : k ≀ n) :
                carlesonSum (𝔓pos ∩ π”“β‚αΆœ ∩ β„­ k n) f x = carlesonSum (𝔓pos ∩ π”“β‚αΆœ ∩ 𝔏₀ k n) f x + βˆ‘ j ∈ Finset.Iic (2 * n + 3), carlesonSum (𝔓pos ∩ π”“β‚αΆœ ∩ ℭ₁ k n j) f x

                In each set β„­ k n, the Carleson sum can be decomposed as a sum over 𝔏₀ k n and over various ℭ₁ k n j.

                source
                theorem carlesonSum_𝔓pos_inter_𝔏₀_eq_sum {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 : β„•} {f : X β†’ β„‚} {x : X} :
                carlesonSum (𝔓pos ∩ π”“β‚αΆœ ∩ 𝔏₀ k n) f x = βˆ‘ l ∈ Finset.Iio n, carlesonSum (𝔓pos ∩ π”“β‚αΆœ ∩ 𝔏₀' k n l) f x
                source
                theorem carlesonSum_𝔓pos_inter_ℭ₁_eq_add_sum {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 : β„•} {f : X β†’ β„‚} {x : X} :
                carlesonSum (𝔓pos ∩ π”“β‚αΆœ ∩ ℭ₁ k n j) f x = carlesonSum (𝔓pos ∩ π”“β‚αΆœ ∩ β„­β‚‚ k n j) f x + βˆ‘ l ∈ Finset.Iic (defaultZ a * (n + 1)), carlesonSum (𝔓pos ∩ π”“β‚αΆœ ∩ 𝔏₁ k n j l) f x

                In each set ℭ₁ k n j, the Carleson sum can be decomposed as a sum over β„­β‚‚ k n j and over various 𝔏₁ k n j l.

                source
                theorem carlesonSum_𝔓pos_inter_β„­β‚‚_eq_add_sum {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 : β„•} {f : X β†’ β„‚} {x : X} (hkn : k ≀ n) (hj : j ≀ 2 * n + 3) :
                carlesonSum (𝔓pos ∩ π”“β‚αΆœ ∩ β„­β‚‚ k n j) f x = carlesonSum (𝔓pos ∩ π”“β‚αΆœ ∩ 𝔏₂ k n j) f x + βˆ‘ l ∈ Finset.Iic (defaultZ a * (n + 1)), carlesonSum (𝔓pos ∩ π”“β‚αΆœ ∩ 𝔏₃ k n j l) f x

                In each set β„­β‚‚ k n j, the Carleson sum can be decomposed as a sum over 𝔏₂ k n j and over various 𝔏₃ k n j l.

                source
                theorem lintegral_carlesonSum_𝔓₁_compl_le_sum_lintegral {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 β†’ β„‚} (h'f : Measurable f) :
                ∫⁻ (x : X) in G \ G', ↑‖carlesonSum π”“β‚αΆœ f xβ€–β‚Š ≀ (((βˆ‘ n ∈ Finset.Iic (maxβ„­ X), βˆ‘ k ∈ Finset.Iic n, βˆ‘ l ∈ Finset.Iio n, ∫⁻ (x : X) in G \ G', ↑‖carlesonSum (𝔓pos ∩ π”“β‚αΆœ ∩ 𝔏₀' k n l) f xβ€–β‚Š) + βˆ‘ n ∈ Finset.Iic (maxβ„­ X), βˆ‘ k ∈ Finset.Iic n, βˆ‘ j ∈ Finset.Iic (2 * n + 3), βˆ‘ l ∈ Finset.Iic (defaultZ a * (n + 1)), ∫⁻ (x : X) in G \ G', ↑‖carlesonSum (𝔓pos ∩ π”“β‚αΆœ ∩ 𝔏₁ k n j l) f xβ€–β‚Š) + βˆ‘ n ∈ Finset.Iic (maxβ„­ X), βˆ‘ k ∈ Finset.Iic n, βˆ‘ j ∈ Finset.Iic (2 * n + 3), ∫⁻ (x : X) in G \ G', ↑‖carlesonSum (𝔓pos ∩ π”“β‚αΆœ ∩ 𝔏₂ k n j) f xβ€–β‚Š) + βˆ‘ n ∈ Finset.Iic (maxβ„­ X), βˆ‘ k ∈ Finset.Iic n, βˆ‘ j ∈ Finset.Iic (2 * n + 3), βˆ‘ l ∈ Finset.Iic (defaultZ a * (n + 1)), ∫⁻ (x : X) in G \ G', ↑‖carlesonSum (𝔓pos ∩ π”“β‚αΆœ ∩ 𝔏₃ k n j l) f xβ€–β‚Š

                Putting together all the previous decomposition lemmas, one gets an estimate of the integral of β€–carlesonSum π”“β‚αΆœ f xβ€–β‚Š by a sum of integrals of the same form over various subsets of 𝔓, which are all antichains by design.

                source
                theorem lintegral_nnnorm_carlesonSum_le_of_isAntichain_subset_β„­ {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 : β„•} {f : X β†’ β„‚} {𝔄 : Set (𝔓 X)} (hf : βˆ€ (x : X), β€–f xβ€– ≀ F.indicator 1 x) (h'f : Measurable f) (hA : IsAntichain (fun (x1 x2 : 𝔓 X) => x1 ≀ x2) 𝔄) (h'A : 𝔄 βŠ† β„­ k n) :
                ∫⁻ (x : X) in G \ G', ↑‖carlesonSum (𝔓pos ∩ π”“β‚αΆœ ∩ 𝔄) f xβ€–β‚Š ≀ ↑(C_2_0_3 (↑a) (nnq X)) * 2 ^ (a + 3) * MeasureTheory.volume G ^ (1 - q⁻¹) * MeasureTheory.volume F ^ q⁻¹ * 2 ^ (-((q - 1) / (8 * ↑a ^ 4) * ↑n))

                Custom version of the antichain operator theorem, in the specific form we need to handle the various terms in the previous statement.

                source
                theorem lintegral_carlesonSum_𝔓₁_compl_le_sum_aux1 {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] {N : β„•} :
                βˆ‘ x ∈ Finset.Iic N, ((12 + 8 * ↑(defaultZ a)) * ↑x ^ 0 + (19 + 20 * ↑(defaultZ a)) * ↑x ^ 1 + (7 + 16 * ↑(defaultZ a)) * ↑x ^ 2 + 4 * ↑(defaultZ a) * ↑x ^ 3) * 2 ^ (-((q - 1) / (8 * ↑a ^ 4) * ↑x)) ≀ 2 ^ (28 * a + 20) / (q - 1) ^ 4
                source
                theorem lintegral_carlesonSum_𝔓₁_compl_le_sum_aux2 {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] {N : β„•} :
                βˆ‘ x ∈ Finset.Iic N, (12 + 8 * ↑(defaultZ a) + (19 + 20 * ↑(defaultZ a)) * ↑x + (7 + 16 * ↑(defaultZ a)) * ↑x ^ 2 + 4 * ↑(defaultZ a) * ↑x ^ 3) * 2 ^ (-((q - 1) / (8 * ↑a ^ 4) * ↑x)) ≀ 2 ^ (28 * a + 20) / (↑(nnq X) - 1) ^ 4
                source
                def C5_1_3_optimized (a : β„•) (q : NNReal) :
                NNReal

                An optimized constant for Lemma 5.1.3.

                Equations
                Instances For
                  source
                  def C5_1_3 (a : β„•) (q : NNReal) :
                  NNReal

                  The constant used in Lemma 5.1.3 in the blueprint, with value 2 ^ (153 * 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] :
                    0 < C5_1_3 a (nnq X)
                    source
                    theorem C5_1_3_optimized_le_C5_1_3 {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] :
                    C5_1_3_optimized a (nnq X) ≀ C5_1_3 a (nnq X)
                    source
                    theorem forest_complement_optimized {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) (h'f : Measurable f) :
                    ∫⁻ (x : X) in G \ G', ↑‖carlesonSum π”“β‚αΆœ f xβ€–β‚Š ≀ ↑(C5_1_3_optimized a (nnq X)) * MeasureTheory.volume G ^ (1 - q⁻¹) * MeasureTheory.volume F ^ q⁻¹
                    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) (h'f : Measurable f) :
                    ∫⁻ (x : X) in G \ G', ↑‖carlesonSum π”“β‚αΆœ f xβ€–β‚Š ≀ ↑(C5_1_3 a (nnq X)) * MeasureTheory.volume G ^ (1 - q⁻¹) * MeasureTheory.volume F ^ q⁻¹

                    Lemma 5.1.3, proving the bound on the integral of the Carleson sum over all leftover tiles which do not fit in a forest. It follows from a careful grouping of these tiles into finitely many antichains.