Documentation

Carleson.ForestOperator.Forests

Lemmas 7.4.4 #

source
theorem TileStructure.Forest.C7_4_4_def (a n : β„•) :
C7_4_4 a n = 2 ^ (550 * ↑a ^ 3 - 3 * ↑n)
source
@[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
source
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 : 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), adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u₁) g₁ x * (starRingEnd β„‚) (adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚) gβ‚‚ x)β€–β‚Š ≀ ↑(C7_4_4 a n) * MeasureTheory.eLpNorm (fun (x : X) => (↑(π“˜ u₁) ∩ ↑(π“˜ uβ‚‚)).indicator (t.adjointBoundaryOperator u₁ g₁) x) 2 MeasureTheory.volume * MeasureTheory.eLpNorm (fun (x : X) => (↑(π“˜ u₁) ∩ ↑(π“˜ uβ‚‚)).indicator (t.adjointBoundaryOperator uβ‚‚ gβ‚‚) x) 2 MeasureTheory.volume
source
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 : 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), adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u₁) g₁ x * (starRingEnd β„‚) (adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚) gβ‚‚ x)β€–β‚Š ≀ ↑(C7_4_4 a n) * MeasureTheory.eLpNorm (fun (x : X) => (↑(π“˜ u₁) ∩ ↑(π“˜ uβ‚‚)).indicator (t.adjointBoundaryOperator u₁ g₁) x) 2 MeasureTheory.volume * MeasureTheory.eLpNorm (fun (x : X) => (↑(π“˜ u₁) ∩ ↑(π“˜ uβ‚‚)).indicator (t.adjointBoundaryOperator uβ‚‚ gβ‚‚) x) 2 MeasureTheory.volume

Lemma 7.4.4.

Section 7.7 #

source
def TileStructure.Forest.rowDecomp_zornset {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)] (s : Set (𝔓 X)) :
Set (Set (𝔓 X))
Equations
  • One or more equations did not get rendered due to their size.
source
theorem TileStructure.Forest.mem_rowDecomp_zornset_iff {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)] (s s' : Set (𝔓 X)) :
s' ∈ rowDecomp_zornset s ↔ s' βŠ† s ∧ (s'.PairwiseDisjoint fun (x : 𝔓 X) => ↑(π“˜ x)) ∧ βˆ€ u ∈ s', Maximal (fun (x : Grid X) => x ∈ π“˜ '' s) (π“˜ u)
source
theorem TileStructure.Forest.rowDecomp_zornset_chain_Union_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)] (s' : Set (𝔓 X)) {c : Set (Set (𝔓 X))} (hc : c βŠ† rowDecomp_zornset s') (hc_chain : IsChain (fun (x1 x2 : Set (𝔓 X)) => x1 βŠ† x2) c) :
⋃ s ∈ c, s ∈ rowDecomp_zornset s' ∧ βˆ€ s ∈ c, s βŠ† ⋃ s'' ∈ c, s''
source
@[irreducible]
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 : Forest X n) (j : β„•) :
Set (𝔓 X)
Equations
source
theorem TileStructure.Forest.rowDecomp_π”˜_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)] {n : β„•} (t : Forest X n) (j : β„•) :
Maximal (fun (x : Set (𝔓 X)) => x ∈ rowDecomp_zornset (t.π”˜ \ ⋃ (i : β„•), ⋃ (_ : i < j), t.rowDecomp_π”˜ i)) (t.rowDecomp_π”˜ j)
source
theorem TileStructure.Forest.rowDecomp_π”˜_mem_zornset {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 : Forest X n) (j : β„•) :
t.rowDecomp_π”˜ j ∈ rowDecomp_zornset (t.π”˜ \ ⋃ (i : β„•), ⋃ (_ : i < j), t.rowDecomp_π”˜ i)
source
theorem TileStructure.Forest.rowDecomp_π”˜_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 : Forest X n) (j : β„•) :
t.rowDecomp_π”˜ j βŠ† t.π”˜ \ ⋃ (i : β„•), ⋃ (_ : i < j), t.rowDecomp_π”˜ i
source
theorem TileStructure.Forest.rowDecomp_π”˜_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)] {n : β„•} (t : Forest X n) (j : β„•) :
(t.rowDecomp_π”˜ j).PairwiseDisjoint fun (x : 𝔓 X) => ↑(π“˜ x)
source
theorem TileStructure.Forest.mem_rowDecomp_π”˜_maximal {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 : Forest X n) (j : β„•) (x : 𝔓 X) :
x ∈ t.rowDecomp_π”˜ j β†’ Maximal (fun (x : Grid X) => x ∈ π“˜ '' (t.π”˜ \ ⋃ (i : β„•), ⋃ (_ : i < j), t.rowDecomp_π”˜ i)) (π“˜ x)
source
theorem TileStructure.Forest.rowDecomp_π”˜_subset_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)] {n : β„•} (t : Forest X n) (j : β„•) :
t.rowDecomp_π”˜ j βŠ† t.π”˜
source
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 : Forest X n) (j : β„•) :
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
  • One or more equations did not get rendered due to their size.
source
theorem TileStructure.Forest.mem_forest_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)] {n : β„•} {t : Forest X n} {j : β„•} {x : 𝔓 X} (hx : x ∈ t.rowDecomp j) :
x ∈ t
source
theorem TileStructure.Forest.rowDecomp_π”˜_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)] {n : β„•} (t : Forest X n) (j : β„•) :
(t.rowDecomp j).π”˜ = t.rowDecomp_π”˜ j
source
theorem TileStructure.Forest.stackSize_remainder_ge_one_of_exists {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 : Forest X n) (j : β„•) (x : X) (this : βˆƒ 𝔲' ∈ (t.rowDecomp j).π”˜, x ∈ π“˜ 𝔲') :
1 ≀ stackSize ((t.π”˜ \ ⋃ (i : β„•), ⋃ (_ : i < j), (t.rowDecomp i).π”˜) ∩ (t.rowDecomp j).π”˜) x
source
theorem TileStructure.Forest.remainder_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)] {n : β„•} (t : Forest X n) (j : β„•) (x : X) :
stackSize (t.π”˜ \ ⋃ (i : β„•), ⋃ (_ : i < j), (t.rowDecomp i).π”˜) x ≀ 2 ^ n - j
source
@[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 : Forest X n} :
⋃ (j : β„•), ⋃ (_ : j < 2 ^ n), (t.rowDecomp j).π”˜ = t.π”˜

Part of Lemma 7.7.1

source
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 : Forest X n} :
(Set.Iio (2 ^ n)).PairwiseDisjoint fun (x : β„•) => (t.rowDecomp x).π”˜

Part of Lemma 7.7.1

source
@[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 : Forest X n} {u : 𝔓 X} :
(fun (x : 𝔓 X) => (t.rowDecomp j).𝔗 x) u = (fun (x : 𝔓 X) => t.𝔗 x) u
source
@[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
source
theorem TileStructure.Forest.C7_7_2_1_def (a n : β„•) :
C7_7_2_1 a n = 2 ^ (156 * ↑a ^ 3 - ↑n / 2)
source
@[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
source
theorem TileStructure.Forest.C7_7_2_2_def (a n : β„•) :
C7_7_2_2 a n = 2 ^ (257 * ↑a ^ 3 - ↑n / 2)
source
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 : Forest X n} {f : X β†’ β„‚} (hj : j < 2 ^ n) (hg : MeasureTheory.BoundedCompactSupport f) (h2f : βˆ€ (x : X), β€–f xβ€– ≀ G.indicator 1 x) :
MeasureTheory.eLpNorm (βˆ‘ u ∈ {p : 𝔓 X | p ∈ t.rowDecomp j}, adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u) f) 2 MeasureTheory.volume ≀ ↑(C7_7_2_1 a n) * MeasureTheory.eLpNorm f 2 MeasureTheory.volume

Part of Lemma 7.7.2.

source
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 : Forest X n} {u : 𝔓 X} {f : X β†’ β„‚} (hj : j < 2 ^ n) (hf : MeasureTheory.BoundedCompactSupport f) (h2f : βˆ€ (x : X), β€–f xβ€– ≀ G.indicator 1 x) :
MeasureTheory.eLpNorm ((βˆ‘ u ∈ {p : 𝔓 X | p ∈ t.rowDecomp j}, F.indicator) (adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u) f)) 2 MeasureTheory.volume ≀ ↑(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.

source
theorem TileStructure.Forest.C7_7_3_def (a n : β„•) :
C7_7_3 a n = 2 ^ (862 * ↑a ^ 3 - 2 * ↑n)
source
@[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
source
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 : Forest X n} {f₁ fβ‚‚ : X β†’ β„‚} (hjj' : j < j') (hj' : j' < 2 ^ n) (hf₁ : Bornology.IsBounded (Set.range f₁)) (h2f₁ : HasCompactSupport f₁) (h3f₁ : βˆ€ (x : X), β€–f₁ xβ€– ≀ G.indicator 1 x) (hfβ‚‚ : Bornology.IsBounded (Set.range fβ‚‚)) (h2fβ‚‚ : HasCompactSupport fβ‚‚) (h3fβ‚‚ : βˆ€ (x : X), β€–fβ‚‚ xβ€– ≀ G.indicator 1 x) :
β†‘β€–βˆ« (x : X), (βˆ‘ u ∈ {p : 𝔓 X | p ∈ t.rowDecomp j}, adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u) f₁ x) * βˆ‘ u ∈ {p : 𝔓 X | p ∈ t.rowDecomp j'}, adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u) fβ‚‚ xβ€–β‚Š ≀ ↑(C7_7_3 a n) * MeasureTheory.eLpNorm f₁ 2 MeasureTheory.volume * MeasureTheory.eLpNorm fβ‚‚ 2 MeasureTheory.volume

Lemma 7.7.3.

source
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 : Forest X n) (j : β„•) :
Set X

The definition of Eβ±Ό defined above Lemma 7.7.4.

Equations
source
theorem TileStructure.Forest.disjoint_impl {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 p' : 𝔓 X} :
Disjoint (Ξ© p) (Ξ© p') β†’ Disjoint (E p) (E p')
source
theorem TileStructure.Forest.disjoint_of_ne_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)] {n : β„•} {t : Forest X n} {i j : β„•} {u u' : 𝔓 X} (hne : u β‰  u') (hu : u ∈ t.rowDecomp i) (hu' : u' ∈ t.rowDecomp j) {p p' : 𝔓 X} (hp : p ∈ (fun (x : 𝔓 X) => t.𝔗 x) u) (hp' : p' ∈ (fun (x : 𝔓 X) => t.𝔗 x) u') :
Disjoint (E p) (E p')
source
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 : Forest X n} :
(Set.Iio (2 ^ n)).PairwiseDisjoint t.rowSupport

Lemma 7.7.4

Proposition 2.0.4 #

source
theorem C2_0_4_base_def (a : ℝ) :
C2_0_4_base a = 2 ^ (432 * a ^ 3)
source
@[irreducible]
def C2_0_4_base (a : ℝ) :
NNReal
Equations
source
theorem C2_0_4_def (a q : ℝ) (n : β„•) :
C2_0_4 a q n = C2_0_4_base a * 2 ^ (-(q - 1) / q * ↑n)
source
@[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
source
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 ∈ {p : 𝔓 X | p ∈ 𝔉}, 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
source
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 : X β†’ β„‚} {A : Set X} (hf : Measurable f) (h2f : βˆ€ (x : X), β€–f xβ€– ≀ F.indicator 1 x) (hA : MeasurableSet A) (h'A : Bornology.IsBounded A) :
∫⁻ (x : X) in A, β€–βˆ‘ u ∈ {p : 𝔓 X | p ∈ 𝔉}, 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.volume A ^ (1 / 2)

Version of the forest operator theorem, but controlling the integral of the norm instead of the integral of the function multiplied by another function.

source
theorem forest_operator_le_volume {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 : X β†’ β„‚} {A : Set X} (hf : Measurable f) (h2f : βˆ€ (x : X), β€–f xβ€– ≀ F.indicator 1 x) (hA : MeasurableSet A) (h'A : Bornology.IsBounded A) :
∫⁻ (x : X) in A, β€–βˆ‘ u ∈ {p : 𝔓 X | p ∈ 𝔉}, carlesonSum ((fun (x : 𝔓 X) => 𝔉.𝔗 x) u) f xβ€–β‚‘ ≀ ↑(C2_0_4 (↑a) q n) * densβ‚‚ (⋃ u ∈ 𝔉, (fun (x : 𝔓 X) => 𝔉.𝔗 x) u) ^ (q⁻¹ - 2⁻¹) * MeasureTheory.volume F ^ (1 / 2) * MeasureTheory.volume A ^ (1 / 2)

Version of the forest operator theorem, but controlling the integral of the norm instead of the integral of the function multiplied by another function, and with the upper bound in terms of volume F and volume G.