1.4. Proof of Finitary Carleson
To prove Proposition Theorem 1.2.1, we already fixed in
Proof of Metric Space Carleson, overview measurable functions \sigma_1,\sigma_2, \tQ and Borel
sets F,G. We have also defined S to be the smallest integer such that
the ranges of \sigma_1 and \sigma_2 are contained in [-S,S] and F
and G are contained in the ball B(o, \frac 14 D^S).
The proof of the next lemma is done in Proof of Grid Existence Lemma, following the construction of dyadic cubes in the literature.
There exists a grid structure (\mathcal{D}, c,s).
Lean code for Lemma1.4.1●1 definition
Associated Lean declarations
-
grid_existence[complete]
-
grid_existence[complete]
-
defdefined in Carleson/TileExistence.leancomplete
def grid_existence.{u_1} (X : Type u_1) {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] : GridStructure X (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)
def grid_existence.{u_1} (X : Type u_1) {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] : GridStructure X (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)
Proof that there exists a grid structure.
The next lemma, which we prove in Proof of Tile Structure Lemma, should be compared with the construction in the literature.
For a given grid structure (\mathcal{D}, c,s), there exists a tile
structure (\fP,\scI,\fc,\fcc,\pc,\ps).
Lean code for Lemma1.4.2●1 definition
Associated Lean declarations
-
tile_existence[complete]
-
tile_existence[complete]
-
defdefined in Carleson/TileExistence.leancomplete
def tile_existence.{u_1} (X : Type u_1) {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] [GridStructure X (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] : TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)
def tile_existence.{u_1} (X : Type u_1) {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] [GridStructure X (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] : TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)
Choose a grid structure (\mathcal{D}, c,s) with Lemma 1.4.1 and a tile
structure for this grid structure (\fP,\scI,\fc,\fcc,\pc,\ps) with
Lemma 1.4.2. Applying Theorem 1.2.2, we obtain a Borel set G' in
X with 2\mu(G')\leq \mu(G) such that for all Borel functions
f:X\to \C with |f|\le \mathbf{1}_F we have disclesssim.
-
tile_sum_operator[complete] -
integrable_tile_sum_operator[complete]
We have for all x\in G\setminus G'
\sum_{\fp\in \fP}T_{\fp} f(x)= \sum_{s=\sigma_1(x)}^{\sigma_2(x)}
\int K_{s}(x,y) f(y) e(\tQ(x)(y)-\tQ(x)(x))\, d\mu(y).
Lean code for Lemma1.4.3●2 theorems
Associated Lean declarations
-
tile_sum_operator[complete]
-
integrable_tile_sum_operator[complete]
-
tile_sum_operator[complete] -
integrable_tile_sum_operator[complete]
-
theoremdefined in Carleson/FinitaryCarleson.leancomplete
theorem tile_sum_operator.{u_1} {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)] {G' : Set X} {f : X → ℂ} {x : X} (hx : x ∈ G \ G') : ∑ p, carlesonOn p f x = ∑ s ∈ (Set.Icc (σ₁ x) (σ₂ x)).toFinset, ∫ (y : X), Ks s x y * f y * Complex.exp (Complex.I * (↑((Q x) y) - ↑((Q x) x)))
theorem tile_sum_operator.{u_1} {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)] {G' : Set X} {f : X → ℂ} {x : X} (hx : x ∈ G \ G') : ∑ p, carlesonOn p f x = ∑ s ∈ (Set.Icc (σ₁ x) (σ₂ x)).toFinset, ∫ (y : X), Ks s x y * f y * Complex.exp (Complex.I * (↑((Q x) y) - ↑((Q x) x)))
Lemma 4.0.3
-
theoremdefined in Carleson/FinitaryCarleson.leancomplete
theorem integrable_tile_sum_operator.{u_1} {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ σ₂ F G] {f : X → ℂ} (hf : Measurable f) (h2f : ∀ (x : X), ‖f x‖ ≤ F.indicator 1 x) {x : X} {s : ℤ} : MeasureTheory.Integrable (fun y ↦ Ks s x y * f y * Complex.exp (Complex.I * (↑((Q x) y) - ↑((Q x) x)))) MeasureTheory.volume
theorem integrable_tile_sum_operator.{u_1} {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ σ₂ F G] {f : X → ℂ} (hf : Measurable f) (h2f : ∀ (x : X), ‖f x‖ ≤ F.indicator 1 x) {x : X} {s : ℤ} : MeasureTheory.Integrable (fun y ↦ Ks s x y * f y * Complex.exp (Complex.I * (↑((Q x) y) - ↑((Q x) x)))) MeasureTheory.volume
Proof. Fix x\in G\setminus G'. Sorting the tiles \fp on the left-hand
side by the value \ps(\fp)\in [-S,S], it suffices to prove for every
-S\le s\le S that
\sum_{\fp\in \fP: \ps(\fp)=s}T_{\fp} f(x)=0
if s\not\in [\sigma_1(x), \sigma_2(x)] and
\sum_{\fp\in \fP: \ps(\fp)=s}T_{\fp} f(x)=
\int K_{s}(x,y) f(y) e(\tQ(x)(y) - \tQ(x)(x))\, d\mu(y).
if s\in [\sigma_1(x),\sigma_2(x)]. If
s\not\in [\sigma_1(x), \sigma_2(x)], then by definition of E(\fp) we
have x\not\in E(\fp) for any \fp with \ps(\fp)=s and thus
T_{\fp} f(x)=0. This proves the vanishing case.
Now assume s\in [\sigma_1(x),\sigma_2(x)]. By coverdyadic,
subsetmaxcube, eq-vol-sp-cube, the fact that c(I_0) = o and
G\subset B(o,\frac 14 D^S), there is at least one
I\in \mathcal{D} with s(I)=s and x\in I. By dyadicproperty, this
I is unique. By eq-dis-freq-cover, there is precisely one
\fp\in \fP(I) such that \tQ(x)\in \fc(\fp). Hence there is precisely one
\fp\in \fP with \ps(\fp)=s such that x\in E(\fp). For this \fp,
the value T_{\fp}(x) by its definition in definetp equals the right-hand
side of the non-vanishing case. This proves the lemma.
We use this to prove Theorem 1.2.1.
Proof of Theorem 1.2.1. We now estimate with Lemma 1.4.3 and
Theorem 1.2.2
\int_{G \setminus G'} \left|\sum_{s={\sigma_1}(x)}^{{\sigma_2}(x)} \int K_s(x,y) f(y) e(\tQ(x)(y)) \, \mathrm{d}\mu(y)\right| \mathrm{d}\mu(x)
=\int_{G \setminus G'} \left|\sum_{s={\sigma_1}(x)}^{{\sigma_2}(x)} \int K_s(x,y) f(y) e(\tQ(x)(y) - \tQ(x)(x))\mathrm{d}\mu(y)\right| \mathrm{d}\mu(x)
=\int_{G \setminus G'} \left|\sum_{\fp\in \fP}T_{\fp} f(x)\right| \mathrm{d}\mu(x)
\le \frac{2^{442a^3}}{(q-1)^5} \mu(G)^{1 - \frac{1}{q}} \mu(F)^{\frac{1}{q}}.
This proves eq-linearized for the chosen set G' and arbitrary f and
thus completes the proof of Proposition Theorem 1.2.1.
1.4.1. Proof of Grid Existence Lemma
We begin with the construction of the centers of the dyadic cubes.
Let -S\le k\le S. Consider Y\subset X such that for any y\in Y, we
have
y\in B(o,4D^S-D^k),
furthermore, for any y'\in Y with y\neq y', we have
B(y,D^k)\cap B(y',D^k)=\emptyset.
Then the cardinality of Y is bounded by
|Y|\le 2^{3a + 200Sa^3}.
Lean code for Lemma1.4.1.1●1 theorem
Associated Lean declarations
-
counting_balls[complete]
-
counting_balls[complete]
-
theoremdefined in Carleson/TileExistence.leancomplete
theorem counting_balls.{u_1} {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] {k : ℤ} (hk_lower : -↑(defaultS X) ≤ k) {Y : Set X} (hY : Y ⊆ Metric.ball (cancelPt X) (4 * ↑(defaultD a) ^ defaultS X - ↑(defaultD a) ^ k)) (hYdisjoint : Y.PairwiseDisjoint fun x ↦ Metric.ball x (↑(defaultD a) ^ k)) : ↑Y.encard ≤ ↑(C4_1_1 X)
theorem counting_balls.{u_1} {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] {k : ℤ} (hk_lower : -↑(defaultS X) ≤ k) {Y : Set X} (hY : Y ⊆ Metric.ball (cancelPt X) (4 * ↑(defaultD a) ^ defaultS X - ↑(defaultD a) ^ k)) (hYdisjoint : Y.PairwiseDisjoint fun x ↦ Metric.ball x (↑(defaultD a) ^ k)) : ↑Y.encard ≤ ↑(C4_1_1 X)
Proof. Let k and Y be given. By applying the doubling property
doublingx inductively, we have for each integer j\ge 0
\mu(B(y,2^{j}D^k))\le 2^{aj} \mu(B(y,D^k)).
Since X is the union of the balls B(y,2^{j}D^k) and \mu is not zero,
at least one of the balls B(y,2^{j}D^k) has positive measure, thus
B(y,D^k) has positive measure.
Applying the previous estimate for
j' = \ln_2(8D^{2S}) = 3 + 2S \cdot 100a^2 by defineD, using
-S\le k\le S, y\in B(o,4D^S), and the triangle inequality, we have
B(o, 4D^S) \subset B(y, 8D^S) \subset B(y,2^{j'}D^k).
Using the disjointedness of the balls in eq-disj-yballs, ybinb, and the
triangle inequality for \rho, we obtain
|Y|\mu(B(o,4D^S))\le 2^{j'a}\sum_{y\in Y}\mu(B(y,D^k))
\le 2^{j'a}\mu(\bigcup_{y\in Y}B(y,D^k))
\le 2^{j'a}\mu(o,4D^S).
As \mu(o,4D^S) is not zero, the lemma follows.
For each -S\le k\le S, let Y_k be a set of maximal cardinality in X
such that Y=Y_k satisfies the properties ybinb and eq-disj-yballs and
such that o \in Y_k. By the upper bound of Lemma 1.4.1.1, such a set
exists.
For each -S\le k\le S, choose an enumeration of the points in the finite set
Y_k and thus a total order < on Y_k.
For each -S\le k\le S, the ball B(o, 4D^S-D^k) is contained in the union
of the balls B(y,2D^k) with y\in Y_k.
Lean code for Lemma1.4.1.2●1 theorem
Associated Lean declarations
-
cover_big_ball[complete]
-
cover_big_ball[complete]
-
theoremdefined in Carleson/TileExistence.leancomplete
theorem cover_big_ball.{u_1} {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] (k : ℤ) : Metric.ball (cancelPt X) (4 * ↑(defaultD a) ^ defaultS X - ↑(defaultD a) ^ k) ⊆ ⋃ y ∈ Yk X k, Metric.ball y (2 * ↑(defaultD a) ^ k)
theorem cover_big_ball.{u_1} {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] (k : ℤ) : Metric.ball (cancelPt X) (4 * ↑(defaultD a) ^ defaultS X - ↑(defaultD a) ^ k) ⊆ ⋃ y ∈ Yk X k, Metric.ball y (2 * ↑(defaultD a) ^ k)
Proof. Let x be any point of B(o, 4D^S-D^k). By maximality of |Y_k|,
the ball B(x, D^k) intersects one of the balls B(y, D^k) with
y\in Y_k. By the triangle inequality, x\in B(y,2D^k).
Define the set
\mathcal{C}:= \{(y,k): -S\le k\le S, y\in Y_k\},
We totally order the set \mathcal{C} lexicographically by setting
(y,k)<(y',k') if k< k' or both k=k' and y<y'. In what follows, we
define recursively in the sense of this order a function
(I_1,I_2,I_3): \mathcal{C}\to \mathcal{P}(X)\times \mathcal{P}(X)\times \mathcal{P}(X).
Assume the sets {I}_j(y',k') have already been defined for j=1,2,3 if
k'<k and if k=k' and y'<y.
If k=-S, define for j\in \{1,2\} the set {I}_j(y,k) to be
B(y,jD^{-S}). If -S<k, define for j\in \{1,2\} and y\in Y_k the
set {I}_j(y,k) to be
\bigcup\{I_3(y',k-1):
y'\in Y_{k-1}\cap B(y,jD^k)\}.
Define for -S\leq k\leq S and y\in Y_k
I_3(y,k):={I_1}(y,k)\cup \left[{I_2}(y,k)\setminus \left[X_k\cup \bigcup\{I_3(y',k):y'\in Y_{k}, y'<y\})\right]\right]
with
X_{k}:=\bigcup\{I_1(y', k):y'\in Y_{k}\}.
-
I1_prop_1[complete] -
I3_prop_1[complete] -
I2_prop_2[complete] -
I3_prop_2[complete] -
I3_prop_3_1[complete] -
I3_prop_3_2[complete]
For each -S\le k\le S and 1\le j\le 3 the following holds.
If j\neq 2 and for some x\in X and y_1,y_2\in Y_k we have
x\in I_j(y_1,k)\cap I_j(y_2,k),
then y_1=y_2.
If j\neq 1, then
B(o, 4D^S-2D^k)\subset \bigcup_{y\in Y_k} I_j(y,k).
We have for each y\in Y_k,
B(y,\frac 12 D^k) \subset I_3(y,k)\subset
B(y,4D^k).
Lean code for Lemma1.4.1.3●6 theorems
Associated Lean declarations
-
I1_prop_1[complete]
-
I3_prop_1[complete]
-
I2_prop_2[complete]
-
I3_prop_2[complete]
-
I3_prop_3_1[complete]
-
I3_prop_3_2[complete]
-
I1_prop_1[complete] -
I3_prop_1[complete] -
I2_prop_2[complete] -
I3_prop_2[complete] -
I3_prop_3_1[complete] -
I3_prop_3_2[complete]
-
theoremdefined in Carleson/TileExistence.leancomplete
theorem I1_prop_1.{u_1} {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] {k : ℤ} (hk : -↑(defaultS X) ≤ k) {x : X} {y1 y2 : ↑(Yk X k)} : x ∈ I1 hk y1 ∩ I1 hk y2 → y1 = y2
theorem I1_prop_1.{u_1} {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] {k : ℤ} (hk : -↑(defaultS X) ≤ k) {x : X} {y1 y2 : ↑(Yk X k)} : x ∈ I1 hk y1 ∩ I1 hk y2 → y1 = y2
-
theoremdefined in Carleson/TileExistence.leancomplete
theorem I3_prop_1.{u_1} {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] {k : ℤ} (hk : -↑(defaultS X) ≤ k) {x : X} {y1 y2 : ↑(Yk X k)} : x ∈ I3 hk y1 ∩ I3 hk y2 → y1 = y2
theorem I3_prop_1.{u_1} {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] {k : ℤ} (hk : -↑(defaultS X) ≤ k) {x : X} {y1 y2 : ↑(Yk X k)} : x ∈ I3 hk y1 ∩ I3 hk y2 → y1 = y2
-
theoremdefined in Carleson/TileExistence.leancomplete
theorem I2_prop_2.{u_1} {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] {k : ℤ} (hk : -↑(defaultS X) ≤ k) : Metric.ball (cancelPt X) (4 * ↑(defaultD a) ^ defaultS X - 2 * ↑(defaultD a) ^ k) ⊆ ⋃ y, I2 hk y
theorem I2_prop_2.{u_1} {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] {k : ℤ} (hk : -↑(defaultS X) ≤ k) : Metric.ball (cancelPt X) (4 * ↑(defaultD a) ^ defaultS X - 2 * ↑(defaultD a) ^ k) ⊆ ⋃ y, I2 hk y
-
theoremdefined in Carleson/TileExistence.leancomplete
theorem I3_prop_2.{u_1} {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] {k : ℤ} (hk : -↑(defaultS X) ≤ k) : Metric.ball (cancelPt X) (4 * ↑(defaultD a) ^ defaultS X - 2 * ↑(defaultD a) ^ k) ⊆ ⋃ y, I3 hk y
theorem I3_prop_2.{u_1} {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] {k : ℤ} (hk : -↑(defaultS X) ≤ k) : Metric.ball (cancelPt X) (4 * ↑(defaultD a) ^ defaultS X - 2 * ↑(defaultD a) ^ k) ⊆ ⋃ y, I3 hk y
-
theoremdefined in Carleson/TileExistence.leancomplete
theorem I3_prop_3_1.{u_1} {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] {k : ℤ} (hk : -↑(defaultS X) ≤ k) (y : ↑(Yk X k)) : Metric.ball (↑y) (2⁻¹ * ↑(defaultD a) ^ k) ⊆ I3 hk y
theorem I3_prop_3_1.{u_1} {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] {k : ℤ} (hk : -↑(defaultS X) ≤ k) (y : ↑(Yk X k)) : Metric.ball (↑y) (2⁻¹ * ↑(defaultD a) ^ k) ⊆ I3 hk y
-
theoremdefined in Carleson/TileExistence.leancomplete
theorem I3_prop_3_2.{u_1} {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] {k : ℤ} (hk : -↑(defaultS X) ≤ k) (y : ↑(Yk X k)) : I3 hk y ⊆ Metric.ball (↑y) (4 * ↑(defaultD a) ^ k)
theorem I3_prop_3_2.{u_1} {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] {k : ℤ} (hk : -↑(defaultS X) ≤ k) (y : ↑(Yk X k)) : I3 hk y ⊆ Metric.ball (↑y) (4 * ↑(defaultD a) ^ k)
Proof. We prove these statements simultaneously by induction on the ordered set
of pairs (y,k). Let -S\le k\le S.
We first consider disji for j=1. If k=-S, disjointedness of the sets
I_1(y,-S) follows by definition of I_1 and Y_k. If k>-S, assume
x is in I_1(y_m,k) for m=1,2. Then, for m=1,2, there is
z_m\in Y_{k-1}\cap B(y_m,D^k) with x\in I_3(z_m,k-1). Using disji
inductively for j=3, we conclude z_1=z_2. This implies that the balls
B(y_1, D^k) and B(y_2, D^k) intersect. By construction of Y_k, this
implies y_1=y_2. This proves disji for j=1.
We next consider disji for j=3. Assume x is in I_3(y_m,k) for
m=1,2 and y_m\in Y_k. If x is in X_k, then by definition
definei3, x\in I_1(y_m,k) for m=1,2. As we have already shown disji
for j=1, we conclude y_1=y_2. This completes the proof in case
x\in X_k, and we may assume x is not in X_k. By definition
definei3, x is not in I_3(z,k) for any z with z<y_1 or
z<y_2. Hence, neither y_1<y_2 nor y_2<y_1, and by totality of the
order of Y_k, we have y_1=y_2. This completes the proof of disji for
j=3.
We show unioni for j=2. In case k=-S, this follows from
Lemma 1.4.1.2. Assume k>-S. Let x be a point of
B(o, 4D^S-2D^k). By induction, there is y'\in Y_{k-1} such that
x\in I_3(y',k-1). Using the inductive statement squeezedyadic, we obtain
x\in B(y',4D^{k-1}). As D>4, by applying the triangle inequality with
the points o, x, and y', we obtain that
y'\in B(o, 4D^S-D^k). By Lemma 1.4.1.2, y' is in B(y,2D^k) for
some y\in Y_k. It follows that x\in I_2(y,k). This proves unioni for
j=2.
We show unioni for j=3. Let x\in B(o, 4D^S-2D^k). In case
x\in X_k, then by definition of X_k we have x\in I_1(y,k) for some
y\in Y_k and thus x\in I_3(y,k). We may thus assume x\not\in X_k. As
we have already seen unioni for j=2, there is y\in Y_k such that
x\in I_2(y,k). We may assume this y is minimal with respect to the order
in Y_k. Then x\in I_3(y,k). This proves unioni for j=3.
Next, we show the first inclusion in squeezedyadic. Let
x\in B(y,\frac 12 D^k). As I_1(y,k)\subset I_3(y,k), it suffices to show
x\in I_1(y,k). If k=-S, this follows immediately from the assumption on
x and the definition of I_1. Assume k>-S. By the inductive statement
unioni and D>4, there is a y'\in Y_{k-1} such that
x\in I_3(y',k-1). By the inductive statement squeezedyadic, we conclude
x\in B(y',4D^{k-1}). By the triangle inequality with points x, y,
y', and D\geq8, we have y'\in B(y,D^k). It follows by definition
defineij that I_3(y',k-1)\subset I_1(y,k), and thus x\in I_3(y,k).
This proves the first inclusion in squeezedyadic.
We show the second inclusion in squeezedyadic. Let x\in I_3(y,k). As
I_1(y,k)\subset I_2(y,k) directly from the definition defineij, it
follows by definition definei3 that x\in I_2(y,k). By definition
defineij, there is y'\in Y_{k-1}\cap B(y,2D^k) with
x\in I_3(y',k-1). By induction, x\in B(y', 4D^{k-1}). By the triangle
inequality applied to the points x,y',y and D>4, we conclude
x\in B(y,4D^k). This shows the second inclusion in squeezedyadic and
completes the proof of the lemma.
Let -S\le l\le k\le S and y\in Y_k. We have
I_3(y,k)\subset \bigcup_{y'\in Y_l} I_3(y',l).
Lean code for Lemma1.4.1.4●1 theorem
Associated Lean declarations
-
cover_by_cubes[complete]
-
cover_by_cubes[complete]
-
theoremdefined in Carleson/TileExistence.leancomplete
theorem cover_by_cubes.{u_1} {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] {l : ℤ} (hl : -↑(defaultS X) ≤ l) {k : ℤ} : l ≤ k → ∀ (hk : -↑(defaultS X) ≤ k) (y : ↑(Yk X k)), I3 hk y ⊆ ⋃ yl, I3 hl yl
theorem cover_by_cubes.{u_1} {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] {l : ℤ} (hl : -↑(defaultS X) ≤ l) {k : ℤ} : l ≤ k → ∀ (hk : -↑(defaultS X) ≤ k) (y : ↑(Yk X k)), I3 hk y ⊆ ⋃ yl, I3 hl yl
Proof. Let -S\le l\le k\le S and y\in Y_k. If l=k, the inclusion
3coverdyadic is true from the definition of set union. We may then assume
inductively that k>l and the statement of the lemma is true if k is
replaced by k-1. Let x\in I_3(y,k). By definition definei3,
x\in I_j(y,k) for some j\in \{1,2\}. By defineij,
x\in I_3(w,k-1) for some w\in Y_{k-1}. We conclude 3coverdyadic by
induction.
Let -S\le l\le k\le S and y\in Y_k and y'\in Y_l with
I_3(y',l)\cap I_3(y,k)\neq \emptyset. Then
I_3(y',l)\subset I_3(y,k).
Lean code for Lemma1.4.1.5●1 theorem
Associated Lean declarations
-
dyadic_property[complete]
-
dyadic_property[complete]
-
theoremdefined in Carleson/TileExistence.leancomplete
theorem dyadic_property.{u_1} {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] {l : ℤ} (hl : -↑(defaultS X) ≤ l) {k : ℤ} (hl_k : l ≤ k) (hk : -↑(defaultS X) ≤ k) (y : ↑(Yk X k)) (y' : ↑(Yk X l)) : ¬Disjoint (I3 hl y') (I3 hk y) → I3 hl y' ⊆ I3 hk y
theorem dyadic_property.{u_1} {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] {l : ℤ} (hl : -↑(defaultS X) ≤ l) {k : ℤ} (hl_k : l ≤ k) (hk : -↑(defaultS X) ≤ k) (y : ↑(Yk X k)) (y' : ↑(Yk X l)) : ¬Disjoint (I3 hl y') (I3 hk y) → I3 hl y' ⊆ I3 hk y
Proof. Let l,k,y,y' be as in the lemma. Pick
x\in I_3(y',l)\cap I_3(y,k). Assume first l=k. By disji of
Lemma 1.4.1.3, we conclude y'=y, and thus 3dyadicproperty. Now
assume l<k. By induction, we may assume that the statement of the lemma is
proven for k-1 in place of k. By Lemma 1.4.1.4, there is a
y''\in Y_{k-1} such that x\in I_3(y'',k-1). By induction, we have
I_3(y',l)\subset I_3(y'',k-1). It remains to prove
I_3(y'',k-1)\subset I_3(y,k).
We make a case distinction and assume first x\in X_k. By Definition
definei3, we have x\in I_1(y,k). By Definition defineij, there is a
v\in Y_{k-1}\cap B(y,D^k) with x\in I_3(v,k-1). By disji of
Lemma 1.4.1.3, we have v=y''. By Definition defineij, we then
have I_3(y'',k-1)\subset I_1(y,k). Then the claim follows by Definition
definei3 in the given case. Assume now the case x\notin X_k. By
definei3, we have x\in I_2(y,k). Moreover, for any u<y in Y_k, we
have x\not\in I_3(u,k). Let u<y. By transitivity of the order in Y_k,
we conclude x\not \in I_2(u,k). By defineij and the disjointedness
property of Lemma 1.4.1.3, we have
I_3(y'',k-1)\cap I_2(u,k)= \emptyset. Similarly,
I_3(y'',k-1)\cap I_1(u,k)= \emptyset. Hence
I_3(y'',k-1)\cap I_3(u,k)=\emptyset. As u<y was arbitrary, we conclude
with definei3 the claim in the given case. This completes the proof of the
claim, and thus also 3dyadicproperty.
For -S\le k'\le k\le S and y'\in Y_{k'}, y\in Y_k write
(y',k'|y,k) if I_3(y',k')\subset I_3(y,k) and
\inf_{x\in X\setminus I_3(y,k)}\rho(y',x)<6D^{k'}.
Assume -S\le k''< k'< k\le S and y''\in Y_{k''}, y'\in Y_{k'},
y\in Y_k. Assume there is x\in X such that
x\in I_3(y'',k'')\cap I_3(y',k')\cap I_3(y,k).
If (y'',k''|y,k), then also (y'',k''|y',k') and
(y',k'|y,k).
Lean code for Lemma1.4.1.6●1 theorem
Associated Lean declarations
-
transitive_boundary[complete]
-
transitive_boundary[complete]
-
theoremdefined in Carleson/TileExistence.leancomplete
theorem transitive_boundary.{u_1} {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] {k1 k2 k3 : ℤ} (hk1 : -↑(defaultS X) ≤ k1) (hk2 : -↑(defaultS X) ≤ k2) (hk3 : -↑(defaultS X) ≤ k3) (hk1_2 : k1 ≤ k2) (hk2_3 : k2 ≤ k3) (y1 : ↑(Yk X k1)) (y2 : ↑(Yk X k2)) (y3 : ↑(Yk X k3)) (x : X) (hx : x ∈ I3 hk1 y1 ∩ I3 hk2 y2 ∩ I3 hk3 y3) : ClosenessProperty hk1 hk3 y1 y3 → ClosenessProperty hk1 hk2 y1 y2 ∧ ClosenessProperty hk2 hk3 y2 y3
theorem transitive_boundary.{u_1} {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] {k1 k2 k3 : ℤ} (hk1 : -↑(defaultS X) ≤ k1) (hk2 : -↑(defaultS X) ≤ k2) (hk3 : -↑(defaultS X) ≤ k3) (hk1_2 : k1 ≤ k2) (hk2_3 : k2 ≤ k3) (y1 : ↑(Yk X k1)) (y2 : ↑(Yk X k2)) (y3 : ↑(Yk X k3)) (x : X) (hx : x ∈ I3 hk1 y1 ∩ I3 hk2 y2 ∩ I3 hk3 y3) : ClosenessProperty hk1 hk3 y1 y3 → ClosenessProperty hk1 hk2 y1 y2 ∧ ClosenessProperty hk2 hk3 y2 y3
Proof. As x\in I_3(y'',k'')\cap I_3(y',k') and k''< k', we have by
Lemma 1.4.1.5 that I_3(y'',k'')\subset I_3(y',k'). Similarly,
I_3(y',k')\subset I_3(y,k). Pick x'\in X\setminus I_3(y,k) such that
\rho(y'',x')< 6D^{k''}, which exists as (y'',k''|y,k). As
x'\in X\setminus I_3(y',k') as well, we conclude
(y'',k''| y',k'). By the triangle inequality, we have
\rho(y',x')\le \rho(y',x)+\rho(x,y'')+\rho(y'',x').
Using the choice of x and squeezedyadic as well as the choice of x',
we estimate this by
< 4D^{k'}+4D^{k''}+6D^{k''}\le 6D^{k'},
where we have used D>5 and k''<k'. We conclude (y',k'|y,k).
Let K = 2^{4a+1}. For each -S+K\le k\le S and y\in Y_k we have
\sum_{z\in Y_{k-K}: (z,k-K|y,k)}\mu(I_3(z,k-K)) \le \frac 12 \mu(I_3(y,k)).
Lean code for Lemma1.4.1.7●1 theorem
Associated Lean declarations
-
_root_.small_boundary[complete]
-
_root_.small_boundary[complete]
-
theoremdefined in Carleson/TileExistence.leancomplete
theorem small_boundary.{u_1} {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] (k : ℤ) (hk : -↑(defaultS X) ≤ k) (hk_mK : -↑(defaultS X) ≤ k - ↑const_K) (y : ↑(Yk X k)) : ∑' (z : ↑(Yk X (k - ↑const_K))), ∑ᶠ (_ : ClosenessProperty hk_mK hk z y), MeasureTheory.volume (I3 hk_mK z) ≤ 2⁻¹ * MeasureTheory.volume (I3 hk y)
theorem small_boundary.{u_1} {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] (k : ℤ) (hk : -↑(defaultS X) ≤ k) (hk_mK : -↑(defaultS X) ≤ k - ↑const_K) (y : ↑(Yk X k)) : ∑' (z : ↑(Yk X (k - ↑const_K))), ∑ᶠ (_ : ClosenessProperty hk_mK hk z y), MeasureTheory.volume (I3 hk_mK z) ≤ 2⁻¹ * MeasureTheory.volume (I3 hk y)
Proof. Let K be as in the lemma. Let -S+K\le k\le S and y\in Y_k.
Pick k' so that k-K\le k'\le k. For each y''\in Y_{k-K} with
(y'',k-K| y,k), by Lemma 1.4.1.4 and Lemma 1.4.1.5, there is a
unique y'\in Y_{k'} such that
I_3(y'',k-K)\subset I_3(y',k')\subset I_3(y,k).
Using Lemma 1.4.1.6, (y',k'|y,k). We conclude using the
disjointedness property of Lemma 1.4.1.3 that
\sum_{y'': (y'',k-K|y,k)}\mu(I_3(y'',k-K))
\le
\sum_{y': (y',k'|y,k)}
\mu(I_3(y',k')) .
Adding over k-K<k'\le k, and using
\mu(I_3(y',k'))\le 2^{4a} \mu(B(y', \frac 14 D^{k'})) from doublingx and
squeezedyadic gives
K\sum_{y'': (y'',k-K|y,k)}
\mu(I_3(y'',k-K))
\le 2^{4a} \sum_{k-K<k'\le k}
\left[ \sum_{y': (y',k'|y,k)}
\mu(B(y', \frac 14 D^{k'}))\right].
Each ball B(y', \frac 14 D^{k'}) occurring here is contained in
I_3(y',k') by squeezedyadic and in turn contained in I_3(y,k). Assume
for the moment all these balls are pairwise disjoint. Then by additivity of
the measure,
K\sum_{y'': (y'',k-K|y,k)}
\mu(I_3(y'',k-K))
\le 2^{4a}
\mu(I_3(y,k)),
which by K=2^{4a+1} implies new-small-boundary. It thus remains to prove
that the balls occurring in the previous sum are pairwise disjoint. Let
(u,l) and (u',l') be two parameter pairs occurring in the sum and let
B(u, \frac 14 D^l) and B({u'}, \frac 14 D^{l'}) be the corresponding
balls. If l=l', then the balls are equal or disjoint by squeezedyadic and
disji of Lemma 1.4.1.3. Assume then without loss of generality that
l'<l. Towards a contradiction, assume that
B(u, \frac 14 D^l)\cap B({u'}, \frac 14 D^{l'})\neq \emptyset.
As (u',l'|y,k), there is a point x in X\setminus I_3(y,k) with
\rho(x,u')<6D^{l'}. Using D>25, we conclude from the triangle inequality
and the assumed intersection that x\in B(u,\frac 12D^l). However,
B(u,\frac 12 D^l)\subset I_3(u,l), and I_3(u,l)\subset I_3(y,k), a
contradiction to x\not\in I_3(y,k). This proves the lemma.
Let K = 2^{4a+1} and let n\ge 0 be an integer. Then for each
-S+nK\le k\le S we have
\sum_{y'\in Y_{k-nK}: (y',k-nK|y,k)}\mu(I_3(y',k-nK)) \le 2^{-n} \mu(I_3(y,k)).
Lean code for Lemma1.4.1.8●1 theorem
Associated Lean declarations
-
smaller_boundary[complete]
-
smaller_boundary[complete]
-
theoremdefined in Carleson/TileExistence.leancomplete
theorem smaller_boundary.{u_1} {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] (n : ℕ) {k : ℤ} (hk : -↑(defaultS X) ≤ k) (hk_mnK : -↑(defaultS X) ≤ k - ↑n * ↑const_K) (y : ↑(Yk X k)) : ∑' (y' : ↑(Yk X (k - ↑n * ↑const_K))), ∑ᶠ (_ : ClosenessProperty hk_mnK hk y' y), MeasureTheory.volume (I3 hk_mnK y') ≤ 2⁻¹ ^ n * MeasureTheory.volume (I3 hk y)
theorem smaller_boundary.{u_1} {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] (n : ℕ) {k : ℤ} (hk : -↑(defaultS X) ≤ k) (hk_mnK : -↑(defaultS X) ≤ k - ↑n * ↑const_K) (y : ↑(Yk X k)) : ∑' (y' : ↑(Yk X (k - ↑n * ↑const_K))), ∑ᶠ (_ : ClosenessProperty hk_mnK hk y' y), MeasureTheory.volume (I3 hk_mnK y') ≤ 2⁻¹ ^ n * MeasureTheory.volume (I3 hk y)
Proof. We prove this by induction on n. If n=0, both sides of
very-new-small are equal to \mu(I_3(y,k)) by disji. If n=1, this
follows from Lemma 1.4.1.7.
Assume n>1 and very-new-small has been proven for n-1. We write
very-new-small
\sum_{y''\in Y_{k-nK}: (y'',k-nK|y,k)}\mu(I_3(y'',k-nK))
= \sum_{y'\in Y_{k-K}:(y',k-K|y,k)} \left[ \sum_{y''\in Y_{k-nK}: (y'',k-nK|y',k-K)}\mu(I_3(y'',k-nK)) \right]
Applying the induction hypothesis, this is bounded by
= \sum_{y'\in Y_{k-K}:(y',k-K|y,k)} 2^{1-n}\mu(I_3(y',k-K))
Applying new-small-boundary gives very-new-small, and proves the lemma.
For each -S\le k\le S and y\in Y_k and 0<t<1 with
tD^k\ge D^{-S} we have
\mu(\{x \in I_3(y,k) \ : \ \rho(x, X \setminus I_3(y,k)) \leq t D^{k}\}) \le 2 t^\kappa \mu(I_3(y,k)).
Lean code for Lemma1.4.1.9●1 theorem
Associated Lean declarations
-
boundary_measure[complete]
-
boundary_measure[complete]
-
theoremdefined in Carleson/TileExistence.leancomplete
theorem boundary_measure.{u_1} {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] {k : ℤ} (hk : -↑(defaultS X) ≤ k) (y : ↑(Yk X k)) {t : NNReal} (ht : t ∈ Set.Ioo 0 1) (htD : ↑(defaultD a) ^ (-↑(defaultS X)) ≤ ↑t * ↑(defaultD a) ^ k) : MeasureTheory.volume {x | x ∈ I3 hk y ∧ Metric.infEDist x (I3 hk y)ᶜ ≤ ↑t * ↑(defaultD a) ^ k} ≤ 2 * ↑t ^ defaultκ a * MeasureTheory.volume (I3 hk y)
theorem boundary_measure.{u_1} {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] {k : ℤ} (hk : -↑(defaultS X) ≤ k) (y : ↑(Yk X k)) {t : NNReal} (ht : t ∈ Set.Ioo 0 1) (htD : ↑(defaultD a) ^ (-↑(defaultS X)) ≤ ↑t * ↑(defaultD a) ^ k) : MeasureTheory.volume {x | x ∈ I3 hk y ∧ Metric.infEDist x (I3 hk y)ᶜ ≤ ↑t * ↑(defaultD a) ^ k} ≤ 2 * ↑t ^ defaultκ a * MeasureTheory.volume (I3 hk y)
Proof. Let x\in I_3(y,k) with
\rho(x, X \setminus I_3(y,k)) \leq t D^{k}. Let
K = 2^{4a+1} as in Lemma 1.4.1.8. Let n be the largest integer such
that D^{nK} \le \frac{1}{t}, so that tD^k \le D^{k-nK} and
D^{nK} > \frac{1}{tD^K}.
Let k' = k - nK, by the assumption tD^k \ge D^{-S}, we have
k' \ge -S. By 3coverdyadic, there exists y' \in Y_{k'} with
x \in I_3(y',k'). By the squeezing property squeezedyadic and the
assumption on x, we have
\rho(y', X \setminus I_3(y,k)) \le \rho(x,y') + \rho(x, X \setminus I_3(y,k)) \le 4 D^{k'} + t D^{k}.
By the assumption on n and the definition of k', this is
\le 4D^{k'} + D^{k - nK} < 6D^{k'}.
Together with 3dyadicproperty thus (y',k'|y,k). We have shown that
\{x \in I_3(y,k) \ : \ \rho(x, X \setminus I_3(y,k)) \leq t D^{k}\}
\subset \bigcup_{y'\in Y_{k-nK}: (y',k-nK|y,k)}I_3(y',k-nK).
Using monotonicity and additivity of the measure and Lemma 1.4.1.8, we
obtain
\mu(\{x \in I_3(y,k) \ : \ \rho(x, X \setminus I_3(y,k)) \leq t D^{k}\}) \le 2^{-n} \mu(I_3(y,k)).
By eq-n-size and the definition defineD of D, this is bounded by
2 t^{1/(100a^2 K)} \mu(I_3(y,k)),
which completes the proof by the definition definekappa of \kappa.
Let \tilde{\mathcal{D}} be the set of all I_3(y,k) with k\in [-S,S]
and y\in Y_k. Define
s(I_3(y,k)):=k
c(I_3(y,k)):=y.
We define \mathcal{D} to be the set of all I \in \tilde{\mathcal{D}}
such that I \subset I_3(o, S).
Proof of Lemma 1.4.1. We first show that
(\tilde{\mathcal{D}},c,s) satisfies properties coverdyadic,
dyadicproperty, eq-vol-sp-cube and eq-small-boundary. Property
eq-vol-sp-cube follows from squeezedyadic, while eq-small-boundary
follows from Lemma 1.4.1.9.
Let x\in B(o, D^S). We show properties coverdyadic and dyadicproperty
for (\tilde{\mathcal{D}},c,s) and x. We first show coverdyadic for
(\tilde{\mathcal{D}},c,s) by contradiction. Then there is an I
violating the conclusion of coverdyadic. Pick such I=I_3(y,l) such that
l is minimal. By assumption, we have -S\le k<l; in particular
-S<l. By definition, I_3(y, l) is contained in I_1(y, l)\cup I_2(y,
l), which is contained in the union of I_3(y',l-1) with
y'\in Y_{l-1}. By minimality of l, each such I_3(y',l-1) is
contained in the union of all I_3(z,k) with z\in Y_k. This proves
coverdyadic.
We now show dyadicproperty for (\tilde{\mathcal{D}},c,s). Assume to get a
contradiction that there are non-disjoint I, J\in \tilde{\mathcal{D}} with
s(I)\le s(J) and I \not \subset J. We may assume the existence of such
I and J with minimal s(J)-s(I). Let k=s(I). Assume first
s(J)=k. Let I=I_3(y_1,k) and J=I_3(y_2,k) with
y_1,y_2\in Y_k. If y_1=y_2, then I=J, a contradiction to
I\not \subset J. If y_1\neq y_2, then I\cap J=\emptyset by disji,
a contradiction to the non-disjointedness of I,J. Assume now
s(J)>k. Choose y\in I\cap J. By property coverdyadic, there is
K\in \tilde{\mathcal{D}} with s(K)=s(J)-1 and y\in K. By construction
of J, and pairwise disjointedness of all I_3(w,s(J)-1) that we have
already seen, we have K\subset J. By minimality of s(J), we have
I\subset K. This proves I\subset J and thus dyadicproperty.
Now note that properties dyadicproperty, eq-vol-sp-cube and
eq-small-boundary immediately carry over to (\mathcal{D},c, s) by
restriction. subsetmaxcube is true for (\mathcal{D}, c, s) by definition,
and coverdyadic follows from coverdyadic and dyadicproperty for
(\tilde{\mathcal{D}}, c, s).
1.4.2. Proof of Tile Structure Lemma
Choose a grid structure (\mathcal{D}, c, s) with Lemma 1.4.1. Let
I \in \mathcal{D}. Suppose that
\mathcal{Z} \subset \tQ(X)
is such that for any \mfa, \mfb \in \mathcal{Z} with \mfa\ne \mfb we
have
B_{I^\circ}(\mfa, 0.3) \cap B_{I^\circ}(\mfb, 0.3) \cap \tQ(X) = \emptyset.
Since \tQ(X) is finite, there exists a set \mathcal{Z} satisfying both
conditions of maximal cardinality among all such sets. We pick for each
I \in \mathcal{D} such a set \mathcal{Z}(I).
For each I \in \mathcal{D}, we have
\tQ(X) \subset \bigcup_{z \in \mathcal{Z}(I)} B_{I^\circ}(z, 0.7).
Lean code for Lemma1.4.2.1●1 theorem
Associated Lean declarations
-
frequency_ball_cover[complete]
-
frequency_ball_cover[complete]
-
theoremdefined in Carleson/TileExistence.leancomplete
theorem frequency_ball_cover.{u_1} {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] [GridStructure X (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {I : Grid X} : ↑Q.range ⊆ ⋃ z ∈ 𝓩 I, ball_{c I, ↑(defaultD a) ^ s I / 4} z C4_2_1
theorem frequency_ball_cover.{u_1} {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] [GridStructure X (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {I : Grid X} : ↑Q.range ⊆ ⋃ z ∈ 𝓩 I, ball_{c I, ↑(defaultD a) ^ s I / 4} z C4_2_1
Equation (4.2.3), Lemma 4.2.1
Proof. Let \mfb \in \bigcup_{\mfa \in \tQ(X)} B_{I^\circ}(\mfa, 1). By
maximality of \mathcal{Z}(I), there must be a point z \in \mathcal{Z}(I)
such that B_{I^\circ}(z, 0.3) \cap B_{I^\circ}(\mfb, 0.3) \ne \emptyset.
Else, \mathcal{Z}(I) \cup \{\mfb\} would be a set of larger cardinality than
\mathcal{Z}(I) satisfying eq-tile-Z and eq-tile-disjoint-Z. Fix such a
z, and fix a point
z_1 \in B_{I^\circ}(z, 0.3) \cap B_{I^\circ}(\mfb, 0.3). By the triangle
inequality, we deduce that
d_{I^\circ}(z,\mfb) \le d_{I^\circ}(z,z_1) + d_{I^\circ}(\mfb, z_1) < 0.3 + 0.3 = 0.6,
and hence \mfb \in B_{I^\circ}(z, 0.7).
We define
\fP = \{(I, z) \ : \ I \in \mathcal{D}, z \in \mathcal{Z}(I)\},
\scI((I, z)) = I\qquad \text{and} \qquad \fcc((I, z)) = z.
We further set
\ps(\fp) = s(\scI(\fp)),\qquad \qquad \pc(\fp) = c(\scI(\fp)).
Then tilecenter, tilescale hold by definition.
It remains to construct the map \Omega, and verify properties
eq-dis-freq-cover, eq-freq-dyadic and eq-freq-comp-ball. We first
construct an auxiliary map \Omega_1. For each I \in \mathcal{D}, we pick
an enumeration of the finite set \mathcal{Z}(I)
\mathcal{Z}(I) = \{z_1, \dotsc, z_M\}.
We define \Omega_1:\fP \mapsto \mathcal{P}(\Mf) as follows. Set
\Omega_1((I, z_1)) = B_{I^\circ}(z_1, 0.7) \setminus \bigcup_{z \in \mathcal{Z}(I)\setminus \{z_1\}} B_{I^\circ}(z, 0.3)
and then define iteratively
\Omega_1((I, z_k)) = B_{I^\circ}(z_k, 0.7) \setminus \bigcup_{z \in \mathcal{Z}(I) \setminus \{z_k\}} B_{I^\circ}(z, 0.3) \setminus \bigcup_{i=1}^{k-1} \Omega_1((I, z_i)).
-
Construction.disjoint_frequency_cubes[complete]
For each I \in \mathcal{D}, and \fp_1, \fp_2\in \fP(I), if
\Omega_1(\fp_1)\cap \Omega_1(\fp_2)\neq \emptyset
then \fp_1=\fp_2.
Lean code for Lemma1.4.2.2●1 theorem
Associated Lean declarations
-
Construction.disjoint_frequency_cubes[complete]
-
Construction.disjoint_frequency_cubes[complete]
-
theoremdefined in Carleson/TileExistence.leancomplete
theorem Construction.disjoint_frequency_cubes.{u_1} {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] [GridStructure X (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {I : Grid X} {f g : ↥(𝓩 I)} (h : (Construction.Ω₁ ⟨I, f⟩ ∩ Construction.Ω₁ ⟨I, g⟩).Nonempty) : f = g
theorem Construction.disjoint_frequency_cubes.{u_1} {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] [GridStructure X (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {I : Grid X} {f g : ↥(𝓩 I)} (h : (Construction.Ω₁ ⟨I, f⟩ ∩ Construction.Ω₁ ⟨I, g⟩).Nonempty) : f = g
Lemma 4.2.2
Proof. By the definition of the map \scI, we have
\fP(I) = \{(I, z) \, : \, z \in \mathcal{Z}(I)\}.
By eq-def-omega1, the set \Omega_1((I, z_k)) is disjoint from each
\Omega_1((I, z_i)) with i < k. Thus the sets \Omega_1(\fp),
\fp \in \fP(I) are pairwise disjoint.
-
Construction.iUnion_ball_subset_iUnion_Ω₁[complete] -
Construction.ball_subset_Ω₁[complete] -
Construction.Ω₁_subset_ball[complete]
For each I \in \mathcal{D}, it holds that
\bigcup_{z \in \mathcal{Z}(I)} B_{I^\circ}(z, 0.7)\subset \bigcup_{\fp \in \fP(I)} \Omega_1(\fp).
For every \fp \in \fP, it holds that
B_{\fp}(\fcc(\fp), 0.3) \subset \Omega_1(\fp) \subset B_{\fp}(\fcc(\fp), 0.7).
Lean code for Lemma1.4.2.3●3 theorems
Associated Lean declarations
-
Construction.iUnion_ball_subset_iUnion_Ω₁[complete]
-
Construction.ball_subset_Ω₁[complete]
-
Construction.Ω₁_subset_ball[complete]
-
Construction.iUnion_ball_subset_iUnion_Ω₁[complete] -
Construction.ball_subset_Ω₁[complete] -
Construction.Ω₁_subset_ball[complete]
-
theoremdefined in Carleson/TileExistence.leancomplete
theorem Construction.iUnion_ball_subset_iUnion_Ω₁.{u_1} {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] [GridStructure X (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {I : Grid X} : ⋃ z ∈ 𝓩 I, ball_{c I, ↑(defaultD a) ^ s I / 4} z C4_2_1 ⊆ ⋃ f, Construction.Ω₁ ⟨I, f⟩
theorem Construction.iUnion_ball_subset_iUnion_Ω₁.{u_1} {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] [GridStructure X (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {I : Grid X} : ⋃ z ∈ 𝓩 I, ball_{c I, ↑(defaultD a) ^ s I / 4} z C4_2_1 ⊆ ⋃ f, Construction.Ω₁ ⟨I, f⟩
Equation (4.2.5)
-
theoremdefined in Carleson/TileExistence.leancomplete
theorem Construction.ball_subset_Ω₁.{u_1} {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] [GridStructure X (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] (p : 𝔓 X) : ball_{𝔠 p, ↑(defaultD a) ^ 𝔰 p / 4} (𝒬 p) C𝓩 ⊆ Construction.Ω₁ p
theorem Construction.ball_subset_Ω₁.{u_1} {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] [GridStructure X (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] (p : 𝔓 X) : ball_{𝔠 p, ↑(defaultD a) ^ 𝔰 p / 4} (𝒬 p) C𝓩 ⊆ Construction.Ω₁ p
Equation (4.2.6), first inclusion
-
theoremdefined in Carleson/TileExistence.leancomplete
theorem Construction.Ω₁_subset_ball.{u_1} {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] [GridStructure X (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] (p : 𝔓 X) : Construction.Ω₁ p ⊆ ball_{𝔠 p, ↑(defaultD a) ^ 𝔰 p / 4} (𝒬 p) C4_2_1
theorem Construction.Ω₁_subset_ball.{u_1} {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] [GridStructure X (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] (p : 𝔓 X) : Construction.Ω₁ p ⊆ ball_{𝔠 p, ↑(defaultD a) ^ 𝔰 p / 4} (𝒬 p) C4_2_1
Equation (4.2.6), second inclusion
Proof. For eq-omega1-incl let \fp = (I, z). The second inclusion in
eq-omega1-incl then follows from eq-def-omega1 and the equality
B_{\fp}(\fcc(\fp), 0.7) = B_{I^\circ}(z, 0.7), which is true by definition.
For the first inclusion in eq-omega1-incl let
\mfa \in B_{\fp}(\fcc(\fp),0.3). Let k be such that z = z_k in the
enumeration chosen above. It follows immediately from eq-def-omega1 and
eq-tile-disjoint-Z that \mfa \notin \Omega_1((I, z_i)) for all
i < k. Thus, again from eq-def-omega1, we have
\mfa \in \Omega_1((I,z_k)).
To show eq-omega1-cover let
\mfa \in \bigcup_{z \in \mathcal{Z}(I)} B_{I^\circ}(z,0.7). If there exists
z \in \mathcal{Z}(I) with \mfa \in B_{I^\circ}(z,0.3), then
z \in \Omega_1((I, z)) \subset \bigcup_{\fp \in \fP(I)} \Omega_1(\fp)
by the first inclusion in eq-omega1-incl.
Now suppose that there exists no z \in \mathcal{Z}(I) with
\mfa \in B_{I^\circ}(z, 0.3). Let k be minimal such that
\mfa \in B_{I^\circ}(z_k, 0.7). Since
\Omega_1((I, z_i)) \subset B_{I^\circ}(z_i, 0.7) for each i by
eq-def-omega1, we have that \mfa \notin \Omega_1((I, z_i)) for all
i < k. Hence \mfa \in \Omega_1((I, z_k)), again by eq-def-omega1.
Now we are ready to define the function \Omega. We define for all
\fp \in \fP(I_0)
\fc(\fp) = \Omega_1(\fp).
For all other cubes I \in \mathcal{D}, I \ne I_0, there exists, by
dyadicproperty and subsetmaxcube, J \in \mathcal{D} with
I \subset J and I \ne J. On such I we define \Omega by recursion.
We can pick an inclusion minimal J \in \mathcal{D} among the finitely many
cubes such that I \subset J and I \ne J. This J is unique. Suppose
that J' is another inclusion minimal cube with I \subset J' and
I \ne J'. Without loss of generality, we have that s(J) \le s(J'). By
dyadicproperty, it follows that J \subset J'. Since J' is minimal with
respect to inclusion, it follows that J = J'. Then we define
\fc(\fp) = \bigcup_{z \in \mathcal{Z}(J) \cap \Omega_1(\fp)} \Omega((J, z)) \cup B_{\fp}(\fcc(\fp),0.2).
We now verify that (\fP,\scI,\fc,\fcc,\pc,\ps) forms a tile structure.
Proof of Lemma 1.4.2. First, we prove eq-freq-comp-ball. If
I =I_0, then eq-freq-comp-ball holds for all \fp \in \fP(I) by
eq-max-omega and eq-omega1-incl. Now suppose that I is not maximal in
\mathcal{D} with respect to set inclusion. Then we may assume by induction
that for all J \in \mathcal{D} with I \subset J and all
\fp' \in \fP(J), eq-freq-comp-ball holds. Let J be the unique minimal
cube in \mathcal{D} with I \subsetneq J.
Suppose that \mfa \in \Omega(\fp). If
\mfa\in B_{\fp}(\mathcal{Q}(\fp), 0.2), then since
B_{\fp}(\mathcal{Q}(\fp), 0.2)\subset B_{\fp}(\mathcal{Q}(\fp), 1), we
conclude that \mfa\in B_{\fp}(\mathcal{Q}(\fp), 0.7). If not, by
eq-it-omega, there exists z \in \mathcal{Z}(J) \cap \Omega_1(\fp) with
\mfa \in \Omega(J,z). Using the triangle inequality,
Lemma 1.2.1.2 and eq-freq-comp-ball, we obtain
d_{\fp'}(\fcc(\fp'),z) \le d_{\fp'}(\fcc(\fp'), \mfa) + d_{\fp'}(z, \mfa) \le 0.2 + 2^{-95a} \cdot 1 < 0.3.
Thus z \in \Omega_1(\fp') by eq-omega1-incl. By
Lemma 1.4.2.2, it follows that \fp = \fp'. This shows the
second inclusion in eq-freq-comp-ball. The first inclusion is immediate from
eq-it-omega.
Next, we show eq-dis-freq-cover. Let I \in \mathcal{D}. If
I = I_0, then disjointedness of the sets \fc(\fp) for
\fp \in \fP(I) follows from the definition eq-max-omega and
Lemma 1.4.2.2. To obtain the inclusion in eq-dis-freq-cover one
combines the inclusions eq-tile-cover and eq-omega1-cover of
Lemma 1.4.2.3 with eq-max-omega.
Now we turn to the case where there exists J \in \mathcal{D} with
I \subset J and I\ne J. In this case we use induction: It suffices to
show eq-dis-freq-cover under the assumption that it holds for all cubes
J \in \mathcal{D} with I \subset J. As shown before definition
eq-it-omega, we may choose the unique inclusion minimal such J. To show
disjointedness of the sets \fc(\fp), \fp \in \fP(I) we pick two tiles
\fp, \fp' \in \fP(I) and \mfa \in \fc(\fp) \cap \fc(\fp'). Then we are
by eq-it-omega in one of four cases. In the case where both come from
elements z,z' \in \mathcal{Z}(J), the induction hypothesis gives z=z'
and then Lemma 1.4.2.2 gives \fp = \fp'. In the mixed case
where one side comes from \Omega(J,z) and the other from
B_{\fp'}(\fcc(\fp'), 0.2), the same estimate as above gives
z \in \Omega_1(\fp'), hence Lemma 1.4.2.2 gives
\fp=\fp'. The symmetric mixed case is identical after swapping the roles.
If both points lie in the small balls
B_{\fp}(\fcc(\fp), 0.2) \cap B_{\fp'}(\fcc(\fp'), 0.2), then
\fp=\fp' because these small balls are pairwise disjoint by
eq-omega1-incl and Lemma 1.4.2.2.
To show the inclusion in eq-dis-freq-cover, let \mfa \in \tQ(X). By the
induction hypothesis, there exists \fp \in \fP(J) such that
\mfa \in \Omega(\fp). By definition of the set \fP, we have
\fp = (J, z) for some z \in \mathcal{Z}(J). Thus, by eq-tile-cover,
there exists z' \in \mathcal{Z}(I) with z \in B_{I^\circ}(z', 0.7). Then
by Lemma 1.4.2.3 there exists \fp' \in \fP(I) with
z \in \mathcal{Z}(J) \cap \Omega_1(\fp'). Consequently, by eq-it-omega,
\mfa \in \fc(\fp'). This completes the proof of eq-dis-freq-cover.
Finally, we show eq-freq-dyadic. Let \fp, \fq \in \fP with
\scI(\fp) \subset \scI(\fq) and
\fc(\fp) \cap \fc(\fq) \ne \emptyset. If we have
\ps(\fp) \ge \ps(\fq), then it follows from dyadicproperty that
I = J, thus \fp, \fq \in \fP(I). By eq-dis-freq-cover we have then
either \fc(\fp) \cap \fc(\fq) = \emptyset or
\fc(\fp) = \fc(\fq). By the assumption in eq-freq-dyadic we have
\fc(\fp) \cap \fc(\fq) \ne \emptyset, so we must have
\fc(\fp) = \fc(\fq) and in particular \fc(\fq) \subset \fc(\fp).
So it remains to show eq-freq-dyadic under the additional assumption that
\ps(\fq) > \ps(\fp). In this case, we argue by induction on
\ps(\fq)-\ps(\fp). By coverdyadic, there exists a cube J \in \mathcal{D}
with s(J) = \ps(\fq) - 1 and J \cap\scI(\fp) \ne \emptyset. We pick one
such J. By dyadicproperty, we have
\scI(\fp) \subset J \subset \scI(\fq).
Thus, by eq-tile-cover, there exists z' \in \mathcal{Z}(J) with
\fcc(\fq) \in B_{J^\circ}(z', 0.7). Then by Lemma 1.4.2.3 there
exists \fq' \in \fP(J) with \fcc(\fq) \in\Omega_1(\fq'). By eq-it-omega,
it follows that \Omega(\fq) \subset \Omega(\fq'). Note that then
\scI(\fp) \subset \scI(\fq') and
\fc(\fp) \cap \fc(\fq') \ne \emptyset and
\ps(\fq') - \ps(\fp) = \ps(\fq) - \ps(\fp) - 1. Thus, we have by the
induction hypothesis that \Omega(\fq') \subset \Omega(\fp). This completes
the proof.