Lemmas 7.4.4

theorem TileStructure.Forest.C7_4_4_def (a n : ℕ) : TileStructure.Forest.C7_4_4 a n = 2 ^ (550 * ↑a ^ 3 - 3 * ↑n)

@[irreducible]

def TileStructure.Forest.C7_4_4 (a n : ℕ) : NNReal

The constant used in correlation_separated_trees. Has value 2 ^ (550 * a ^ 3 - 3 * n) in the blueprint.

Equations

• TileStructure.Forest.C7_4_4 = TileStructure.Forest.wrapped✝.1

theorem TileStructure.Forest.correlation_separated_trees_of_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)] {n : ℕ} {t : TileStructure.Forest X n} {u₁ u₂ : 𝔓 X} {f₁ f₂ g₁ g₂ : X → ℂ} (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂) (h2u : 𝓘 u₁ ≤ 𝓘 u₂) (hf₁ : Bornology.IsBounded (Set.range f₁)) (h2f₁ : HasCompactSupport f₁) (hf₂ : Bornology.IsBounded (Set.range f₂)) (h2f₂ : HasCompactSupport f₂) : ↑‖∫ (x : X), TileStructure.Forest.adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u₁) g₁ x * (starRingEnd ℂ) (TileStructure.Forest.adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u₂) g₂ x)‖₊ ≤ ↑(TileStructure.Forest.C7_4_4 a n) * MeasureTheory.eLpNorm (fun (x : X) => ((↑(𝓘 u₁) ∩ ↑(𝓘 u₂)).indicator (t.adjointBoundaryOperator u₁ g₁) x).toReal) 2 MeasureTheory.volume * MeasureTheory.eLpNorm (fun (x : X) => ((↑(𝓘 u₁) ∩ ↑(𝓘 u₂)).indicator (t.adjointBoundaryOperator u₂ g₂) x).toReal) 2 MeasureTheory.volume

theorem TileStructure.Forest.correlation_separated_trees {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 : ℕ} {t : TileStructure.Forest X n} {u₁ u₂ : 𝔓 X} {f₁ f₂ g₁ g₂ : X → ℂ} (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂) (hf₁ : Bornology.IsBounded (Set.range f₁)) (h2f₁ : HasCompactSupport f₁) (hf₂ : Bornology.IsBounded (Set.range f₂)) (h2f₂ : HasCompactSupport f₂) : ↑‖∫ (x : X), TileStructure.Forest.adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u₁) g₁ x * (starRingEnd ℂ) (TileStructure.Forest.adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u₂) g₂ x)‖₊ ≤ ↑(TileStructure.Forest.C7_4_4 a n) * MeasureTheory.eLpNorm (fun (x : X) => ((↑(𝓘 u₁) ∩ ↑(𝓘 u₂)).indicator (t.adjointBoundaryOperator u₁ g₁) x).toReal) 2 MeasureTheory.volume * MeasureTheory.eLpNorm (fun (x : X) => ((↑(𝓘 u₁) ∩ ↑(𝓘 u₂)).indicator (t.adjointBoundaryOperator u₂ g₂) x).toReal) 2 MeasureTheory.volume

Lemma 7.4.4.

Section 7.7

def TileStructure.Forest.rowDecomp {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 : ℕ} (t : TileStructure.Forest X n) (j : ℕ) : TileStructure.Row X n

The row-decomposition of a tree, defined in the proof of Lemma 7.7.1. The indexing is off-by-one compared to the blueprint.

Equations

• t.rowDecomp j = sorry

@[simp]

theorem TileStructure.Forest.biUnion_rowDecomp {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 : ℕ} {t : TileStructure.Forest X n} : ⋃ (j : ℕ), ⋃ (_ : j < 2 ^ n), (t.rowDecomp j).𝔘 = t.𝔘

Part of Lemma 7.7.1

theorem TileStructure.Forest.pairwiseDisjoint_rowDecomp {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 : ℕ} {t : TileStructure.Forest X n} : (Set.Iio (2 ^ n)).PairwiseDisjoint fun (x : ℕ) => (t.rowDecomp x).𝔘

Part of Lemma 7.7.1

@[simp]

theorem TileStructure.Forest.rowDecomp_apply {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 j : ℕ} {t : TileStructure.Forest X n} {u : 𝔓 X} : (fun (x : 𝔓 X) => (t.rowDecomp j).𝔗 x) u = (fun (x : 𝔓 X) => t.𝔗 x) u

@[irreducible]

def TileStructure.Forest.C7_7_2_1 (a n : ℕ) : NNReal

The constant used in row_bound. Has value 2 ^ (156 * a ^ 3 - n / 2) in the blueprint.

Equations

• TileStructure.Forest.C7_7_2_1 = TileStructure.Forest.wrapped✝.1

theorem TileStructure.Forest.C7_7_2_1_def (a n : ℕ) : TileStructure.Forest.C7_7_2_1 a n = 2 ^ (156 * ↑a ^ 3 - ↑n / 2)

@[irreducible]

def TileStructure.Forest.C7_7_2_2 (a n : ℕ) : NNReal

The constant used in indicator_row_bound. Has value 2 ^ (257 * a ^ 3 - n / 2) in the blueprint.

Equations

• TileStructure.Forest.C7_7_2_2 = TileStructure.Forest.wrapped✝.1

theorem TileStructure.Forest.C7_7_2_2_def (a n : ℕ) : TileStructure.Forest.C7_7_2_2 a n = 2 ^ (257 * ↑a ^ 3 - ↑n / 2)

theorem TileStructure.Forest.row_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 j : ℕ} {t : TileStructure.Forest X n} {f : X → ℂ} (hj : j < 2 ^ n) (hf : MeasureTheory.BoundedCompactSupport f) : MeasureTheory.eLpNorm (∑ u ∈ Finset.filter (fun (p : 𝔓 X) => p ∈ t.rowDecomp j) Finset.univ, TileStructure.Forest.adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u) f) 2 MeasureTheory.volume ≤ ↑(TileStructure.Forest.C7_7_2_1 a n) * MeasureTheory.eLpNorm f 2 MeasureTheory.volume

Part of Lemma 7.7.2.

theorem TileStructure.Forest.indicator_row_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 j : ℕ} {t : TileStructure.Forest X n} {u : 𝔓 X} {f : X → ℂ} (hj : j < 2 ^ n) (hf : MeasureTheory.BoundedCompactSupport f) : MeasureTheory.eLpNorm ((∑ u ∈ Finset.filter (fun (p : 𝔓 X) => p ∈ t.rowDecomp j) Finset.univ, F.indicator) (TileStructure.Forest.adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u) f)) 2 MeasureTheory.volume ≤ ↑(TileStructure.Forest.C7_7_2_2 a n) * dens₂ (⋃ u ∈ t, (fun (x : 𝔓 X) => t.𝔗 x) u) ^ 2⁻¹ * MeasureTheory.eLpNorm f 2 MeasureTheory.volume

Part of Lemma 7.7.2.

theorem TileStructure.Forest.C7_7_3_def (a n : ℕ) : TileStructure.Forest.C7_7_3 a n = 2 ^ (862 * ↑a ^ 3 - 2 * ↑n)

@[irreducible]

def TileStructure.Forest.C7_7_3 (a n : ℕ) : NNReal

The constant used in row_correlation. Has value 2 ^ (862 * a ^ 3 - 3 * n) in the blueprint.

Equations

• TileStructure.Forest.C7_7_3 = TileStructure.Forest.wrapped✝.1

theorem TileStructure.Forest.row_correlation {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 j j' : ℕ} {t : TileStructure.Forest X n} {f₁ f₂ : X → ℂ} (hjj' : j < j') (hj' : j' < 2 ^ n) (hf₁ : Bornology.IsBounded (Set.range f₁)) (h2f₁ : HasCompactSupport f₁) (hf₂ : Bornology.IsBounded (Set.range f₂)) (h2f₂ : HasCompactSupport f₂) : ↑‖∫ (x : X), (∑ u ∈ Finset.filter (fun (p : 𝔓 X) => p ∈ t.rowDecomp j) Finset.univ, TileStructure.Forest.adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u) f₁ x) * ∑ u ∈ Finset.filter (fun (p : 𝔓 X) => p ∈ t.rowDecomp j') Finset.univ, TileStructure.Forest.adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u) f₂ x‖₊ ≤ ↑(TileStructure.Forest.C7_7_3 a n) * MeasureTheory.eLpNorm f₁ 2 MeasureTheory.volume * MeasureTheory.eLpNorm f₂ 2 MeasureTheory.volume

Lemma 7.7.3.

def TileStructure.Forest.rowSupport {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 : ℕ} (t : TileStructure.Forest X n) (j : ℕ) : Set X

The definition of Eⱼ defined above Lemma 7.7.4.

Equations

• t.rowSupport j = ⋃ u ∈ t.rowDecomp j, ⋃ p ∈ (fun (x : 𝔓 X) => t.𝔗 x) u, E p

theorem TileStructure.Forest.pairwiseDisjoint_rowSupport {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 : ℕ} {t : TileStructure.Forest X n} : (Set.Iio (2 ^ n)).PairwiseDisjoint t.rowSupport

Lemma 7.7.4

Proposition 2.0.4

@[irreducible]

def C2_0_4 (a q : ℝ) (n : ℕ) : NNReal

The constant used in forest_operator. Has value 2 ^ (432 * a ^ 3 - (q - 1) / q * n) in the blueprint.

Equations

• C2_0_4 = wrapped✝.1

theorem C2_0_4_def (a q : ℝ) (n : ℕ) : C2_0_4 a q n = 2 ^ (432 * a ^ 3 - (q - 1) / q * ↑n)

theorem forest_operator {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 : ℕ} (𝔉 : TileStructure.Forest X n) {f g : X → ℂ} (hf : Measurable f) (h2f : ∀ (x : X), ‖f x‖ ≤ F.indicator 1 x) (hg : Measurable g) (h2g : Bornology.IsBounded (Function.support g)) : ↑‖∫ (x : X), (starRingEnd ℂ) (g x) * ∑ u ∈ Finset.filter (fun (p : 𝔓 X) => p ∈ 𝔉) Finset.univ, carlesonSum ((fun (x : 𝔓 X) => 𝔉.𝔗 x) u) f x‖₊ ≤ ↑(C2_0_4 (↑a) q n) * dens₂ (⋃ u ∈ 𝔉, (fun (x : 𝔓 X) => 𝔉.𝔗 x) u) ^ (q⁻¹ - 2⁻¹) * MeasureTheory.eLpNorm f 2 MeasureTheory.volume * MeasureTheory.eLpNorm g 2 MeasureTheory.volume