Section 5.3

Note: the lemmas 5.3.1-5.3.3 are in TileStructure.

theorem ordConnected_tilesAt {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 : ℕ} : (TilesAt k).OrdConnected

Lemma 5.3.4

theorem ordConnected_C {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 : ℕ} : (ℭ k n).OrdConnected

Lemma 5.3.5

theorem ordConnected_C1 {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 : ℕ} : (ℭ₁ k n j).OrdConnected

Lemma 5.3.6

theorem ordConnected_C2 {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 : ℕ} : (ℭ₂ k n j).OrdConnected

Lemma 5.3.7

theorem ordConnected_C3 {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 : ℕ} : (ℭ₃ k n j).OrdConnected

Lemma 5.3.8

theorem ordConnected_C4 {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 : ℕ} : (ℭ₄ k n j).OrdConnected

Lemma 5.3.9

theorem ordConnected_C5 {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 : ℕ} : (ℭ₅ k n j).OrdConnected

Lemma 5.3.10

Section 5.4 and Lemma 5.1.2

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 j : ℕ) : Set (𝔓 X)

The subset ℭ₆(k, n, j) of ℭ₅(k, n, j), given above (5.4.1).

Equations

• ℭ₆ k n j = {p : 𝔓 X | p ∈ ℭ₅ k n j ∧ ¬↑(𝓘 p) ⊆ G'}

theorem ℭ₆_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 j : ℕ} : ℭ₆ k n j ⊆ ℭ₅ k n j

theorem ℭ₆_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 j : ℕ} : ℭ₆ k n j ⊆ ℭ k n

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 j : ℕ) (u : 𝔓 X) : Set (𝔓 X)

The subset 𝔗₁(u) of ℭ₁(k, n, j), given in (5.4.1). In lemmas, we will assume u ∈ 𝔘₁ k n l

Equations

• 𝔗₁ k n j u = {p : 𝔓 X | p ∈ ℭ₁ k n j ∧ 𝓘 p ≠ 𝓘 u ∧ smul 2 p ≤ smul 1 u}

theorem 𝓘_lt_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 p' : 𝔓 X} (h : p ∈ 𝔗₁ k n j p') : 𝓘 p < 𝓘 p'

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 j : ℕ) : Set (𝔓 X)

The subset 𝔘₂(k, n, j) of 𝔘₁(k, n, j), given in (5.4.2).

Equations

• 𝔘₂ k n j = {u : 𝔓 X | u ∈ 𝔘₁ k n j ∧ ¬Disjoint (𝔗₁ k n j u) (ℭ₆ k n j)}

theorem 𝔘₂_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 j : ℕ} : 𝔘₂ k n j ⊆ 𝔘₁ k n j

def URel {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 : ℕ) (u u' : 𝔓 X) : Prop

The relation ∼ defined below (5.4.2). It is an equivalence relation on 𝔘₂ k n j.

Equations

• URel k n j u u' = (u = u' ∨ ∃ p ∈ 𝔗₁ k n j u, smul 10 p ≤ smul 1 u')

theorem URel.rfl {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 : ℕ} {u : 𝔓 X} : URel k n j u u

theorem URel.not_disjoint {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 : ℕ} {u u' : 𝔓 X} (hu : u ∈ 𝔘₂ k n j) (hu' : u' ∈ 𝔘₂ k n j) (huu' : URel k n j u u') : ¬Disjoint (Metric.ball (𝒬 u) 100) (Metric.ball (𝒬 u') 100)

Lemma 5.4.1, part 2.

theorem URel.eq {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 : ℕ} {u u' : 𝔓 X} (hu : u ∈ 𝔘₂ k n j) (hu' : u' ∈ 𝔘₂ k n j) (huu' : URel k n j u u') : 𝓘 u = 𝓘 u'

Lemma 5.4.1, part 1.

theorem urel_of_not_disjoint {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 : ℕ} {x y : 𝔓 X} (my : y ∈ 𝔘₂ k n j) (xye : 𝓘 x = 𝓘 y) (nd : ¬Disjoint (Metric.ball (𝒬 x) 100) (Metric.ball (𝒬 y) 100)) : URel k n j y x

Helper for 5.4.2 that is also used in 5.4.9.

theorem equivalenceOn_urel {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 : ℕ} : EquivalenceOn (URel k n j) (𝔘₂ k n j)

Lemma 5.4.2.

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 j : ℕ) : Set (𝔓 X)

𝔘₃(k, n, j) ⊆ 𝔘₂ k n j is an arbitary set of representatives of URel on 𝔘₂ k n j, given above (5.4.5).

Equations

• 𝔘₃ k n j = ⋯.reprs

theorem 𝔘₃_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 j : ℕ} : 𝔘₃ k n j ⊆ 𝔘₂ k n j

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 j : ℕ) (u : 𝔓 X) : Set (𝔓 X)

The subset 𝔗₂(u) of ℭ₆(k, n, j), given in (5.4.5). In lemmas, we will assume u ∈ 𝔘₃ k n l

Equations

• 𝔗₂ k n j u = ℭ₆ k n j ∩ ⋃ u' ∈ 𝔘₂ k n j, ⋃ (_ : URel k n j u u'), 𝔗₁ k n j u'

theorem 𝔗₂_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 j : ℕ} {u : 𝔓 X} : 𝔗₂ k n j u ⊆ ℭ₆ k n j

theorem C6_forest {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 : ℕ} : ℭ₆ k n j = ⋃ u ∈ 𝔘₃ k n j, 𝔗₂ k n j u

Lemma 5.4.3

theorem forest_disjoint {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 : ℕ} : (𝔘₃ k n j).PairwiseDisjoint fun (u : 𝔓 X) => 𝔗₂ k n j u

This one could deserve a lemma in the blueprint, as it is needed to decompose the sum of Carleson operators over disjoint subfamilies.

theorem forest_geometry {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 u : 𝔓 X} (hu : u ∈ 𝔘₃ k n j) (hp : p ∈ 𝔗₂ k n j u) : smul 4 p ≤ smul 1 u

Lemma 5.4.4, verifying (2.0.32)

theorem forest_convex {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 : ℕ} {u : 𝔓 X} : (𝔗₂ k n j u).OrdConnected

Lemma 5.4.5, verifying (2.0.33)

theorem forest_separation {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 u u' : 𝔓 X} (hu : u ∈ 𝔘₃ k n j) (hu' : u' ∈ 𝔘₃ k n j) (huu' : u ≠ u') (hp : p ∈ 𝔗₂ k n j u') (h : 𝓘 p ≤ 𝓘 u) : 2 ^ (defaultZ a * (n + 1)) < dist (𝒬 p) (𝒬 u)

Lemma 5.4.6, verifying (2.0.36) Note: swapped u and u' to match (2.0.36)

theorem forest_inner {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 u : 𝔓 X} (hu : u ∈ 𝔘₃ k n j) (hp : p ∈ 𝔗₂ k n j u) : Metric.ball (𝔠 p) (8 * ↑(defaultD a) ^ 𝔰 p) ⊆ ↑(𝓘 u)

Lemma 5.4.7, verifying (2.0.37)

def C5_4_8 (n : ℕ) : ℕ

The multiplicity appearing in Lemma 5.4.8.

Equations

• C5_4_8 n = (4 * n + 12) * 2 ^ n

theorem exists_smul_le_of_𝔘₃ {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 : ℕ} (u : ↑(𝔘₃ k n j)) : ∃ (m : ↑(𝔐 k n)), smul 100 ↑u ≤ smul 1 ↑m

def mf {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 : ℕ) (u : ↑(𝔘₃ k n j)) : ↑(𝔐 k n)

The good choice of an element to get a contradiction in the proof of Lemma 5.4.8.

Equations

• mf k n j u = ⋯.choose

theorem mf_injOn {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 : ℕ} {x : X} : Set.InjOn (mf k n j) {u : ↑(𝔘₃ k n j) | x ∈ 𝓘 ↑u}

theorem stackSize_𝔘₃_le_𝔐 {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 : ℕ} (x : X) : stackSize (𝔘₃ k n j) x ≤ stackSize (𝔐 k n) x

theorem forest_stacking {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 : ℕ} (x : X) (hkn : k ≤ n) : stackSize (𝔘₃ k n j) x ≤ C5_4_8 n

Lemma 5.4.8, used to verify that 𝔘₄ satisfies 2.0.34.

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 j l : ℕ) : Set (𝔓 X)

Define 𝔘₄ k n j l as the union of 2 ^ n disjoint subfamilies in 𝔘₃ k n j, to make sure the multiplicity is at most 2 ^ n to get a forest.

Equations

• 𝔘₄ k n j l = ⋃ i ∈ Set.Ico (l * 2 ^ n) ((l + 1) * 2 ^ n), iteratedMaximalSubfamily (𝔘₃ k n j) i

theorem 𝔘₄_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 j l : ℕ} : 𝔘₄ k n j l ⊆ 𝔘₃ k n j

theorem iUnion_𝔘₄ {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 : ℕ} (hkn : k ≤ n) : ⋃ l ∈ Set.Iio (4 * n + 12), 𝔘₄ k n j l = 𝔘₃ k n j

The sets (𝔘₄(k, n, j, l))_l form a partition of 𝔘₃ k n j.

theorem C6_forest' {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 : ℕ} (hkn : k ≤ n) : ℭ₆ k n j = ⋃ l ∈ Set.Iio (4 * n + 12), ⋃ u ∈ 𝔘₄ k n j l, 𝔗₂ k n j u

theorem pairwiseDisjoint_𝔘₄ {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 : ℕ} : Set.univ.PairwiseDisjoint (𝔘₄ k n j)

theorem stackSize_𝔘₄_le {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 : ℕ} (x : X) : stackSize (𝔘₄ k n j l) x ≤ 2 ^ n

def forest {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 : ℕ) : TileStructure.Forest X n

The forest based on 𝔘₄ k n j l.

Equations

• forest k n j l = { 𝔘 := 𝔘₄ k n j l, 𝔗 := 𝔗₂ k n j, nonempty' := ⋯, ordConnected' := ⋯, 𝓘_ne_𝓘' := ⋯, smul_four_le' := ⋯, stackSize_le' := ⋯, dens₁_𝔗_le' := ⋯, lt_dist' := ⋯, ball_subset' := ⋯ }

theorem carlesonSum_𝔓₁_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 𝔓₁ f x = ∑ n ∈ Finset.Iic (maxℭ X), ∑ k ∈ Finset.Iic n, ∑ j ∈ Finset.Iic (2 * n + 3), carlesonSum (ℭ₅ k n j) f x

From the fact that the ℭ₅ k n j are disjoint, one can rewrite the whole Carleson sum over 𝔓₁ (the union of the ℭ₅ k n j) as a sum of Carleson sums over the ℭ₅ k n j.

theorem carlesonSum_ℭ₅_eq_ℭ₆ {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} (hx : x ∈ G \ G') {k n j : ℕ} : carlesonSum (ℭ₅ k n j) f x = carlesonSum (ℭ₆ k n j) f x

The Carleson sum over ℭ₅ and ℭ₆ coincide, for points in G \ G'.

theorem carlesonSum_ℭ₆_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} {k n j : ℕ} (hkn : k ≤ n) : carlesonSum (ℭ₆ k n j) f x = ∑ l ∈ Finset.Iio (4 * n + 12), carlesonSum (⋃ u ∈ 𝔘₄ k n j l, 𝔗₂ k n j u) f x

The Carleson sum over ℭ₆ can be decomposed as a sum over 4 n + 12 forests based on 𝔘₄ k n j l.

theorem lintegral_carlesonSum_forest {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 : ℕ} {f : X → ℂ} (hf : Measurable f) (h2f : ∀ (x : X), ‖f x‖ ≤ F.indicator 1 x) : ∫⁻ (x : X) in G \ G', ↑‖carlesonSum (⋃ u ∈ 𝔘₄ k n j l, 𝔗₂ k n j u) f x‖₊ ≤ ↑(C2_0_4 (↑a) q n) * (2 ^ (2 * a + 5) * MeasureTheory.volume F / MeasureTheory.volume G) ^ (q⁻¹ - 2⁻¹) * MeasureTheory.volume F ^ (1 / 2) * MeasureTheory.volume G ^ (1 / 2)

For each forest, the integral of the norm of the Carleson sum can be controlled thanks to the forest theorem and to the density control coming from the fact we are away from G₁.

theorem lintegral_carlesonSum_forest' {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 : ℕ} {f : X → ℂ} (hf : Measurable f) (h2f : ∀ (x : X), ‖f x‖ ≤ F.indicator 1 x) : ∫⁻ (x : X) in G \ G', ↑‖carlesonSum (⋃ u ∈ 𝔘₄ k n j l, 𝔗₂ k n j u) f x‖₊ ≤ ↑(C2_0_4 (↑a) q n) * 2 ^ (↑a + 5 / 2) * MeasureTheory.volume G ^ (1 - q⁻¹) * MeasureTheory.volume F ^ q⁻¹

For each forest, the integral of the norm of the Carleson sum can be controlled thanks to the forest theorem and to the density control coming from the fact we are away from G₁. Second version, with the volume of F.

theorem forest_union_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)] {f : X → ℂ} (hf : ∀ (x : X), ‖f x‖ ≤ F.indicator 1 x) (h'f : Measurable f) : ∫⁻ (x : X) in G \ G', ↑‖carlesonSum 𝔓₁ f x‖₊ ≤ ↑(C2_0_4_base ↑a) * 2 ^ (↑a + 5 / 2) * MeasureTheory.volume G ^ (1 - q⁻¹) * MeasureTheory.volume F ^ q⁻¹ * ∑ n ∈ Finset.Iic (maxℭ X), ∑ _k ∈ Finset.Iic n, ∑ _j ∈ Finset.Iic (2 * n + 3), ∑ _l ∈ Finset.Iio (4 * n + 12), 2 ^ (-(q - 1) / q * ↑n)

Putting all the above decompositions together, one obtains a control of the integral of the full Carleson sum over 𝔓₁, as a sum over all the forests.

theorem forest_union_sum_aux1 (M : ℕ) (q : ℝ) (hq : 1 < q) (h'q : q ≤ 2) : ∑ n ∈ Finset.Iic M, ∑ _k ∈ Finset.Iic n, ∑ _j ∈ Finset.Iic (2 * n + 3), ∑ _l ∈ Finset.Iio (4 * n + 12), 2 ^ (-((q - 1) / q * ↑n)) ≤ 13009 / (q - 1) ^ 4

theorem forest_union_sum_aux2 (M : ℕ) (q : ℝ) (hq : 1 < q) (h'q : q ≤ 2) : ∑ n ∈ Finset.Iic M, ∑ _k ∈ Finset.Iic n, ∑ _j ∈ Finset.Iic (2 * n + 3), ∑ _l ∈ Finset.Iio (4 * n + 12), 2 ^ (-((q - 1) / q * ↑n)) ≤ 13009 / ENNReal.ofReal (q - 1) ^ 4

def C5_1_2_optimized (a : ℝ) (q : NNReal) : NNReal

An optimized constant for the forest union theorem. The constant from the blueprint, defined as C5_1_2 below, is slightly worse.

Equations

• C5_1_2_optimized a q = C2_0_4_base a * 2 ^ (a + 5 / 2) * 13009 / (q - 1) ^ 4

theorem forest_union_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_2_optimized (↑a) (nnq X)) * MeasureTheory.volume G ^ (1 - q⁻¹) * MeasureTheory.volume F ^ q⁻¹

Version of the forest union result with a better constant.

theorem C5_1_2_optimized_le' {a : ℕ} {q : NNReal} (ha : 4 ≤ a) : C5_1_2_optimized (↑a) q ≤ C2_0_4_base ↑a * 2 ^ a ^ 3 / (q - 1) ^ 4

def C5_1_2 (a : ℝ) (q : NNReal) : NNReal

The constant used in Lemma 5.1.2, with value 2 ^ (433 * a ^ 3) / (q - 1) ^ 4. The best constant naturally given by this step is C5_1_2_optimized above.

Equations

• C5_1_2 a q = 2 ^ (433 * a ^ 3) / (q - 1) ^ 4

theorem C5_1_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 < C5_1_2 (↑a) (nnq X)

theorem C5_1_2_optimized_le {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ σ₂ F G] : C5_1_2_optimized (↑a) (nnq X) ≤ C5_1_2 (↑a) (nnq X)

theorem forest_union {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_2 (↑a) (nnq X)) * MeasureTheory.volume G ^ (1 - q⁻¹) * MeasureTheory.volume F ^ q⁻¹

Lemma 5.1.2 in the blueprint: the integral of the Carleson sum over the set which can naturally be decomposed as a union of forests can be controlled, thanks to the estimate for a single forest.