Dependency graph

Legend

Boxes: definitions
Ellipses: theorems and lemmas
Blue border: the statement of this result is ready to be formalized; all prerequisites are done
Orange border: the statement of this result is not ready to be formalized; the blueprint needs more work
Blue background: the proof of this result is ready to be formalized; all prerequisites are done
Green border: the statement of this result is formalized
Green background: the proof of this result is formalized
Dark green background: the proof of this result and all its ancestors are formalized

Lemma 7.4.1adjoint tile support

For each $p \in P$ , we have

T_{p}^{*} g = 1_{B (c (p), 5 D^{s (p)})} T_{p}^{*} 1_{I (p)} g .

For each $u \in U$ and each $p \in T (u)$ , we have

T_{p}^{*} g = 1_{I (u)} T_{p}^{*} 1_{I (u)} g .

LaTeX

Lean

TileStructure.Forest.adjoint_tile_support1
TileStructure.Forest.adjoint_tile_support2

Lemma 7.4.3adjoint tree control

We have for all $u \in U$ and $g$ with $| g | \leq 1_{G}$

‖ S_{2, u} g ‖_{2} \leq 2^{156 a^{3}} ‖ g ‖_{2} .

LaTeX Lean

Lemma 7.4.2adjoint tree estimate

For all $g$ with $| g | \leq 1_{G}$ , we have that

{‖ \sum_{p \in T (u)} T_{p}^{*} g ‖}_{2} \leq 2^{155 a^{3}} {dens}_{1} (T (u))^{1 / 2} ‖ g ‖_{2} .

LaTeX Lean

Lemma 5.5.1antichain decomposition

We have that

\begin{aligned} P_{2} \cap P_{G ∖ G^{'}} \\ = ⋃_{k \geq 0} ⋃_{n \geq k} L_{0} (k, n) \cap P_{G ∖ G^{'}} \\ \cup ⋃_{k \geq 0} ⋃_{n \geq k} ⋃_{0 \leq j \leq 2 n + 3} L_{2} (k, n, j) \cap P_{G ∖ G^{'}} \\ \cup ⋃_{k \geq 0} ⋃_{n \geq k} ⋃_{0 \leq j \leq 2 n + 3} ⋃_{0 \leq l \leq Z (n + 1)} L_{1} (k, n, j, l) \cap P_{G ∖ G^{'}} \\ \cup ⋃_{k \geq 0} ⋃_{n \geq k} ⋃_{0 \leq j \leq 2 n + 3} ⋃_{0 \leq l \leq Z (n + 1)} L_{3} (k, n, j, l) \cap P_{G ∖ G^{'}} . \end{aligned}

LaTeX Lean

Proposition 2.0.3antichain operator

For any antichain $A$ and for all $f : X \to C$ with $| f | \leq 1_{F}$ and all $g : X \to C$ with $| g | \leq 1_{G}$

| \int \overset{―}{g (x)} \sum_{p \in A} T_{p} f (x) d μ (x) |

2.0.30

\leq \frac{2^{150 a^{3}}}{q - 1} {dens}_{1} (A)^{\frac{q - 1}{8 a^{4}}} {dens}_{2} (A)^{\frac{1}{q} - \frac{1}{2}} ‖ f ‖_{2} ‖ g ‖_{2} .

2.0.31

LaTeX Lean

Lemma 6.1.6antichain tile count

Set $p := 4 a^{4}$ and let $p^{'}$ be the dual exponent of $p$ , that is $1 / p + 1 / p^{'} = 1$ . For every $ϑ \in Θ$ and every subset $A^{'}$ of $A$ we have

‖ \sum_{p \in A^{'}} (1 + d_{p} (Q (p), ϑ))^{- 1 / (2 a^{2} + a^{3})} 1_{E (p)} 1_{G} ‖_{p}

6.1.46

\leq 2^{104 a} {dens}_{1} (A)^{\frac{1}{p}} μ {(\cup_{p \in A^{'}} I_{p})}^{\frac{1}{p}} .

6.1.47

LaTeX Lean

Lemma 10.2.4Ball covering

Given an open set $O \neq X$ , there exists a countable family of balls $B_{j} = B (x_{j}, r_{j})$ such that

B_{j} \cap B_{j^{'}} = \emptyset for j \neq j^{'}

10.2.5

and for $B_{j}^{*} := B (x_{j}, 3 r_{j})$ ,

⋃_{j} B_{j}^{*} = O

10.2.6

and for $B_{j}^{* *} := B (x_{j}, 7 r_{j})$ ,

B_{j}^{* *} \cap (X ∖ O) \neq \emptyset for all j

10.2.7

and we have the bounded intersection property that each $x \in O$ is contained in at most $2^{6 a}$ of the $B_{j}^{*}$ .

LaTeX Lean

Lemma 2.1.1ball metric entropy

Let $B^{'} \subset X$ be a ball. Let $r > 0$ , $ϑ \in Θ$ and $k \in N$ . Suppose that $Z \subset B_{B^{'}} (ϑ, r 2^{k})$ satisfies that ${B_{B^{'}} (z, r) ∣ z \in Z}$ is a collection of pairwise disjoint sets. Then

| Z | \leq 2^{k a} .

LaTeX Lean

Lemma 4.1.3basic grid structure

For each $- S \leq k \leq S$ and $1 \leq j \leq 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),

4.1.13

then $y_{1} = y_{2}$ .

If $j \neq 1$ , then

B (o, 4 D^{S} - 2 D^{k}) \subset ⋃_{y \in Y_{k}} I_{j} (y, k) .

4.1.14

We have for each $y \in Y_{k}$ ,

B (y, \frac{1}{2} D^{k}) \subset I_{3} (y, k) \subset B (y, 4 D^{k}) .

4.1.15

LaTeX

Lean

I1_prop_1
I3_prop_1
I2_prop_2
I3_prop_2
I3_prop_3_1
I3_prop_3_2

Lemma 7.6.2bound for tree projection

We have

‖ P_{J^{'}} | T_{T (u_{2}) ∖ S}^{*} g_{2} | ‖_{2} \leq 2^{118 a^{3}} 2^{- \frac{100}{202 a} Z n κ} ‖ 1_{I (u_{1})} M_{B, 1} | g_{2} | ‖_{2}

LaTeX Lean

Lemma 5.2.9boundary exception

Let $L (u)$ be as defined in 5.1.20. We have for each $u \in U_{1} (k, n, l)$ ,

μ (⋃_{I \in L (u)} I) \leq D^{1 - κ Z (n + 1)} μ (I (u)) .

5.2.24

LaTeX Lean

Lemma 4.1.9boundary measure

For each $- S \leq k \leq S$ and $y \in Y_{k}$ and $0 < t < 1$ with $t D^{k} \geq D^{- S}$ we have

μ ({x \in I_{3} (y, k) : ρ (x, X ∖ I_{3} (y, k)) \leq t D^{k}}) \leq 2 t^{κ} μ (I_{3} (y, k)) .

4.1.35

LaTeX Lean

Lemma 7.2.3boundary operator bound

For all $u \in U$ and all bounded functions $f$ with bounded support

‖ S_{1, u} f ‖_{2} \leq 2^{12 a} ‖ f ‖_{2} .

7.2.2

LaTeX Lean

Lemma 7.2.4boundary overlap

For every cube $I \in D$ , there exist at most $2^{9 a}$ cubes $J \in D$ with $s (J) = s (I)$ and $B (c (I), 16 D^{s (I)}) \cap B (c (J), 16 D^{s (J)}) \neq \emptyset$ .

LaTeX Lean

Lemma 5.3.5C convex

For each $k, n$ , the collection $C (k, n)$ is convex.

LaTeX Lean

Lemma 5.3.12C dens1

For each set $A \subset C (k, n)$ , we have

{dens}_{1} (A) \leq 2^{4 a} 2^{- n + 1} .

LaTeX Lean

Lemma 5.3.6C1 convex

For each $k, n, j$ , the collection $C_{1} (k, n, j)$ is convex.

LaTeX Lean

Lemma 5.3.7C2 convex

For each $k, n, j$ , the collection $C_{2} (k, n, j)$ is convex.

LaTeX Lean

Lemma 5.3.8C3 convex

For each $k, n, j$ , the collection $C_{3} (k, n, j)$ is convex.

LaTeX Lean

Lemma 5.3.9C4 convex

For each $k, n, j$ , the collection $C_{4} (k, n, j)$ is convex.

LaTeX Lean

Lemma 5.3.10C5 convex

For each $k, n, j$ , the collection $C_{5} (k, n, j)$ is convex.

LaTeX Lean

Lemma 5.4.3C6 forest

We have

C_{6} (k, n, j) = ⋃_{u \in U_{3} (k, n, j)} T_{2} (u) .

5.4.6

LaTeX Lean

Lemma 10.2.5Calderon Zygmund decomposition

Let $f$ be a bounded, measurable function supported on a set of finite measure and let $α > \frac{1}{μ (X)} \int | f | d μ$ . Then there exists a measurable function $g$ , a countable family of balls $B_{j}^{*}$ (where we allow $B_{1}^{*} = X$ in the special case that $μ (X) < \infty$ ) such that each $x \in X$ is contained in at most $2^{6 a}$ of the $B_{j}^{*}$ , and a countable family of measurable functions ${b_{j}}_{j \in J}$ such that for all $x \in X$

f (x) = g (x) + \sum_{j} b_{j} (x)

10.2.16

and such that the following holds. For almost every $x \in X$ ,

| g (x) | \leq 2^{3 a} α .

10.2.17

We have

\int | g (y) | d μ (y) \leq \int | f (y) | d μ (y) .

10.2.18

For every $j$

supp b_{j} \subset B_{j}^{*} .

10.2.19

For every $j$

\int_{B_{j}^{*}} b_{j} (x) d μ (x) = 0,

10.2.20

and

\int_{B_{j}^{*}} | b_{j} (x) | d μ (x) \leq 2^{2 a + 1} α μ (B_{j}^{*}) .

10.2.21

We have

\sum_{j} μ (B_{j}^{*}) \leq \frac{2^{4 a}}{α} \int | f (y) | d μ (y)

10.2.22

and

\sum_{j} \int_{B_{j}^{*}} | b_{j} (y) | d μ (y) \leq 2 \int | f (y) | d μ (y) .

10.2.23

LaTeX

Lean

cardinalMk_czBall3_le
tsum_czRemainder'
measurable_czApproximation
czApproximation_add_czRemainder
norm_czApproximation_le
norm_czApproximation_le_infinite
eLpNorm_czApproximation_le
support_czRemainder'_subset
integral_czRemainder'
integral_czRemainder
eLpNorm_czRemainder'_le
eLpNorm_czRemainder_le
tsum_volume_czBall3_le
volume_univ_le
tsum_eLpNorm_czRemainder'_le
tsum_eLpNorm_czRemainder_le

Lemma 10.0.3Calderon-Zygmund Weak (1, 1)

Let $f : X \to C$ be a bounded measurable function supported on a set of finite measure and assume for some $r > 0$ that for every bounded measurable function $g : X \to C$ supported on a set of finite measure,

‖ T_{r} g ‖_{2} \leq 2^{a^{3}} ‖ g ‖_{2} .

10.0.8

Then for all $α > 0$ , we have

μ ({x \in X : | T_{r} f (x) | > α}) \leq \frac{2^{a^{3} + 19 a}}{α} \int | f (y) | d μ (y) .

10.0.9

LaTeX Lean

Theorem 1.0.1classical Carleson

Let $f$ be a $2 π$ -periodic complex-valued continuous function on $R$ . Then for almost all $x \in R$ we have

lim_{N \to \infty} S_{N} f (x) = f (x),

1.0.3

where $S_{N} f$ is the $N$ -th partial Fourier sum of $f$ defined in 1.0.2.

LaTeX Lean

Lemma 11.1.3control approximation effect

There is a set $E \subset R$ with Lebesgue measure $| E | \leq ϵ$ such that for all

x \in [0, 2 π) ∖ E

11.1.7

we have

sup_{N \geq 0} | S_{N} f (x) - S_{N} f_{0} (x) | \leq \frac{ϵ}{4} .

11.1.8

LaTeX Lean

Lemma 11.1.2convergence for smooth

There exists some $N_{0} \in N$ such that for all $N > N_{0}$ and $x \in [0, 2 π]$ we have

| S_{N} f_{0} (x) - f_{0} (x) | \leq \frac{ϵ}{4} .

11.1.6

LaTeX Lean

Lemma 11.2.3

Let $f : R \to C$ be $2 π$ -periodic and twice continuously differentiable. Then

sup_{x \in [0, 2 π]} | f (x) - S_{N} f (x) | \to 0

11.2.4

as $N \to \infty$ .

LaTeX Lean

Lemma 11.2.2

Let $f : R \to C$ such that

\sum_{n \in Z} | {\hat{f}}_{n} | < \infty .

11.2.2

Then

sup_{x \in [0, 2 π]} | f (x) - S_{N} f (x) | \to 0

11.2.3

as $N \to \infty$ .

LaTeX Lean

Lemma 7.1.1convex scales

For each $u \in U$ , we have

σ (u, x) = Z \cap [\underset{―}{σ} (u, x), \overset{―}{σ} (u, x)] .

LaTeX Lean

Lemma 7.4.5correlation distant tree parts

We have for all $u_{1} \neq u_{2} \in U$ with $I (u_{1}) \subset I (u_{2})$ and all bounded $g_{1}, g_{2}$ with bounded support

| \int_{X} \sum_{p_{1} \in T (u_{1})} \sum_{p_{2} \in T (u_{2}) \cap S} T_{p_{1}}^{*} g_{1} \overset{―}{T_{p_{2}}^{*} g_{2}} d μ |

7.4.6

\leq 2^{541 a^{3}} 2^{- Z n / (4 a^{2} + 2 a^{3})} \prod_{j = 1}^{2} ‖ S_{2, u_{j}} g_{j} ‖_{L^{2} (I (u_{1}))} .

7.4.7

LaTeX Lean

Lemma 6.2.1correlation kernel bound

Let $- S \leq s_{1} \leq s_{2} \leq S$ and let $x_{1}, x_{2} \in X$ . Define

φ (y) := \overset{―}{K_{s_{1}} (x_{1}, y)} K_{s_{2}} (x_{2}, y) .

6.2.1

If $φ (y) \neq 0$ , then

y \in B (x_{1}, D^{s_{1}}) .

6.2.2

Moreover, we have with $τ = 1 / a$

‖ φ ‖_{C^{τ} (B (x_{1}, D^{s_{1}}))} \leq \frac{2^{254 a^{3}}}{μ (B (x_{1}, D^{s_{1}})) μ (B (x_{2}, D^{s_{2}}))} .

6.2.3

LaTeX

Lean

Tile.correlation
Tile.mem_ball_of_correlation_ne_zero
Tile.correlation_kernel_bound

Lemma 7.4.6correlation near tree parts

We have for all $u_{1} \neq u_{2} \in U$ with $I (u_{1}) \subset I (u_{2})$ and all bounded $g_{1}, g_{2}$ with bounded support

| \int_{X} \sum_{p_{1} \in T (u_{1})} \sum_{p_{2} \in T (u_{2}) ∖ S} T_{p_{1}}^{*} g_{1} \overset{―}{T_{p_{2}}^{*} g_{2}} d μ |

7.4.8

\leq 2^{222 a^{3}} 2^{- Z n 2^{- 10 a}} \prod_{j = 1}^{2} ‖ S_{2, u_{j}} g_{j} ‖_{L^{2} (I (u_{1}))} .

7.4.9

LaTeX Lean

Lemma 7.4.4correlation separated trees

For any $u_{1} \neq u_{2} \in U$ and all bounded $g_{1}, g_{2}$ with bounded support, we have

| \int_{X} \sum_{p_{1} \in T (u_{1})} \sum_{p_{2} \in T (u_{2})} T_{p_{1}}^{*} g_{1} \overset{―}{T_{p_{2}}^{*} g_{2}} d μ |

7.4.3

\leq 2^{550 a^{3} - 3 n} \prod_{j = 1}^{2} ‖ S_{2, u_{j}} g_{j} ‖_{L^{2} (I (u_{1}) \cap I (u_{2}))} .

7.4.4

LaTeX Lean

Lemma 10.1.3Cotlar control

Let $0 < r \leq R$ and $x \in X$ . Let $g : X \to C$ be a bounded measurable function supported on a set of finite measure. Then for all $x^{'} \in X$ with $ρ (x, x^{'}) \leq \frac{R}{4}$ we have

| T_{R} g (x) | \leq | T_{r} (g - g 1_{B (x, \frac{R}{2})}) (x^{'}) | + 2^{a^{3} + 4 a + 1} M g (x) .

10.1.15

LaTeX Lean

Lemma 10.1.5Cotlar estimate

Assume that 10.0.3 holds. Let $0 < r \leq R$ and $x \in X$ . Let $g : X \to C$ be a bounded measurable function supported on a set of finite measure. Then

| T_{R} g (x) | \leq 2^{2} M (T_{r} g) (x) + 2^{a^{3} + 20 a + 3} M g (x) .

10.1.28

LaTeX Lean

Lemma 10.1.4Cotlar sets

Assume that 10.0.3 holds. Let $0 < r \leq R$ and $x \in X$ . Let $g : X \to C$ be a bounded measurable function supported on a set of finite measure. Then the measure $| F_{1} |$ of the set $F_{1}$ of all $x^{'} \in B (x, \frac{R}{4})$ such that

| T_{r} g (x^{'}) | > 4 M (T_{r} g) (x)

10.1.21

is less than or equal to $μ (B (x, \frac{R}{4})) / 4$ . Moreover, the measure $| F_{2} |$ of the set $F_{2}$ of all $x^{'} \in B (x, \frac{R}{4})$ such that

| T_{r} (g 1_{B (x, \frac{R}{2})}) (x^{'}) | > 2^{a^{3} + 20 a + 2} M g (x)

10.1.22

is less than or equal to $μ (B (x, \frac{R}{4})) / 4$ .

LaTeX

Lean

cotlar_set_F₁
cotlar_set_F₂

Lemma 4.1.1counting balls

Let $- S \leq k \leq S$ . Consider $Y \subset X$ such that for any $y \in Y$ , we have

y \in B (o, 4 D^{S} - D^{k}),

4.1.1

furthermore, for any $y^{'} \in Y$ with $y \neq y^{'}$ , we have

B (y, D^{k}) \cap B (y^{'}, D^{k}) = \emptyset .

4.1.2

Then the cardinality of $Y$ is bounded by

| Y | \leq 2^{3 a + 200 S a^{3}} .

4.1.3

LaTeX Lean

Lemma 4.1.2cover big ball

For each $- S \leq k \leq S$ , the ball $B (o, 4 D^{S} - D^{k})$ is contained in the union of the balls $B (y, 2 D^{k})$ with $y \in Y_{k}$ .

LaTeX Lean

Lemma 4.1.4cover by cubes

Let $- S \leq l \leq k \leq S$ and $y \in Y_{k}$ . We have

I_{3} (y, k) \subset ⋃_{y^{'} \in Y_{l}} I_{3} (y^{'}, l) .

4.1.16

LaTeX Lean

Lemma 9.0.2covering separable space

For each $r > 0$ , there exists a countable collection $C (r) \subset X$ of points such that

X \subset ⋃_{c \in C (r)} B (c, r) .

LaTeX Lean

Lemma 5.3.11dens compare

We have for every $k \geq 0$ and $P^{'} \subset P (k)$

{dens}_{1} (P^{'}) \leq {dens}_{k}^{'} (P^{'}) .

5.3.7

LaTeX Lean

Lemma 6.1.4dens1 antichain

Set $p := 4 a^{4}$ . We have

| \int \overset{―}{g (x)} \sum_{p \in A} T_{p} f (x) d μ (x) | \leq 2^{150 a^{3}} {dens}_{1} (A)^{\frac{1}{2 p}} ‖ f ‖_{2} ‖ g ‖_{2} .

6.1.22

LaTeX

Lemma 6.1.3dens2 antichain

We have that

| \int \overset{―}{g (x)} \sum_{p \in A} T_{p} f (x) d μ (x) | \leq 2^{111 a^{3}} (q - 1)^{- 1} {dens}_{2} (A)^{\frac{1}{\tilde{q}} - \frac{1}{2}} ‖ f ‖_{2} ‖ g ‖_{2} .

6.1.11

LaTeX Lean

Lemma 5.2.2dense cover

For each $k \geq 0$ , the union of all dyadic cubes in $C (G, k)$ has measure at most $2^{k + 1} μ (G)$ .

LaTeX Lean

Lemma 7.3.1densities tree bound

Let $u \in U$ . Then for all bounded $f$ with bounded support and $g$ with $| g | \leq 1_{G}$ we have

| \int_{X} \bar{g} \sum_{p \in T (u)} T_{p} f d μ | \leq 2^{202.5 a^{3}} {dens}_{1} (T (u))^{1 / 2} ‖ f ‖_{2} ‖ g ‖_{2} .

7.3.1

If additionally $| f | \leq 1_{F}$ , then we have

| \int_{X} \bar{g} \sum_{p \in T (u)} T_{p} f d μ | \leq 2^{303 a^{3}} {dens}_{1} (T (u))^{1 / 2} {dens}_{2} (T (u))^{1 / 2} ‖ f ‖_{2} ‖ g ‖_{2} .

7.3.2

LaTeX

Lean

TileStructure.Forest.density_tree_bound1
TileStructure.Forest.density_tree_bound2

Lemma 11.3.5Dirichlet approximation

Let $0 < r < 1$ . Let $N$ be the smallest integer larger than $\frac{1}{r}$ . There is a $2 π$ -periodic continuous function $L^{'}$ on $R$ that satisfies for all $- π \leq x \leq π$ and all $2 π$ -periodic bounded measurable functions $f$ on $R$

L_{N} f (x) = \frac{1}{2 π} \int_{- π}^{π} f (y) L^{'} (x - y) d y

11.3.17

and

| L^{'} (x) - 1_{{y : r < | y | < 1}} κ (x) | \leq 2^{5} k_{r} (x) .

11.3.18

LaTeX

Lean

continuous_dirichletApprox
periodic_dirichletApprox
approxHilbertTransform_eq_dirichletApprox
dist_dirichletApprox_le

Lemma 11.6.1Dirichlet kernel - Hilbert kernel relation

For all $N \in Z$ and $x \in [- π, π] ∖ {0}$ ,

| K_{N} (x) - (e^{- i N x} κ (x) + \overset{―}{e^{- i N x} κ (x)}) | \leq π .

LaTeX Lean

Lemma 11.1.8Dirichlet kernel

We have for every $2 π$ -periodic bounded measurable $f$ and every $N \geq 0$

S_{N} f (x) = \frac{1}{2 π} \int_{0}^{2 π} f (y) K_{N} (x - y) d y

11.1.21

where $K_{N}$ is the $2 π$ -periodic continuous function of $R$ given by

\sum_{n = - N}^{N} e^{i n x^{'}} .

11.1.22

We have for $e^{i x^{'}} \neq 1$ that

K_{N} (x^{'}) = \frac{e^{i N x^{'}}}{1 - e^{- i x^{'}}} + \frac{e^{- i N x^{'}}}{1 - e^{i x^{'}}} .

11.1.23

LaTeX

Lean

dirichletKernel_eq
partialFourierSum_eq_conv_dirichletKernel

Proposition 2.0.2discrete Carleson

Let $(D, c, s)$ be a grid structure and

(P, I, Ω, Q, c, s)

a tile structure for this grid structure. Define for $p \in P$

E (p) = {x \in I (p) : Q (x) \in Ω (p), σ_{1} (x) \leq s (p) \leq σ_{2} (x)}

2.0.20

and

T_{p} f (x) = 1_{E (p)} (x) \int K_{s (p)} (x, y) f (y) e (Q (x) (y) - Q (x) (x)) d μ (y) .

2.0.21

Then there exists a Borel set $G^{'}$ with $2 μ (G^{'}) \leq μ (G)$ such that for all Borel functions $f : X \to C$ with $| f | \leq 1_{F}$ we have

\int_{G ∖ G^{'}} | \sum_{p \in P} T_{p} f (x) | d μ (x) \leq \frac{2^{434 a^{3}}}{(q - 1)^{4}} μ (G)^{1 - \frac{1}{q}} μ (F)^{\frac{1}{q}} .

2.0.22

LaTeX Lean

Lemma 10.2.3Disjoint family countable

In a doubling metric measure space $(X, ρ, μ, a)$ , every disjoint family of balls $B_{j} = B (x_{j}, r_{j})$ , $j \in J$ , is countable.

LaTeX Lean

Lemma 4.2.2disjoint frequency cubes

For each $I \in D$ , and $p_{1}, p_{2} \in P (I)$ , if

Ω_{1} (p_{1}) \cap Ω_{1} (p_{2}) \neq \emptyset,

then $p_{1} = p_{2}$ .

LaTeX Lean

Lemma 7.7.4disjoint row support

The sets $E_{j}$ , $1 \leq j \leq 2^{n}$ are pairwise disjoint.

LaTeX Lean

Lemma 7.5.1dyadic partition 1

We have that

I (u_{1}) = \dot{⋃_{J \in J^{'}}} J .

LaTeX

Lean

TileStructure.Forest.union_𝓙₅
TileStructure.Forest.pairwiseDisjoint_𝓙₅

Lemma 7.6.1dyadic partition 2

We have

I (u_{1}) = \dot{⋃_{J \in J^{'}}} J .

LaTeX

Lean

TileStructure.Forest.union_𝓙₆
TileStructure.Forest.pairwiseDisjoint_𝓙₆

Lemma 7.1.2dyadic partitions

For each $S \subset P$ , we have

⋃_{I \in D} I = \dot{⋃_{J \in J (S)}} J

7.1.1

and

⋃_{I \in D} I = \dot{⋃_{L \in L (S)}} L .

7.1.2

LaTeX

Lean

TileStructure.Forest.biUnion_𝓙
TileStructure.Forest.pairwiseDisjoint_𝓙
TileStructure.Forest.biUnion_𝓛
TileStructure.Forest.pairwiseDisjoint_𝓛

Lemma 4.1.5dyadic property

Let $- S \leq l \leq k \leq 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) .

4.1.17

LaTeX Lean

Lemma 5.2.4dyadic union

For each $x \in A (λ, k, n)$ , there is a dyadic cube $I$ that contains $x$ and is a subset of $A (λ, k, n)$ .

LaTeX Lean

Lemma 5.4.2equivalence relation

For each $k, n, j$ , the relation $\sim$ on $U_{2} (k, n, j)$ is an equivalence relation.

LaTeX Lean

Lemma 10.2.9Estimate bad

We have

μ ({x \in X : | T_{r} b (x) | > α / 2}) \leq \frac{\frac{2^{5 a}}{c} + 2^{a^{3} + 9 a + 4}}{α} \int | f (y) | d μ (y) .

LaTeX Lean

Lemma 10.2.7Estimate bad partial

Let $x \in X ∖ Ω$ . Then

| T_{r} b (x) | \leq 3 F (x) + α / 8,

where

F (x) := 2^{a^{3} + 2 a + 1} c α \sum_{j \in J} {(\frac{r_{j}}{ρ (x, x_{j})})}^{\frac{1}{a}} \frac{μ (B_{j})}{V (x, x_{j})} .

LaTeX Lean

Lemma 10.2.8Estimate F set

For $F$ as defined in Lemma 10.2.7, we have

μ ({x \in X ∖ Ω : F (x) > α / 8}) \leq \frac{2^{a^{3} + 9 a + 4}}{α} \int | f (y) | d μ (y) .

10.2.59

LaTeX Lean

Lemma 10.2.6Estimate good

μ ({x \in X : | T_{r} g (x) | > α / 2}) \leq \frac{2^{2 a^{3} + 3 a + 2} c}{α} \int | f (y) | d μ (y) .

LaTeX Lean

Lemma 10.1.2estimate x shift

Let $0 < r$ and $x \in X$ . Let $g : X \to C$ be a bounded measurable function supported on a set of finite measure. Then for all $x^{'}$ with $ρ (x, x^{'}) \leq r$ .

| T_{r} g (x) - T_{r} g (x^{'}) | \leq 2^{a^{3} + 2 a + 2} M g (x) .

LaTeX Lean

Lemma 5.1.1exceptional set

We have

μ (G^{'}) \leq 2^{- 1} μ (G) .

5.1.29

LaTeX Lean

Theorem 11.1.4classical Carleson with exceptional sets

Let $f$ be a $2 π$ -periodic complex-valued continuous function on $R$ . For all $ϵ > 0$ , there exists a Borel set $E \subset [0, 2 π]$ with Lebesgue measure $| E | \leq ϵ$ and a positive integer $N_{0}$ such that for all $x \in [0, 2 π] ∖ E$ and all integers $N > N_{0}$ , we have

| f (x) - S_{N} f (x) | \leq ϵ .

11.1.9

LaTeX Lean

Proposition 2.0.1finitary Carleson

Let $σ_{1}, σ_{2} : X \to Z$ be measurable functions with finite range and $σ_{1} \leq σ_{2}$ . Let $F, G$ be bounded Borel sets in $X$ . Then there is a Borel set $G^{'}$ in $X$ with $2 μ (G^{'}) \leq μ (G)$ such that for all Borel functions $f : X \to C$ with $| f | \leq 1_{F}$ .

\int_{G ∖ G^{'}} | \sum_{s = σ_{1} (x)}^{σ_{2} (x)} \int K_{s} (x, y) f (y) e (Q (x) (y)) d μ (y) | d μ (x)

\leq \frac{2^{434 a^{3}}}{(q - 1)^{5}} μ (G)^{1 - \frac{1}{q}} μ (F)^{\frac{1}{q}} .

2.0.6

LaTeX Lean

Lemma 3.0.3finitary S truncation

For all finite sets $\tilde{Θ} \subset Θ$

\int 1_{G} (x) max_{- S < s_{1} \leq s_{2} < S} sup_{ϑ \in \tilde{Θ}} | T_{1, s_{1}, s_{2}, ϑ} f (x) | d μ (x)

\leq \frac{2^{445 a^{3}}}{(q - 1)^{6}} μ (G)^{1 - \frac{1}{q}} μ (F)^{\frac{1}{q}} .

3.0.9

LaTeX

Lemma 5.2.1first exception

We have

μ (G_{1}) \leq 2^{- 5} μ (G) .

5.2.1

LaTeX Lean

Lemma 7.1.4first tree pointwise

For all $u \in U$ , all $L \in L (T (u))$ , all $x, x^{'} \in L$ and all bounded $f$ with bounded support, we have

(???) \leq 10 \cdot 2^{104 a^{3}} M_{B, 1} P_{J (T (u))} | f | (x^{'}) .

LaTeX Lean

Lemma 5.1.3forest complement

Let

P_{2} = P ∖ P_{1} .

5.1.32

For all $f : X \to C$ with $| f | \leq 1_{F}$ we have

\int_{G ∖ G^{'}} | \sum_{p \in P_{2}} T_{p} f | d μ \leq \frac{2^{153 a^{3}}}{(q - 1)^{5}} μ (G)^{1 - \frac{1}{q}} μ (F)^{\frac{1}{q}} .

5.1.33

LaTeX Lean

Lemma 5.4.5forest convex

For each $u \in U_{3} (k, n, j)$ , the set $T_{2} (u)$ satisfies the convexity condition 2.0.33.

LaTeX Lean

Lemma 5.4.4forest geometry

For each $u \in U_{3} (k, n, j)$ , the set $T_{2} (u)$ satisfies 2.0.32.

LaTeX Lean

Lemma 5.4.7forest inner

For each $u \in U_{3} (k, n, j)$ and each $p \in T_{2} (u)$ we have

B (c (p), 8 D^{s (p)}) \subset I (u) .

5.4.8

LaTeX Lean

Proposition 2.0.4forest operator

For any $n \geq 0$ and any $n$ -forest $(U, T)$ we have for all $f : X \to C$ with $| f | \leq 1_{F}$ and all bounded $g$ with bounded support

| \int \overset{―}{g (x)} \sum_{u \in U} \sum_{p \in T (u)} T_{p} f (x) d μ (x) |

\leq 2^{432 a^{3}} 2^{- \frac{q - 1}{q} n} {dens}_{2} {(⋃_{u \in U} T (u))}^{\frac{1}{q} - \frac{1}{2}} ‖ f ‖_{2} ‖ g ‖_{2} .

LaTeX Lean

Lemma 7.7.1forest row decomposition

Let $(U, T)$ be an $n$ -forest. Then there exists a decomposition

U = \dot{⋃_{1 \leq j \leq 2^{n}}} U_{j}

such that for all $j = 1, \dots, 2^{n}$ the pair $(U_{j}, T |_{U_{j}})$ is an $n$ -row.

LaTeX

Lean

TileStructure.Forest.rowDecomp
TileStructure.Forest.biUnion_rowDecomp
TileStructure.Forest.pairwiseDisjoint_rowDecomp

Lemma 5.4.6forest separation

For each $u, u^{'} \in U_{3} (k, n, j)$ with $u \neq u^{'}$ and each $p \in T_{2} (u)$ with $I (p) \subset I (u^{'})$ we have

d_{p} (Q (p), Q (u^{'})) > 2^{Z (n + 1)} .

5.4.7

LaTeX Lean

Lemma 5.4.8forest stacking

It holds for $k \leq n$ that

\sum_{u \in U_{3} (k, n, j)} 1_{I (u)} \leq (4 n + 12) 2^{n} .

5.4.9

LaTeX Lean

Lemma 5.1.2forest union

Let

P_{1} = ⋃_{k \geq 0} ⋃_{n \geq k} ⋃_{0 \leq j \leq 2 n + 3} C_{5} (k, n, j)

5.1.30

For all $f : X \to C$ with $| f | \leq 1_{F}$ we have

\int_{G ∖ G^{'}} | \sum_{p \in P_{1}} T_{p} f | d μ \leq \frac{2^{433 a^{3}}}{(q - 1)^{4}} μ (G)^{1 - \frac{1}{q}} μ (F)^{\frac{1}{q}} .

5.1.31

LaTeX Lean

Lemma 11.2.1

Let $f : R \to C$ be $2 π$ -periodic and continuously differentiable, and let $n \in Z ∖ {0}$ . Then

{\hat{f}}_{n} = \frac{1}{i n} {\hat{f^{'}}}_{n} .

11.2.1

LaTeX Lean

Lemma 4.2.1frequency ball cover

For each $I \in D$ , we have

Q (X) \subset ⋃_{z \in Z (I)} B_{I^{\circ}} (z, 0.7) .

4.2.3

LaTeX Lean

Lemma 11.7.9frequency ball doubling

For any $x, x^{'} \in R$ and $R > 0$ with $x \in B (x^{'}, 2 R)$ and any $n, m \in Z$ , we have

d_{B (x^{'}, 2 R)} (ϑ_{n}, ϑ_{m}) \leq 2 d_{B (x, R)} (ϑ_{n}, ϑ_{m}) .

11.7.9

LaTeX Lean

Lemma 11.7.10frequency ball growth

For any $x, x^{'} \in R$ and $R > 0$ with $B (x, R) \subset B (x^{'}, 2 R)$ and any $n, m \in Z$ , we have

2 d_{B (x, R)} (ϑ_{n}, ϑ_{m}) \leq d_{B (x^{'}, 2 R)} (ϑ_{n}, ϑ_{m}) .

11.7.10

LaTeX Lean

Lemma 4.2.3frequency cube cover

For each $I \in D$ , it holds that

⋃_{z \in Z (I)} B_{I^{\circ}} (z, 0.7) \subset ⋃_{p \in P (I)} Ω_{1} (p) .

4.2.5

For every $p \in P$ , it holds that

B_{p} (Q (p), 0.3) \subset Ω_{1} (p) \subset B_{p} (Q (p), 0.7) .

4.2.6

LaTeX

Lean

Construction.iUnion_ball_subset_iUnion_Ω₁
Construction.ball_subset_Ω₁
Construction.Ω₁_subset_ball

Lemma 11.7.6frequency metric

For every $R > 0$ and $x \in X$ , the function $d_{B (x, R)}$ is a metric on $Θ$ .

LaTeX Lean

Lemma 11.7.8frequency monotone

For any $x, x^{'} \in X$ and $R, R^{'} > 0$ with $B (x, R) \subset B (x, R^{'})$ , and for any $n, m \in Z$

d_{B (x, R)} (ϑ_{n}, ϑ_{m}) \leq d_{B (x^{'}, R^{'})} (ϑ_{n}, ϑ_{m}) .

LaTeX Lean

Lemma 10.1.1geometric series estimate

For all real numbers $x \geq 4$ ,

\sum_{n = 0}^{\infty} 2^{- \frac{n}{x}} \leq 2^{x} .

LaTeX Lean

Lemma 6.3.4global antichain density

Let $ϑ \in Θ$ and let $N \geq 0$ be an integer. Then we have

\sum_{p \in A_{ϑ, N}} μ (E (p) \cap G) \leq 2^{101 a^{3} + N a} {dens}_{1} (A) μ (\cup_{p \in A} I_{p}) .

6.3.26

LaTeX Lean

Lemma 7.5.9global tree control 1

Let $C_{1} = T (u_{1})$ and $C_{2} = T (u_{2}) \cap S$ . Then for $i = 1, 2$ and each $J \in J^{'}$ and all bounded $g$ with bounded support, we have

\begin{array}{r} sup_{B (J)} | T_{C_{i}}^{*} g | \leq inf_{B^{\circ} (J)} | T_{C_{i}}^{*} g | + 2^{151 a^{3} + 4 a + 2} inf_{J} M_{B, 1} | g | \end{array}

and for all $y, y^{'} \in B (J)$

| e (Q (u_{i}) (y)) T_{C_{i}}^{*} g (y) - e (Q (u_{i}) (y^{'})) T_{C_{i}}^{*} g (y^{'}) |

\leq 2^{151 a^{3} + 4 a + 1} {(\frac{ρ (y, y^{'})}{D^{s (J)}})}^{1 / a} inf_{J} M_{B, 1} | g | .

7.5.18

LaTeX

Lean

TileStructure.Forest.global_tree_control1_edist_left
TileStructure.Forest.global_tree_control1_edist_right
TileStructure.Forest.global_tree_control1_supbound

Lemma 7.5.10global tree control 2

We have for all $J \in J^{'}$ and all bounded $g$ with bounded support

sup_{B (J)} | T_{T (u_{2}) \cap S}^{*} g | \leq inf_{B^{\circ} (J)} | T_{T (u_{2})}^{*} g | + 2^{155 a^{3}} inf_{J} M_{B, 1} | g | .

LaTeX Lean

Lemma 4.0.1grid existence

There exists a grid structure $(D, c, s)$ .

LaTeX Lean

Proposition 2.0.6Hardy–Littlewood

Let $B$ be a finite collection of balls in $X$ . If for some $λ > 0$ and some measurable function $u : X \to [0, \infty)$ we have

\int_{B} u (x) d μ (x) \geq λ μ (B)

2.0.42

for each $B \in B$ , then

λ μ (⋃ B) \leq 2^{2 a} \int_{X} u (x) d μ (x) .

2.0.43

For every measurable function $v$ and $1 \leq p_{1} < p_{2}$ we have

‖ M_{B, p_{1}} v ‖_{p_{2}} \leq 2^{2 a} \frac{p_{2}}{p_{2} - p_{1}} ‖ v ‖_{p_{2}} .

2.0.44

Moreover, given any measurable bounded function $w : X \to C$ there exists a measurable function $M w : X \to [0, \infty)$ such that the following 2.0.45 and 2.0.46 hold. For each ball $B \subset X$ and each $x \in B$

\frac{1}{μ (B)} \int_{B} | w (y) | d μ (y) \leq M w (x)

2.0.45

and for all $1 \leq p_{1} < p_{2} \leq \infty$

‖ M (w^{p_{1}})^{\frac{1}{p_{1}}} ‖_{p_{2}} \leq 2^{4 a} \frac{p_{2}}{p_{2} - p_{1}} ‖ w ‖_{p_{2}} .

2.0.46

LaTeX

Lean

Finset.measure_biUnion_le_lintegral
hasStrongType_maximalFunction
MeasureTheory.AEStronglyMeasurable.globalMaximalFunction
laverage_le_globalMaximalFunction

Lemma 11.1.11Hilbert kernel bound

For $x, y \in R$ with $x \neq y$ we have

| κ (x - y) | \leq 2^{2} (2 | x - y |)^{- 1} .

11.1.29

LaTeX Lean

Lemma 11.1.12Hilbert kernel regularity

For $x, y, y^{'} \in R$ with $x \neq y, y^{'}$ and

2 | y - y^{'} | \leq | x - y |,

11.1.32

we have

| κ (x - y) - κ (x - y^{'}) | \leq 2^{8} \frac{1}{| x - y |} \frac{| y - y^{'} |}{| x - y |} .

11.1.33

LaTeX Lean

Lemma 11.1.6Hilbert strong 2 2

Let $0 < r < 1$ . Let $f$ be a bounded, measurable function on $R$ with bounded support. Then

‖ H_{r} f ‖_{2} \leq 2^{13} ‖ f ‖_{2},

11.1.17

where

H_{r} f (x) := T_{r} f (x) = \int_{r \leq ρ (x, y)} κ (x - y) f (y) d y

11.1.18

LaTeX Lean

Lemma 7.5.5Holder correlation tile

Let $u \in U$ and $p \in T (u)$ . Then for all $y, y^{'} \in X$ and all bounded $g$ with bounded support, we have

| e (Q (u) (y)) T_{p}^{*} g (y) - e (Q (u) (y^{'})) T_{p}^{*} g (y^{'}) |

\leq \frac{2^{151 a^{3}}}{μ (B (c (p), 4 D^{s (p)}))} {(\frac{ρ (y, y^{'})}{D^{s (p)}})}^{1 / a} \int_{E (p)} | g (x) | d μ (x) .

7.5.9

LaTeX Lean

Lemma 7.5.4Holder correlation tree

We have for all $J \in J^{'}$ that

‖ h_{J} ‖_{C^{τ} (B (c (J), 8 D^{s (J)}))} \leq 2^{535 a^{3}} \prod_{j = 1, 2} (inf_{B (c (J), \frac{1}{8} D^{s (J)})} | T_{T (u_{j})}^{*} g_{j} | + inf_{J} M_{B, 1} | g_{j} |) .

7.5.8

LaTeX Lean

Proposition 2.0.5Holder van der Corput

Let $z \in X$ and $R > 0$ and set $B = B (z, R)$ . Let $φ : X \to C$ by supported on $B$ and satisfy $‖ φ ‖_{C^{τ} (B)} < \infty$ . Let $ϑ, θ \in Θ$ . Then

| \int e (ϑ (x) - θ (x)) φ (x) d x | \leq 2^{8 a} μ (B) ‖ φ ‖_{C^{τ} (B)} (1 + d_{B} (ϑ, θ))^{- \frac{1}{2 a^{2} + a^{3}}} .

2.0.40

LaTeX Lean

Lemma 11.7.11integer ball cover

For every $x \in R$ and $R > 0$ and every $n \in Z$ and $R^{'} > 0$ , there exist $m_{1}, m_{2}, m_{3} \in Z$ such that

B^{'} \subset B_{1} \cup B_{2} \cup B_{3},

11.7.11

where

B^{'} = {ϑ \in Θ : d_{B (x, R)} (ϑ, ϑ_{n}) < 2 R^{'}}

11.7.12

and for $j = 1, 2, 3$

B_{j} = {ϑ \in Θ : d_{B (x, R)} (ϑ, ϑ_{m_{j}}) < R^{'}} .

11.7.13

LaTeX Lean

Lemma 11.3.4integrable bump convolution

Let $g, f$ be bounded measurable $2 π$ -periodic functions. Let $0 < r < π$ . Assume we have for all $0 \leq x \leq 2 π$

| g (x) | \leq k_{r} (x) .

11.3.12

Let

h (x) = \int_{- π}^{π} f (y) g (x - y) d y .

11.3.13

Then

‖ h ‖_{L^{2} [- π, π]} \leq 2^{5} ‖ f ‖_{L^{2} [- π, π]} .

11.3.14

LaTeX Lean

Lemma 5.2.5John Nirenberg

For all integers $k, n, λ \geq 0$ , we have

μ (A (λ, k, n)) \leq 2^{k + 1 - λ} μ (G) .

5.2.5

LaTeX Lean

Lemma 2.1.3kernel summand

Let $- S \leq s \leq S$ and $x, y, y^{'} \in X$ . If $K_{s} (x, y) \neq 0$ , then we have

\frac{1}{4} D^{s - 1} \leq ρ (x, y) \leq \frac{1}{2} D^{s} .

2.1.2

We have

| K_{s} (x, y) | \leq \frac{2^{102 a^{3}}}{μ (B (x, D^{s}))}

2.1.3

and

| K_{s} (x, y) - K_{s} (x, y^{'}) | \leq \frac{2^{150 a^{3}}}{μ (B (x, D^{s}))} {(\frac{ρ (y, y^{'})}{D^{s}})}^{\frac{1}{a}} .

2.1.4

LaTeX

Lean

dist_mem_Icc_of_Ks_ne_zero
norm_Ks_le
norm_Ks_sub_Ks_le

Lemma 5.5.2L0 antichain

We have that

L_{0} (k, n) = \dot{⋃_{0 \leq l < n}} L_{0} (k, n, l),

where each $L_{0} (k, n, l)$ is an antichain.

LaTeX

Lean

iUnion_L0'
pairwiseDisjoint_L0'
antichain_L0'

Lemma 5.5.4L1 L3 antichain

Each of the sets $L_{1} (k, n, j, l)$ and $L_{3} (k, n, j, l)$ is an antichain.

LaTeX

Lean

antichain_L1
antichain_L3

Lemma 5.5.3L2 antichain

Each of the sets $L_{2} (k, n, j)$ is an antichain.

LaTeX Lean

Lemma 9.0.1layer cake representation

Let $1 \leq p < \infty$ . Then for any measurable function $u : X \to [0, \infty)$ on the measure space $X$ relative to the measure $μ$ we have

‖ u ‖_{p}^{p} = p \int_{0}^{\infty} λ^{p - 1} μ ({x : u (x) \geq λ}) d λ .

9.0.1

LaTeX Lean

Lemma 10.2.2Lebesgue differentiation

Let $f$ be a bounded measurable function supported on a set of finite measure. Then for $μ$ almost every $x$ , we have

lim_{n \to \infty} \frac{1}{μ (B_{n})} \int_{B_{n}} f (y) d y = f (x),

where ${B_{n}}_{n \geq 1}$ is a sequence of balls with radii $r_{n} > 0$ such that $x \in B_{n}$ for each $n \geq 1$ and

lim_{n \to \infty} r_{n} = 0 .

LaTeX Lean

Lemma 7.5.6limited scale impact

Let $p \in T (u_{2}) ∖ S$ , $J \in J^{'}$ and suppose that

B (I (p)) \cap B^{\circ} (J) \neq \emptyset .

Then

s (J) \leq s (p) \leq s (J) + 3 .

LaTeX Lean

Theorem 1.0.3linearised metric Carleson

For all integers $a \geq 4$ and real numbers $1 < q \leq 2$ the following holds. Let $(X, ρ, μ, a)$ be a doubling metric measure space. Let $Θ$ be a cancellative compatible collection of functions. Let $Q : X \to Θ$ be a Borel function with finite range. Let $K$ be a one-sided Calderón–Zygmund kernel on $(X, ρ, μ, a)$ . Assume that for every $ϑ \in Θ$ and every bounded measurable function $g$ on $X$ supported on a set of finite measure we have

‖ T_{Q}^{ϑ} g ‖_{2} \leq 2^{a^{3}} ‖ g ‖_{2},

1.0.23

where $T_{Q}^{ϑ}$ is defined in 1.0.21. Then for all bounded Borel sets $F$ and $G$ in $X$ and all Borel functions $f : X \to C$ with $| f | \leq 1_{F}$ , we have, with $T_{Q}$ defined in 1.0.22,

| \int_{G} T_{Q} f d μ | \leq \frac{2^{450 a^{3}}}{(q - 1)^{6}} μ (G)^{1 - \frac{1}{q}} μ (F)^{\frac{1}{q}} .

1.0.24

LaTeX Lean

Lemma 3.0.4linearized truncation

Let $σ_{1}, σ_{2} : X \to Z$ be measurable functions with finite range $[- S, S]$ and $σ_{1} \leq σ_{2}$ . Let $Q : X \to \tilde{Θ}$ be a measurable function. Then we have

\int 1_{G} (x) | T_{2, σ_{1}, σ_{2}, Q} f (x) | d μ (x) \leq \frac{2^{445 a^{3}}}{(q - 1)^{6}} μ (G)^{1 - \frac{1}{q}} μ (F)^{\frac{1}{q}},

3.0.11

with

T_{2, σ_{1}, σ_{2}, Q} f (x) = \sum_{σ_{1} (x) \leq s \leq σ_{2} (x)} \int K_{s} (x, y) f (y) e (Q (x) (y) - Q (x) (x)) d μ (y) .

3.0.12

LaTeX

Lemma 8.0.1Lipschitz Holder approximation

Let $z \in X$ and $R > 0$ . Let $φ : X \to C$ be a function supported in the ball $B := B (z, R)$ with finite norm $‖ φ ‖_{C^{τ} (B)}$ . Let $0 < t \leq 1$ . There exists a function $\tilde{φ} : X \to C$ , supported in $B (z, 2 R)$ , such that for every $x \in X$

| φ (x) - \tilde{φ} (x) | \leq t^{τ} ‖ φ ‖_{C^{τ} (B)}

8.0.1

and

‖ \tilde{φ} ‖_{Lip (B (z, 2 R))} \leq 2^{4 a} t^{- 1 - a} ‖ φ ‖_{C^{τ} (B)} .

8.0.2

LaTeX

Lean

support_holderApprox_subset
dist_holderApprox_le
iLipENorm_holderApprox

Lemma 7.5.2Lipschitz partition unity

There exists a family of functions $χ_{J}$ , $J \in J^{'}$ such that

1_{I (u_{1})} = \sum_{J \in J^{'}} χ_{J},

7.5.2

and for all $J \in J^{'}$ and all $y, y^{'} \in I (u_{1})$

0 \leq χ_{J} (y) \leq 1_{B (J)} (y),

7.5.3

| χ_{J} (y) - χ_{J} (y^{'}) | \leq 2^{226 a^{3}} \frac{ρ (y, y^{'})}{D^{s (J)}} .

7.5.4

LaTeX

Lean

TileStructure.Forest.sum_χ
TileStructure.Forest.χ_le_indicator
TileStructure.Forest.dist_χ_le

Lemma 6.3.3local antichain density

Let $ϑ \in Θ$ and $N$ be an integer. Let $p_{ϑ}$ be a tile with $ϑ \in Ω (p_{ϑ})$ . Then we have

\sum_{p \in A_{ϑ, N} : s (p_{ϑ}) < s (p)} μ (E (p) \cap G \cap I (p_{ϑ})) \leq μ (E_{2} (2^{N + 3}, p_{ϑ})) .

6.3.21

LaTeX

Lean

Antichain.local_antichain_density
Antichain.Ep_inter_G_inter_Ip'_subset_E2

Lemma 7.3.2local dens1 tree bound

Let $u \in U$ and $L \in L (T (u))$ . Then

μ (L \cap G \cap ⋃_{p \in T (u)} E (p)) \leq 2^{101 a^{3}} {dens}_{1} (T (u)) μ (L) .

7.3.3

LaTeX Lean

Lemma 7.3.3local dens2 tree bound

Let $u \in U$ and $J \in J (T (u))$ . Then

μ (F \cap J) \leq 2^{201 a^{3}} {dens}_{2} (T (u)) μ (J) .

LaTeX Lean

Lemma 7.5.7local tree control

For all $J \in J^{'}$ and all bounded $g$ with bounded support

sup_{B^{\circ} (J)} | T_{T (u_{2}) ∖ S}^{*} g | \leq 2^{104 a^{3}} inf_{J} M_{B, 1} | g |

LaTeX Lean

Lemma 7.5.11lower oscillation bound

For all $J \in J^{'}$ , we have that

d_{B (J)} (Q (u_{1}), Q (u_{2})) \geq 2^{- 201 a^{3}} 2^{Z n / 2} .

LaTeX Lean

Lemma 11.1.9lower secant bound

Let $η > 0$ and $- 2 π + η \leq x \leq 2 π - η$ with $| x | \geq η$ . Then

| 1 - e^{i x} | \geq \frac{2}{π} η

11.1.27

LaTeX Lean

Lemma 6.1.2maximal bound antichain

Let $x \in X$ . Then

| \sum_{p \in A} T_{p} f (x) | \leq 2^{107 a^{3}} M_{B} f (x) .

6.1.2

LaTeX Lean

Lemma 10.2.1Maximal theorem

Let $f : X \to C$ be bounded, measurable, supported on a set of finite measure, and let $α > 0$ . Then

μ ({x \in X : M f (x) > α}) \leq \frac{2^{2 a}}{α} \int | f (y) | d μ (y) .

10.2.1

LaTeX Lean

Theorem 1.0.2metric space Carleson

For all integers $a \geq 4$ and real numbers $1 < q \leq 2$ the following holds. Let $(X, ρ, μ, a)$ be a doubling metric measure space. Let $Θ$ be a cancellative compatible collection of functions and let $K$ be a one-sided Calderón–Zygmund kernel on $(X, ρ, μ, a)$ . Assume that for every bounded measurable function $g$ on $X$ supported on a set of finite measure we have

‖ T_{*} g ‖_{2} \leq 2^{a^{3}} ‖ g ‖_{2},

1.0.18

where $T_{*}$ is defined in 1.0.16. Then for all Borel sets $F$ and $G$ in $X$ and all Borel functions $f : X \to C$ with $| f | \leq 1_{F}$ , we have, with $T$ defined in 1.0.17,

| \int_{G} T f d μ | \leq \frac{2^{450 a^{3}}}{(q - 1)^{6}} μ (G)^{1 - \frac{1}{q}} μ (F)^{\frac{1}{q}} .

1.0.19

LaTeX Lean

Lemma 7.5.3moderate scale change

If $J, J^{'} \in J^{'}$ with

B (J) \cap B (J^{'}) \neq \emptyset,

then $| s (J) - s (J^{'}) | \leq 1$ .

LaTeX Lean

Lemma 11.3.1modulated averaged projection

We have for every bounded measurable $2 π$ -periodic function $g$

‖ L_{N} g ‖_{L^{2} [- π, π]} \leq ‖ g ‖_{L^{2} [- π, π]} .

11.3.3

LaTeX Lean

Lemma 2.1.2monotone cube metrics

Let $(D, c, s)$ be a grid structure. Denote for cubes $I \in D$

I^{\circ} := B (c (I), \frac{1}{4} D^{s (I)}) .

Let $I, J \in D$ with $I \subset J$ . Then for all $ϑ, θ \in Θ$ we have

d_{I^{\circ}} (ϑ, θ) \leq d_{J^{\circ}} (ϑ, θ),

and if $I \neq J$ then we have

d_{I^{\circ}} (ϑ, θ) \leq 2^{- 95 a} d_{J^{\circ}} (ϑ, θ) .

LaTeX

Lean

Grid.dist_mono
Grid.dist_strictMono

Lemma 10.0.2nontangential-from-simple

Assume 10.0.3 holds. Then, for every bounded measurable function $g : X \to C$ supported on a set of finite measure we have

‖ T_{*} g ‖_{2} \leq 2^{3 a^{3}} ‖ g ‖_{2} .

10.0.5

LaTeX Lean

Lemma 7.2.2nontangential operator bound

For all bounded $f$ with bounded support and all $ϑ \in Θ$

‖ T_{N}^{ϑ} f ‖_{2} \leq 2^{102 a^{3}} ‖ f ‖_{2} .

LaTeX Lean

Lemma 10.1.8nontangential operator boundary

Let $f : X \to C$ be a bounded measurable function supported on a set of finite measure. For all $x \in X$ ,

T_{*} f (x) = sup_{R_{1} < R_{2}} sup_{x^{'} \in B (x, R_{1})} | \int_{B (x^{'}, R_{2}) ∖ B (x^{'}, R_{1})} K (x^{'}, y) f (y) d μ (y) |

10.1.39

LaTeX Lean

Lemma 11.7.7oscillation control

For every $R > 0$ and $x \in X$ , and for all $n, m \in Z$ , we have

sup_{y, y^{'} \in B (x, R)} | n y - n y^{'} - m y + m y^{'} | \leq 2 | n - m | R .

11.7.8

LaTeX Lean

Lemma 7.4.7overlap implies distance

Let $u_{1} \neq u_{2} \in U$ with $I (u_{1}) \subset I (u_{2})$ . If $p \in T (u_{1}) \cup T (u_{2})$ with $I (p) \cap I (u_{1}) \neq \emptyset$ , then $p \in S$ . In particular, we have $T (u_{1}) \subset S$ .

LaTeX

Lean

TileStructure.Forest.𝔗_subset_𝔖₀
TileStructure.Forest.overlap_implies_distance

Lemma 5.3.4P convex

For each $k$ , the collection $P (k)$ is convex.

LaTeX Lean

Lemma 5.2.3pairwise disjoint

If $p, p^{'} \in M (k, n)$ and

E_{1} (p) \cap E_{1} (p^{'}) \neq \emptyset,

5.2.4

then $p = p^{'}$ .

LaTeX Lean

Lemma 11.6.2partial Fourier sum bound

Let $g : R \to C$ be a measurable $2 π$ -periodic function such that for some $δ > 0$ and every $x \in R$ ,

| g (x) | \leq δ .

11.6.1

Then for every $x \in [0, 2 π]$ and $N > 0$ ,

| S_{N} g (x) | \leq \frac{1}{2 π} (T g (x) + T \bar{g} (x)) + π δ .

LaTeX Lean

Lemma 11.6.4partial Fourier sums of small

Let $g : R \to C$ be a measurable $2 π$ -periodic function such that for some $δ > 0$ and every $x \in R$ ,

| g (x) | \leq δ .

11.6.5

Then for every $ϵ > 0$ , there exists a measurable set $E \subset [0, 2 π]$ with $| E | < ϵ$ such that for every $x \in [0, 2 π] ∖ E$ and $N > 0$ ,

| S_{N} g (x) | \leq C_{ϵ} δ,

11.6.6

where

C_{ϵ} = {(\frac{8}{π ϵ})}^{\frac{1}{2}} C_{4, 2} + π .

11.6.7

LaTeX Lean

Lemma 11.3.2periodic domain shift

Let $f$ be a bounded $2 π$ -periodic function. We have for any $0 \leq x \leq 2 π$ that

\int_{0}^{2 π} f (y) d y = \int_{- x}^{2 π - x} f (y) d y = \int_{- π}^{π} f (y - x) d y .

11.3.6

LaTeX

Lean

Function.Periodic.intervalIntegral_add_eq
intervalIntegral.integral_comp_sub_right

Lemma 7.1.3pointwise tree estimate

Let $u \in U$ and $L \in L (T (u))$ . Let $x, x^{'} \in L$ . Then for all bounded functions $f$ with bounded support

| \sum_{p \in T (u)} T_{p} [e (- Q (u)) f] (x) |

\leq 2^{151 a^{3}} (M_{B, 1} + S_{1, u}) P_{J (T (u))} | f | (x^{'}) + | T_{N}^{Q (u)} P_{J (T (u))} f (x^{'}) |,

7.1.5

LaTeX Lean

Lemma 3.0.1R truncation

For all integers $R > 0$

\int 1_{G \cap B (o, R)} sup_{1 / R < R_{1} < R_{2} < R} sup_{ϑ \in Θ} | T_{R_{1}, R_{2}, ϑ} f (x) | d μ (x)

\leq \frac{2^{450 a^{3}}}{(q - 1)^{6}} μ (G)^{1 - \frac{1}{q}} μ (F)^{\frac{1}{q}},

3.0.2

where

T_{R_{1}, R_{2}, ϑ} f (x) = \int_{R_{1} < ρ (x, y) < R_{2}} K (x, y) f (y) e (ϑ (y)) d μ (y) .

3.0.3

LaTeX

Lemma 11.1.5real Carleson

Let $F, G$ be Borel subsets of $R$ with finite measure. Let $f$ be a bounded measurable function on $R$ with $| f | \leq 1_{F}$ . Then

| \int_{G} T f (x) d x | \leq C_{4, 2} | F |^{\frac{1}{2}} | G |^{\frac{1}{2}},

11.1.15

where

T f (x) = sup_{n \in Z} sup_{r > 0} | \int_{r < | x - y | < 1} f (y) κ (x - y) e^{i n y} d y | .

11.1.16

LaTeX Lean

Lemma 11.6.3real Carleson operator measurable

Let $f$ be a bounded measurable function on $R$ . Then $T f$ as defined in 11.1.16 is measurable.

LaTeX Lean

Lemma 11.7.2real line ball

For $x \in R$ and $R > 0$ , the ball $B (x, R)$ is the interval $(x - R, x + R)$

LaTeX Lean

Lemma 11.7.4real line ball measure

We have for every $x \in R$ and $R > 0$

μ (B (x, R)) = 2 R .

11.7.2

LaTeX Lean

Lemma 11.7.5real line doubling

We have for every $x \in R$ and $R > 0$

μ (B (x, 2 R)) = 2 μ (B (x, R)) .

11.7.4

LaTeX Lean

Lemma 11.7.3real line measure

The measure $μ$ is a sigma-finite non-zero Radon-Borel measure on $R$ .

LaTeX Lean

Lemma 11.7.1real line metric

The space $(R, ρ)$ is a complete locally compact metric space.

LaTeX

Lean

instProperSpaceReal
locally_compact_of_proper
Real.instCompleteSpace

Lemma 11.7.12real van der Corput

For any $x \in R$ and $R > 0$ and any function $φ : X \to C$ supported on $B^{'} = B (x, R)$ such that

‖ φ ‖_{Lip (B^{'})} = sup_{x \in B^{'}} | φ (x) | + R sup_{x, y \in B^{'}, x \neq y} \frac{| φ (x) - φ (y) |}{ρ (x, y)}

11.7.17

is finite and for any $n, m \in Z$ , we have

| \int_{B^{'}} e (ϑ_{n} (x) - ϑ_{m} (x)) φ (x) d μ (x) | \leq 2 π μ (B^{'}) \frac{‖ φ ‖_{Lip (B^{'})}}{1 + d_{B^{'}} (ϑ_{n}, ϑ_{m})} .

11.7.18

LaTeX Lean

Lemma 5.4.1relation geometry

If $u \sim u^{'}$ , then $I (u) = I (u^{'})$ and

B_{u} (Q (u), 100) \cap B_{u^{'}} (Q (u^{'}), 100) \neq \emptyset .

LaTeX

Lean

URel.eq
URel.not_disjoint

Lemma 7.7.2row bound

For each $1 \leq j \leq 2^{n}$ and each bounded $g$ with bounded support with $| g | \leq 1_{G}$ , we have

{‖ \sum_{u \in U_{j}} \sum_{p \in T (u)} T_{p}^{*} g ‖}_{2} \leq 2^{156 a^{3}} 2^{- n / 2} ‖ g ‖_{2}

7.7.1

and

{‖ \sum_{u \in U_{j}} \sum_{p \in T (u)} 1_{F} T_{p}^{*} g ‖}_{2} \leq 2^{257 a^{3}} 2^{- n / 2} {dens}_{2} (⋃_{u \in U} T (u))^{1 / 2} ‖ g ‖_{2} .

7.7.2

LaTeX

Lean

TileStructure.Forest.row_bound
TileStructure.Forest.indicator_row_bound

Lemma 7.7.3row correlation

For all $1 \leq j < j^{'} \leq 2^{n}$ and for all $g_{1}, g_{2}$ with $| g_{i} | \leq 1_{G}$ , it holds that

| \int \sum_{u \in U_{j}} \sum_{u^{'} \in U_{j^{'}}} \sum_{p \in T_{j} (u)} \sum_{p^{'} \in T_{j^{'}} (u^{'})} T_{p}^{*} g_{1} \overset{―}{T_{p^{'}}^{*} g_{2}} d μ | \leq 2^{862 a^{3} - 3 n} ‖ g_{1} ‖_{2} ‖ g_{2} ‖_{2} .

LaTeX Lean

Lemma 3.0.2S truncation

For all integers $S > 0$

\int 1_{G} (x) max_{- S < s_{1} \leq s_{2} < S} sup_{ϑ \in Θ} | T_{1, s_{1}, s_{2}, ϑ} f (x) | d μ (x)

\leq \frac{2^{446 a^{3}}}{(q - 1)^{6}} μ (G)^{1 - \frac{1}{q}} μ (F)^{\frac{1}{q}},

3.0.6

where $T_{1, s_{1}, s_{2}, ϑ}$ is defined in 3.0.4.

LaTeX

Lemma 7.5.8scales impacting interval

Let $C = T (u_{1})$ or $C = T (u_{2}) \cap S$ . Then for each $J \in J^{'}$ and $p \in C$ with $B (I (p)) \cap B (J) \neq \emptyset$ , we have $s (p) \geq s (J)$ .

LaTeX Lean

Lemma 5.2.6second exception

We have

μ (G_{2}) \leq 2^{- 2} μ (G) .

5.2.13

LaTeX Lean

Lemma 7.1.5second tree pointwise

For all $u \in U$ , all $L \in L (T (u))$ , all $x, x^{'} \in L$ and all bounded $f$ with bounded support, we have

| \sum_{s \in σ (u, x)} \int K_{s} (x, y) P_{J (T (u))} f (y) d μ (y) | \leq T_{N}^{Q (u)} P_{J (T (u))} f (x^{'}) .

LaTeX Lean

Lemma 10.1.6simple nontangential operator

Assume that 10.0.3 holds. For every $r > 0$ and every bounded measurable function $g$ supported on a set of finite measure we have

‖ T_{*}^{r} g ‖_{2} \leq 2^{a^{3} + 24 a + 6} ‖ g ‖_{2},

10.1.30

where

T_{*}^{r} g (x) := sup_{r < R} sup_{x^{'} \in B (x, R)} | T_{R} (g) (x^{'}) | .

10.1.31

LaTeX Lean

Lemma 10.1.7small annulus

Let $f : X \to C$ be a bounded measurable function supported on a set of finite measure. Let $x \in X$ and $R > 0$ . Then, for all $ϵ > 0$ , there exists some $δ > 0$ such that

| \int_{R < ρ (x, y) < R + δ} K (x, y) f (y) d μ (y) | \leq ϵ

10.1.37

and

| \int_{R - δ < ρ (x, y) < R} K (x, y) f (y) d μ (y) | \leq ϵ .

10.1.38

LaTeX

Lean

small_annulus_right
small_annulus_left

Lemma 4.1.7small boundary

Let $K = 2^{4 a + 1}$ . For each $- S + K \leq k \leq S$ and $y \in Y_{k}$ we have

\sum_{z \in Y_{k - K} : (z, k - K | y, k)} μ (I_{3} (z, k - K)) \leq \frac{1}{2} μ (I_{3} (y, k)) .

4.1.24

LaTeX Lean

Lemma 4.1.8smaller boundary

Let $K = 2^{4 a + 1}$ and let $n \geq 0$ be an integer. Then for each $- S + n K \leq k \leq S$ we have

\sum_{y^{'} \in Y_{k - n K} : (y^{'}, k - n K | y, k)} μ (I_{3} (y^{'}, k - n K)) \leq 2^{- n} μ (I_{3} (y, k)) .

4.1.31

LaTeX Lean

Lemma 11.1.1smooth approximation

The function $f_{0}$ is $2 π$ -periodic. The function $f_{0}$ is smooth (and therefore measurable). The function $f_{0}$ satisfies for all $x \in R$ :

| f (x) - f_{0} (x) | \leq ϵ^{'},

11.1.5

LaTeX Lean

Lemma 11.1.10spectral projection bound

Let $f$ be a bounded $2 π$ -periodic measurable function. Then, for all $N \geq 0$

‖ S_{N} f ‖_{L^{2} [- π, π]} \leq ‖ f ‖_{L^{2} [- π, π]} .

11.1.28

LaTeX Lean

Lemma 7.6.4square function count

For each $J \in J^{'}$ and all $s \geq 0$ , we have

\frac{1}{μ (J)} \int_{J} (\sum_{\begin{matrix} I \in D, s (I) = s (J) - s \\ I \cap I (u_{1}) = \emptyset \\ J \cap B (I) \neq \emptyset \end{matrix}} 1_{B (I)})^{2} d μ \leq 2^{14 a + 1} (8 D^{- s})^{κ} .

LaTeX Lean

Lemma 6.3.2stack density

Let $ϑ \in Θ$ , $N \geq 0$ and $L \in D$ . Then

\sum_{p \in A_{ϑ, N} : I (p) = L} μ (E (p) \cap G) \leq 2^{a (N + 5)} {dens}_{1} (A) μ (L) .

6.3.16

LaTeX Lean

Lemma 7.6.3thin scale impact

If $p \in T (u_{2}) ∖ S$ and $J \in J^{'}$ with $B (I (p)) \cap B (J) \neq \emptyset$ , then

s (p) \leq s (J) + 2 - \frac{Z n}{202 a^{3}} .

LaTeX Lean

Lemma 5.2.10third exception

We have

μ (G_{3}) \leq 2^{- 4} μ (G) .

5.2.26

LaTeX Lean

Lemma 7.1.6third tree pointwise

For all $u \in U$ , all $L \in L (T (u))$ , all $x, x^{'} \in L$ and all bounded $f$ with bounded support, we have

| \sum_{s \in σ (u, x)} \int K_{s} (x, y) (f (y) - P_{J (T (u))} f (y)) d μ (y) |

\leq 2^{151 a^{3}} S_{1, u} P_{J (T (u))} | f | (x^{'}) .

LaTeX Lean

Lemma 6.1.5tile correlation

Let $p, p^{'} \in P$ with $s (p^{'}) \leq s (p)$ . Then

| \int T_{p^{'}}^{*} g \overset{―}{T_{p}^{*} g} |

6.1.43

\leq 2^{255 a^{3}} \frac{(1 + d_{p^{'}} (Q (p^{'}), Q (p))^{- 1 / (2 a^{2} + a^{3})}}{μ (I (p))} \int_{E (p^{'})} | g | \int_{E (p)} | g | .

6.1.44

Moreover, the term 6.1.43 vanishes unless

I (p^{'}) \subset B (c (p), 15 D^{s (p)}) .

6.1.45

LaTeX

Lean

Tile.correlation_le
Tile.correlation_zero_of_ne_subset

Lemma 6.1.1tile disjointness

Let $p, p^{'} \in A$ . If there exists an $x \in X$ with $x \in E (p) \cap E (p^{'})$ , then $p = p^{'}$ .

LaTeX Lean

Lemma 6.2.2tile range support

For each $p \in P$ , and each $y \in X$ , we have that

T_{p}^{*} g (y) \neq 0

6.2.10

implies

y \in B (c (p), 5 D^{s (p)}) .

6.2.11

LaTeX Lean

Lemma 6.3.1tile reach

Let $ϑ \in Θ$ and $N \geq 0$ be an integer. Let $p, p^{'} \in P$ with

d_{p} (Q (p), ϑ)) \leq 2^{N}

6.3.1

d_{p^{'}} (Q (p^{'}), ϑ)) \leq 2^{N} .

6.3.2

Assume $I (p) \subset I (p^{'})$ and $s (p) < s (p^{'})$ . Then

2^{N + 2} p ≲ 2^{N + 2} p^{'} .

6.3.3

LaTeX Lean

Lemma 4.0.2tile structure

For a given grid structure $(D, c, s)$ , there exists a tile structure $(P, I, Ω, Q, c, s)$ .

LaTeX Lean

Lemma 4.0.3tile sum operator

We have for all $x \in G ∖ G^{'}$

\sum_{p \in P} T_{p} f (x) = \sum_{s = σ_{1} (x)}^{σ_{2} (x)} \int K_{s} (x, y) f (y) e (Q (x) (y) - Q (x) (x)) d μ (y) .

4.0.1

LaTeX

Lean

tile_sum_operator
integrable_tile_sum_operator

Lemma 6.2.3

Let $p_{1}, p_{2} \in P$ with $B (c (p_{1}), 5 D^{s (p_{1})}) \cap B (c (p_{2}), 5 D^{s (p_{2})}) \neq \emptyset$ and $s (p_{1}) \leq s (p_{2})$ . For each $x_{1} \in E (p_{1})$ and $x_{2} \in E (p_{2})$ we have

1 + d_{p_{1}} (Q (p_{1}), Q (p_{2})) \leq 2^{8 a} (1 + d_{B (x_{1}, D^{s (p_{1})})} (Q (x_{1}), Q (x_{2}))) .

6.2.15

LaTeX Lean

Lemma 5.2.7top tiles

We have

\sum_{m \in M (k, n)} μ (I (m)) \leq 2^{n + k + 3} μ (G) .

5.2.16

LaTeX Lean

Lemma 4.1.6transitive boundary

Assume $- S \leq k^{″} < k^{'} < k \leq 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) .

4.1.20

If $(y^{″}, k^{″} | y, k)$ , the also $(y^{″}, k^{″} | y^{'}, k^{'})$ and $(y^{'}, k^{'} | y, k)$

LaTeX Lean

Lemma 5.2.8tree count

Let $k, n, j \geq 0$ . We have for every $x \in X$

\sum_{u \in U_{1} (k, n, j)} 1_{I (u)} (x) \leq 2^{- j} 2^{9 a} \sum_{m \in M (k, n)} 1_{I (m)} (x)

5.2.19

LaTeX Lean

Lemma 7.2.1tree projection estimate

Let $u \in U$ . Then we have for all $f, g$ bounded with bounded support

| \int_{X} \sum_{p \in T (u)} \bar{g} (y) T_{p} f (y) d μ (y) |

\leq 2^{152 a^{3}} ‖ P_{J (T (u))} | f | ‖_{2} ‖ P_{L (T (u))} | g | ‖_{2} .

7.2.1

LaTeX Lean

Theorem 10.0.1two-sided metric space Carleson

For all integers $a \geq 4$ and real numbers $1 < q \leq 2$ the following holds. Let $(X, ρ, μ, a)$ be a doubling metric measure space. Let $Θ$ be a cancellative compatible collection of functions and let $K$ be a two-sided Calderón–Zygmund kernel on $(X, ρ, μ, a)$ . Assume that for every bounded measurable function $g$ on $X$ supported on a set of finite measure and all $r > 0$ we have

‖ T_{r} g ‖_{2} \leq 2^{a^{3}} ‖ g ‖_{2} .

10.0.3

Then for all Borel sets $F$ and $G$ in $X$ and all Borel functions $f : X \to C$ with $| f | \leq 1_{F}$ , we have, with $T$ defined in 1.0.17,

| \int_{G} T f d μ | \leq \frac{2^{452 a^{3}}}{(q - 1)^{6}} μ (G)^{1 - \frac{1}{q}} μ (F)^{\frac{1}{q}} .

10.0.4

LaTeX Lean

Lemma 11.1.7van der Corput

Let $α \leq β$ be real numbers. Let $g : R \to C$ be a measurable function and assume

‖ g ‖_{L i p (α, β)} := sup_{α \leq x \leq β} | g (x) | + \frac{| β - α |}{2} sup_{α \leq x < y \leq β} \frac{| g (y) - g (x) |}{| y - x |} < \infty .

11.1.19

Then for any $α \leq β$ and $n \in Z$ we have

\int_{α}^{β} g (x) e^{i n x} d x \leq 2 π | β - α | ‖ g ‖_{L i p (α, β)} (1 + | n | | β - α |)^{- 1} .

11.1.20

LaTeX Lean

Lemma 5.3.1wiggle order 1

If $n p ≲ m p^{'}$ and $n^{'} \geq n$ and $m \geq m^{'}$ then $n^{'} p ≲ m^{'} p^{'}$ .

LaTeX Lean

Lemma 5.3.2wiggle order 2

Let $n, m \geq 1$ and $k > 0$ . If $p, p^{'} \in P$ with $I (p) \neq I (p^{'})$ and

n p ≲ k p^{'}

5.3.1

then

(n + 2^{- 95 a} m) p ≲ m p^{'} .

5.3.2

LaTeX Lean

Lemma 5.3.3wiggle order 3

The following implications hold for all $q, q^{'} \in P$ :

q \leq q^{'} and λ \geq 1.1 ⟹ λ q ≲ λ q^{'},

5.3.3

10 q ≲ q^{'} and I (q) \neq I (q^{'}) ⟹ 100 q ≲ 100 q^{'},

5.3.4

2 q ≲ q^{'} and I (q) \neq I (q^{'}) ⟹ 4 q ≲ 500 q^{'} .

5.3.5

LaTeX

Lean

wiggle_order_11_10
wiggle_order_100
wiggle_order_500

Lemma 11.3.3Young convolution

Let $f$ and $g$ be two bounded non-negative measurable $2 π$ -periodic functions on $R$ . Then

{(\int_{- π}^{π} {(\int_{- π}^{π} f (y) g (x - y) d y)}^{2} d x)}^{\frac{1}{2}} \leq ‖ f ‖_{L^{2} [- π, π]} ‖ g ‖_{L^{1} [- π, π]} .

11.3.9

LaTeX Lean