Let $1<q\le 2$ be a real number. Let $\mathrm{\Theta }$ be a cancellative compatible collection of functions. By the assumption 10.0.3, we can apply Lemma 10.0.2 to obtain for every bounded measurable $g:X\to \mathbb{C}$ supported on a set of finite measure,

Define

Then $K^{\prime }$ is a two-sided Calderón–Zygmund kernel on $(X,\rho ,\mu ,a)$. Denote the corresponding maximally truncated non-tangential singular operator by $T_{\ast }^{\prime }$ and the corresponding generalized Carleson operator by $T^{\prime }$. With 10.0.6, we obtain for $g$ as above,

Applying Theorem 1.0.2 for $K^{\prime }$ yields that for all Borel sets $F$ and $G$ in $X$ and all Borel functions $f:X\to \mathbb{C}$ with $|f|\le {\mathbf{1}}_F$, we have

This finishes the proof since for all $x\in X$,

By convexity, for all $0\le \lambda \le 1$

For $\lambda :=\frac{4}{x}$, we obtain

We conclude

By definition,

We split the first integral in 10.1.1 into the domains $r\le \rho (x,y)<2r$ and $2r\le \rho (x,y)$. The integral over the first domain we estimate by $\text{(???)}$ below. For the second domain, we observe with $\rho (x,x^{\prime })\le r$ and the triangle inequality that $r\le \rho (x^{\prime },y)$. We therefore combine on this domain with the corresponding part of the second integral in 10.1.1 and estimate that by $\text{(???)}$ below. The remaining part of the second integral in 10.1.1 we estimate by $\text{(???)}$. Overall, we have estimated 10.1.1 by

Using the bound on $K$ in 1.0.14 and the doubling condition 1.0.5, we estimate 10.1.2 by

Using the definition of $Mg$, we estimate 10.1.6 by

Similarly, in the domain of 10.1.4 we note by the triangle inequality and assumption on $x^{\prime }$ that $\rho (x^{\prime },y)<3r$ and thus we estimate 10.1.4 by

We turn to the remaining term. Using 10.0.1, we estimate 10.1.3 by

We decompose and estimate 10.1.3 with the triangle inequality by

Using Lemma 10.1.1, we estimate 10.1.13 by

Summing the estimates for 10.1.2, 10.1.3, and 10.1.4 proves the lemma.

Let $x$ and $x^{\prime }$ be given with $\rho (x,x^{\prime })\le \frac{R}{4}$. By an application of Lemma 10.1.2, we estimate the left-hand-side of 10.1.15 by

We have

On the domain $R\le \rho (x^{\prime },y)$, we have $\frac{R}{2}\le \rho (x,y)$. Hence we may write for 10.1.17

Combining the estimate 10.1.16 with the identification 10.1.18, we obtain

We have

As $\frac{R}{2}\le \rho (x,y)$ together with $\rho (x,x^{\prime })\le \frac{R}{4}$ implies $\frac{R}{4}\le \rho (x^{\prime },y)$, we can estimate the absolute value of 10.1.20 with 1.0.14 by

By the triangle inequality, 10.1.15 follows now from 10.1.19 and the estimate for 10.1.20.

Let $r$, $R$, $x$ and $g$ be given. If $M(T_{r}g)(x)=0$, then $T_{r}g$ is zero almost everywhere and the estimate on $|F_1|$ is trivial. Assume $M(T_{r}g)(x)>0$. We have with 10.1.21

Dividing by $M(T_{r}g)(x)$ gives

This gives the desired bound for the measure of $F_1$. We turn to the set $F_2$. Similarly as above we may assume $Mg(x)>0$. The set $F_2$ is then estimated with Lemma 10.0.3 by

This gives the desired bound for the measure of $F_2$.

By Lemma 10.1.4, the set of all $x^{\prime }\in B(x,\frac{R}{4})$ such that at least one of the conditions 10.1.21 and 10.1.22 is satisfied has measure less than or equal to $\mu (B(x,\frac{R}{4}))/2$ and hence is not all of $B(x,\frac{R}{4})$. Pick an $x^{\prime }\in B(x,\frac{R}{4})$ such that both conditions are not satisfied. Applying Lemma 10.1.3 for this $x^{\prime }$ and using the triangle inequality estimates the left-hand side of 10.1.28 by

This proves the lemma.

With Lemma 10.1.2 and the triangle inequality, we estimate for every $x\in X$

Using further Lemma 10.1.5, we estimate

Taking the $L^2$ norm and using Proposition 2.0.6 with $a=4$ and $p_2=2$ and $p_1=1$ , we obtain

Applying 10.0.3 gives

This shows 10.1.30 and completes the proof of the lemma.

We only prove the second inequality, the first one is analogous. Note that the integrand is bounded in $X\setminus B(x,\frac{R}{2})$. So for $0<\delta \le \frac{R}{2}$,

By continuity from above of $\mu$, the right factor becomes arbitrarily small as $\delta \to 0$. Thus, for small enough $\delta$, the whole expression is $\le ϵ$.

We show two inequalities. Let $ϵ>0$. Let $R_1<R_2$ and $x^{\prime }\in B(x,R_1)$. Then for small enough $\delta >0$,

By Lemma 10.1.7, we can choose $\delta$ such that 10.1.41 is bounded by $ϵ$. Without loss of generality, we can assume $R_1+\delta <R_2$. Then 10.1.42 is bounded by the right hand side of 10.1.39 and we obtain

The inequality still holds when taking the suprema over $R_1<R_2$ and $\rho (x,x^{\prime })<R_1$ in 10.1.40. Since $ϵ>0$ was arbitrary, this proves the first inequality.

The other direction is similar. Let $ϵ>0$. Let $R_1<R_2$ and $x^{\prime }\in B(x,R_1)$. Then for $\delta >0$,

By Lemma 10.1.7, we can choose $\delta$ such that 10.1.44 is bounded by $ϵ$. Without loss of generality, we can assume $\rho (x,x^{\prime })<R_1-\delta$. Then 10.1.45 is bounded by the left hand side of 10.1.39 and we obtain

The inequality still holds when taking the suprema over $R_1<R_2$ and $\rho (x,x^{\prime })<R_1$ in 10.1.40. Since $ϵ>0$ was arbitrary, this proves the second inequality.

Fix $g$ as in the Lemma. Applying Lemma 10.1.6 with a sequence of $r$ tending to $0$ and using Lebesgue monotone convergence shows

where

We now write using Lemma 10.1.8 and the triangle inequality,

Noting that the first integral does not depend on $R_2$ and estimating the second summand by the larger supremum over all $x^{\prime }\in B(x,R_2)$, at which time the integral does not depend on $R_1$, we estimate further

Applying the triangle inequality on the left-hand side of 10.0.5 and applying 10.1.46 twice proves 10.0.5. This completes the proof of Lemma 10.0.2.

By definition, for each $x\in X$ with $Mf(x)>\alpha$, there exists a ball $B_x$ such that $x\in B_x$ and

Since $\{x\in X:Mf(x)>\alpha \}$ is open and $\mu$ is inner regular on open sets, it suffices to show that

for every compact $E\subset \{x\in X:Mf(x)>\alpha \}$. For such an $E$, by compactness, we can select a finite subcollection $\mathcal{B}\subset \{B_x:x\in E\}$ that covers $E$. By 2.0.43 applied to 10.2.2,

and hence

This follows from the Lebesgue differentiation theorem, which is already formalized in Lean.

Choose an arbitrary $x\in X$ as reference point. For $q,Q\in {\mathbb{Q}}_{+}$, let $J_{q,Q}$ denote the set of all $j\in J$ such that $B_j\subset B(x,Q)$ and $r_j\ge q$. It suffices to show that all the $J_{q,Q}$ are finite. Indeed, for all $j\in J_{q,Q}$,

Since the $B_j$ are disjoint,

and hence $|J_{q,Q}|\le 2^{a{\log }_2\lceil \frac{2Q}{q}\rceil }$.

Define for $x\in O$,

Since $O$ is open, and $O\ne X$, we have

Using Zorn’s Lemma, we select a maximal disjoint subfamily of $\{B(x,\frac{\delta (x)}{6}):x\in O\}$. We obtain a (by Lemma 10.2.3 countable) family of balls $B_j=B(x_j,\frac{\delta (x_j)}{6}),j\in J$ such that 10.2.5. 10.2.7 and $\bigcup _j{B}_j^{\ast }\subset O$ are also immediate. For the other inclusion, first observe that for $x,y\in X$, if $B(x,\frac{\delta (x)}{6})\cap B(y,\frac{\delta (y)}{6})\ne \mathrm{\varnothing }$, then

so

Now let $z\in X$. By maximality, there exists some $j\in J$ with $B(z,\frac{\delta (z)}{6})\cap B_j\ne \mathrm{\varnothing }$. By 10.2.10,

and thus $z\in B_j^{\ast }$.

We now turn to the bounded intersection property. Assume that for some $j_1,\dots ,j_N$,

Similarly as above, observe for $1\le k\le N$,

and

so

By 10.2.12 and 10.2.13, for all $1\le k\le N$, $B(z,\frac{\delta (z)}{6})\subset B(x_{j_k},5r_{j_k})$ and $B_{j_k}\subset B(z,\frac{8\delta (z)}{6})$. Using this and 10.2.5, we obtain