Let \(1{\lt}q\le 2\) be a real number. Let \(\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'\) is a two-sided Calderón–Zygmund kernel on \((X,\rho ,\mu ,a)\). Denote the corresponding maximally truncated non-tangential singular operator by \(T_*'\) and the corresponding generalized Carleson operator by \(T'\). With 10.0.6, we obtain for \(g\) as above,

Applying Theorem 1.0.2 for \(K'\) 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){\lt}2r\) and \(2r\le \rho (x,y)\). The integral over the first domain we estimate by \(\eqref{firstxx'}\) below. For the second domain, we observe with \(\rho (x,x')\le r\) and the triangle inequality that \(r\le \rho (x',y)\). We therefore combine on this domain with the corresponding part of the second integral in 10.1.1 and estimate that by \(\eqref{secondxx'}\) below. The remaining part of the second integral in 10.1.1 we estimate by \(\eqref{thirdxx'}\). 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'\) that \(\rho (x',y){\lt}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'\) be given with \(\rho (x,x')\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',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')\le \frac{R}{4}\) implies \(\frac{R}{4}\le \rho (x',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_rg)(x)=0\), then \(T_rg\) is zero almost everywhere and the estimate on \(|F_1|\) is trivial. Assume \(M(T_rg)(x){\gt}0\). We have with 10.1.21

Dividing by \(M(T_rg)(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){\gt}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'\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'\in B(x,\frac{R}4)\) such that both conditions are not satisfied. Applying Lemma 10.1.3 for this \(x'\) 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 inquality, the first one is analogous. Note that the integrand is bounded in \(X\setminus B(x,\frac{R}{2})\). So for \(0{\lt}\delta \le \frac{R}{2}\),

By continuity from above of \(\mu \), the right factor becomes arbitrarily small as \(\delta \rightarrow 0\). Thus, for small enough \(\delta \), the whole expression is \(\le \epsilon \).

We show two inequalities. Let \(\epsilon {\gt}0\). Let \(R_1{\lt}R_2\) and \(x'\in B(x,R_1)\). Then for small enough \(\delta {\gt}0\),

By Lemma 10.1.7, we can choose \(\delta \) such that 10.1.41 is bounded by \(\epsilon \). Without loss of generality, we can assume \(R_1+\delta {\lt}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{\lt}R_2\) and \(\rho (x,x'){\lt}R_1\) in 10.1.40. Since \(\epsilon {\gt}0\) was arbitrary, this proves the first inequality.

The other direction is similar. Let \(\epsilon {\gt}0\). Let \(R_1{\lt}R_2\) and \(x'\in B(x,R_1)\). Then for \(\delta {\gt}0\),

By Lemma 10.1.7, we can choose \(\delta \) such that 10.1.44 is bounded by \(\epsilon \). Without loss of generality, we can assume \(\rho (x,x'){\lt}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{\lt}R_2\) and \(\rho (x,x'){\lt}R_1\) in 10.1.40. Since \(\epsilon {\gt}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'\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) {\gt} \alpha \), there exists a ball \(B_x\) such that \(x\in B_x\) and

Since \(\{ x\in X : Mf(x) {\gt} \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) {\gt} \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^* \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 \emptyset \), 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 \emptyset \). By 10.2.10,

and thus \(z\in B_j^*\).

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

and conclude \(N\le 2^{6a}\).

Let \(E_\alpha :=\{ x\in X: Mf(x){\gt}\alpha \} \). Then \(E_\alpha \) is open. Assume first that \(E_\alpha \ne X\). We apply Lemma 10.2.4 with \(O=E_\alpha \) to obtain the family \(B_j, j\in J,\). Without loss of generality, we can assume \(J={\mathbb {N}}\). Define inductively

Then \(B_j\subset Q_j\subset B_j^*\), the \(Q_j\) are pairwise disjoint and \(\bigcup _j Q_j = E_\alpha \). Define

and, for each \(j\),

Then 10.2.16, 10.2.19 and 10.2.20 are true by construction. For 10.2.17, we first do the case \(x\in X\setminus E_\alpha \). By definition of \(Mf\),

for every ball \(B\subset X\) with \(x\in B\). It follows by Lemma 10.2.2 that for almost every \(x\in X\setminus E_\alpha \), \(|f(x)|\le \alpha \). In the case \(x\in E_\alpha \), there exists some \(j\in J\) with \(x\in Q_j\) and we have that

because \(B_j^{**}\cap (X\setminus E_\alpha ) \ne \emptyset \). We get

To prove 10.2.18, we estimate

Using the triangle inequality, we have that

With 10.2.30, we estimate further

to obtain 10.2.21. Further, summing up 10.2.32 in \(j\) yields 10.2.23. At last, we estimate with Lemma 10.2.1

proving 10.2.22.

Assume now that \(E_\alpha = X\). It follows from Lemma 10.2.1 that then \(\mu (X){\lt}\infty \). Define

and

Then \(f = g + b_1\) and \(\operatorname{\operatorname {supp}}b_1 \subset B_1^*:=X\) and 10.2.16, 10.2.18, 10.2.19, 10.2.20 all hold immediately. By assumption, \(\alpha {\gt}\frac{1}{\mu (X)}\int |f|\, d\mu = g\), so 10.2.17 holds. We also have, using the definitions and the same assumption,

which verifies both 10.2.23 and 10.2.21. Finally, by Lemma 10.2.1,

which shows 10.2.22.

We estimate using monotonicity of the integral

Using 10.0.8 followed by 10.2.17 and 10.2.18, we estimate the right hand side above by

We decompose the index set \(J\) into the following disjoint sets:

Then

For all \(j\in \mathcal{J}_3(x)\), \(\operatorname{\operatorname {supp}}b_j\subset B_j\subset B(x,r)\), and thus \(T_rb_j(x)=0\), so \(\eqref{eq-b-dec-3} = 0\).

Next, for \(j\in \mathcal{J}_1(x)\), \(\operatorname{\operatorname {supp}}b_j\subset B_j\subset X \setminus B(x,r)\), and we have

Using 10.2.20, the above is equal to

Since \(x\in X\setminus \Omega \), we have for each \(y\in B_j\) that

so we can apply 1.0.15 to estimate

and by 10.2.21,

Next, we estimate 10.2.44. For each \(j\in \mathcal{J}_2(x)\), set

Then by 10.2.21

For each \(j\in \mathcal{J}_2(x)\), we have

Thus, using the triangle inequality, the equation above and 10.2.49, we obtain

By 10.2.46, we can apply 1.0.15 and arguing as in 10.2.48, we get that

with \(F\) as in 10.2.48. Define

We claim that

Indeed, for each \(j\in \mathcal{J}_2(x)\) and \(y\in B_j\), using again 10.2.46,

and hence

For the lower bound, we observe

and conclude

Using the bounded intersection property of the \(B_j\), 10.2.52 and 1.0.14, we get

Combining the estimates 10.2.48 for 10.2.43, 10.2.51 for 10.2.44, and 10.2.58, we get

By the definition 10.2.37 of \(c\), this equals

We estimate

Using

we have for all \(j\in J\),

where we used Lemma 10.1.1 in the last step. Plugging this into 10.2.62 and using 10.2.22, we conclude that

We estimate

Using 10.2.40 and 10.2.22, we conclude that

It follows from Lemma 10.2.7 and the triangle inequality that

The claim now follows from 10.2.63, 10.2.65 and 10.2.59.

It follows by the triangle inequality and subadditivity of \(\mu \) that

Using Lemma 10.2.6, Lemma 10.2.9 and the definition 10.2.37 of \(c\), we get

This proves 10.0.9.