Proof. By convexity, for all 0\le\lambda\le1, 2^{\lambda(-\frac14)}\le \lambda 2^{-\frac14}+(1-\lambda)2^0. For \lambda:=\frac4x, we obtain 2^{-\frac1x}\le 1-(1-2^{-\frac14})\frac4x. We conclude \sum_{n=0}^\infty 2^{-\frac nx} =\frac1{1-2^{-\frac1x}} \le\frac1{4(1-2^{-\frac14})}x\le2^x.

Proof. By definition, \left|T_rg(x)-T_rg(x')\right| =\left|\int_{r\le\rho(x,y)}K(x,y)g(y)\,d\mu(y) -\int_{r\le\rho(x',y)}K(x',y)g(y)\,d\mu(y)\right|. We split the first integral into the domains r\le\rho(x,y)<2r and 2r\le\rho(x,y). The integral over the first domain is estimated by \int_{r\le\rho(x,y)<2r}|K(x,y)||g(y)|\,d\mu(y). For the second domain, \rho(x,x')\le r and the triangle inequality imply r\le\rho(x',y). We therefore combine it with the corresponding part of the second integral and estimate it by \left|\int_{2r\le\rho(x,y)}(K(x,y)-K(x',y))g(y)\,d\mu(y)\right|. The remaining part of the second integral is estimated by \int_{r\le\rho(x',y),\ r\le\rho(x,y)<2r}|K(x',y)||g(y)|\,d\mu(y).

Using the bound on K and the doubling condition, the first term is at most \frac{2^{a^3}}{\mu(B(x,r))} \int_{r\le\rho(x,y)<2r}|g(y)|\,d\mu(y) \le \frac{2^{a^3}2^a}{\mu(B(x,2r))} \int_{\rho(x,y)<2r}|g(y)|\,d\mu(y) \le 2^{a^3+a}Mg(x). Similarly, on the domain of the third term the triangle inequality and the assumption on x' give \rho(x',y)<3r, so that term is at most \frac{2^{a^3}}{\mu(B(x',r))} \int_{\rho(x',y)<4r}|g(y)|\,d\mu(y) \le 2^{a^3+2a}Mg(x).

For the remaining term, kernel smoothness gives \int_{2r\le\rho(x,y)} \left(\frac{\rho(x,x')}{\rho(x,y)}\right)^{\frac1a} \frac{2^{a^3}}{V(x,y)}|g(y)|\,d\mu(y). Decomposing into dyadic annuli and using the triangle inequality bounds this by \begin{aligned} &\sum_{j=1}^\infty\int_{2^jr\le\rho(x,y)<2^{j+1}r} \left(\frac{\rho(x,x')}{\rho(x,y)}\right)^{\frac1a} \frac{2^{a^3}}{V(x,y)}|g(y)|\,d\mu(y)\\ &\quad\le \sum_{j=1}^\infty 2^{-\frac ja} \frac{2^{a^3+a}}{\mu(B(x,2^{j+1}r))} \int_{\rho(x,y)<2^{j+1}r}|g(y)|\,d\mu(y)\\ &\quad\le 2^{a^3+a}\sum_{j=1}^\infty2^{-\frac ja}Mg(x) \le 2^{a^3+2a}Mg(x), \end{aligned} where the last step uses Lemma 1.10.1.1. Summing the three estimates proves the lemma.

Proof. Let x and x' be given with \rho(x,x')\le\frac R4. By Lemma 1.10.1.2, |T_Rg(x)|\le |T_Rg(x')|+2^{a^3+2a+2}Mg(x). We have T_Rg(x')=\int_{R\le\rho(x',y)}K(x',y)g(y)\,d\mu(y). On this domain, \frac R2\le\rho(x,y), hence \begin{aligned} T_Rg(x') &=\int_{R\le\rho(x',y)}K(x',y) \left(g-g\mathbf{1}_{B(x,\frac R2)}\right)(y)\,d\mu(y)\\ &=T_R\left(g-g\mathbf{1}_{B(x,\frac R2)}\right)(x'). \end{aligned} It follows that |T_Rg(x)|\le \left|T_R\left(g-g\mathbf{1}_{B(x,\frac R2)}\right)(x')\right| +2^{a^3+2a+2}Mg(x). Moreover, \begin{aligned} &(T_r-T_R)\left(g-g\mathbf{1}_{B(x,\frac R2)}\right)(x')\\ &\quad=\int_{B(x',R)\setminus B(x',r)}K(x',y) \left(g-g\mathbf{1}_{B(x,\frac R2)}\right)(y)\,d\mu(y)\\ &\quad=\int_{B(x',R)\setminus(B(x',r)\cup B(x,\frac R2))} K(x',y)g(y)\,d\mu(y). \end{aligned} Since \frac R2\le\rho(x,y) together with \rho(x,x')\le\frac R4 implies \frac R4\le\rho(x',y), the absolute value of this integral is at most \begin{aligned} &\frac{2^{a^3}}{\mu(B(x',\frac R4))} \int_{B(x,2R)\setminus B(x',\frac R4)}|g(y)|\,d\mu(y)\\ &\quad\le \frac{2^{a^3+a}}{\mu(B(x',\frac R2))} \int_{B(x,2R)}|g(y)|\,d\mu(y)\\ &\quad\le 2^{a^3+a} \frac{\mu(B(x,2R))}{\mu(B(x,\frac R4))}Mg(x) \le 2^{a^3+4a}Mg(x). \end{aligned} The triangle inequality now proves the lemma.

Proof. Let r, R, x, and g be given. If M(T_rg)(x)=0, then T_rg is zero almost everywhere and the estimate for F_1 is trivial. Assume M(T_rg)(x)>0. Then \begin{aligned} M(T_rg)(x) &\ge \frac1{\mu(B(x,\frac R4))} \int_{B(x,\frac R4)}|T_rg(x')|\,dx'\\ &\ge \frac1{\mu(B(x,\frac R4))} \int_{F_1}4M(T_rg)(x)\,dx'. \end{aligned} Dividing by M(T_rg)(x) gives 1\ge\frac4{\mu(B(x,\frac R4))}\mu(F_1), which is the desired bound for F_1.

For F_2, we may similarly assume Mg(x)>0. By Lemma 1.10.3, its measure is at most \frac{2^{a^3+19a}}{2^{a^3+20a+2}Mg(x)} \int\left|g\mathbf{1}_{B(x,\frac R2)}\right|(y)\,d\mu(y) \le \frac1{2^{a+2}Mg(x)}\mu(B(x,\tfrac R2))Mg(x) \le\frac{\mu(B(x,\frac R4))}{4}. This proves the desired bound for F_2.

Proof. By Lemma 1.10.1.4, the set of all x'\in B(x,\frac R4) such that at least one of the two exceptional conditions is satisfied has measure less than or equal to \mu(B(x,\frac R4))/2, and hence is not all of B(x,\frac R4). Pick an x'\in B(x,\frac R4) such that both conditions are not satisfied. Applying Lemma 1.10.1.3 for this x' and using the triangle inequality estimates the left-hand side of the Cotlar estimate by 4M(T_rg)(x)+2^{a^3+20a+2}Mg(x)+2^{a^3+4a+1}Mg(x). This proves the lemma.

Proof. For fixed \lambda, rewriting x'\in B(x,R) as x\in B(x',R) gives \{x:T_*^rg(x)>\lambda\} =\bigcup_{r<R}\bigcup_{\{x':|T_Rg(x')|>\lambda\}}B(x',R). The right-hand side is open, hence T_*^rg is lower-semicontinuous by definition.

For the second part, Lemma 1.10.1.2 and the triangle inequality give, for every x\in X, T_*^rg(x)\le 2^{a^3+2a+2}Mg(x)+\sup_{r<R}|T_Rg(x)|. Using Lemma 1.10.1.5 further gives T_*^rg(x) \le 2^{a^3+2a+2}Mg(x)+2^{a^3+20a+3}Mg(x)+2^2M(T_rg)(x). Taking the L^2 norm and applying Theorem 1.2.6 with a=4, p_2=2, and p_1=1, we obtain \begin{aligned} \|T_*^rg\|_2 &\le 2^{a^3+20a+4}\|Mg\|_2+2^2\|M(T_rg)\|_2\\ &\le 2^{a^3+24a+5}\|g\|_2+2^{4a+3}\|T_rg\|_2. \end{aligned} The assumed T_r bound now gives \|T_*^rg\|_2 \le 2^{a^3+24a+5}\|g\|_2+2^{a^3+4a+3}\|g\|_2, which proves the claimed inequality.

Proof. We prove only the second inequality; the first is analogous. The integrand is bounded in X\setminus B(x,\frac R2). Thus, for 0<\delta\le\frac R2, its absolute value is at most \frac{2^{a^3}}{\mu(B(x,\frac R2))}\sup_{y\in X}|f(x)| \cdot\mu\bigl(\{y\in X:R-\delta<\rho(x,y)<R\}\bigr). By continuity from above of \mu, the right factor becomes arbitrarily small as \delta\to0. Hence, for sufficiently small \delta, the whole expression is at most \epsilon.

Proof. We prove two inequalities. Let \epsilon>0, R_1<R_2, and x'\in B(x,R_1). For sufficiently small \delta>0, \begin{aligned} &\left|\int_{R_1<\rho(x',y)<R_2}K(x',y)f(y)\,d\mu(y)\right|\\ &\quad\le \left|\int_{R_1<\rho(x',y)<R_1+\delta}K(x',y)f(y)\,d\mu(y)\right|\\ &\qquad+ \left|\int_{R_1+\delta\le\rho(x',y)<R_2}K(x',y)f(y)\,d\mu(y)\right|. \end{aligned} By Lemma 1.10.1.7, choose \delta so that the first term on the right is at most \epsilon; we may assume R_1+\delta<R_2. The second term is bounded by the right-hand side of the claimed equality. Thus the expression is at most \epsilon+\sup_{R_1<R_2}\sup_{x'\in B(x,R_1)} \left|\int_{B(x',R_2)\setminus B(x',R_1)}K(x',y)f(y)\,d\mu(y)\right|. The inequality remains true after taking the suprema over R_1<R_2 and \rho(x,x')<R_1. Since \epsilon is arbitrary, this proves the first inequality.

For the other direction, let again \epsilon>0, R_1<R_2, and x'\in B(x,R_1). For \delta>0, \begin{aligned} &\left|\int_{B(x',R_2)\setminus B(x',R_1)}K(x',y)f(y)\,d\mu(y)\right|\\ &\quad\le \left|\int_{R_1-\delta<\rho(x',y)<R_1}K(x',y)f(y)\,d\mu(y)\right|\\ &\qquad+ \left|\int_{R_1-\delta<\rho(x',y)<R_2}K(x',y)f(y)\,d\mu(y)\right|. \end{aligned} By Lemma 1.10.1.7, choose \delta so that the first term on the right is at most \epsilon; we may assume \rho(x,x')<R_1-\delta. The second term is bounded by the left-hand side of the claimed equality. Hence the expression is at most \epsilon+\sup_{R_1<R_2}\sup_{x'\in B(x,R_1)} \left|\int_{R_1<\rho(x',y)<R_2}K(x',y)f(y)\,d\mu(y)\right|. Taking the same suprema and letting \epsilon tend to zero proves the second inequality.

Proof of Lemma 1.10.2. Fix g as in the lemma. Applying Lemma 1.10.1.6 with a sequence of r tending to zero and using Lebesgue monotone convergence gives \|T_*^0g\|_2\le 2^{a^3+24a+6}\|g\|_2, where T_*^0g(x):=\sup_{0<R}\sup_{x'\in B(x,R)} \left|\int_{X\setminus B(x',R)}K(x',y)g(y)\,d\mu(y)\right|. By Lemma 1.10.1.8 and the triangle inequality, \begin{aligned} T_*g(x) &\le\sup_{0<R_1<R_2}\sup_{x'\in B(x,R_1)} \left|\int_{X\setminus B(x',R_1)}K(x',y)g(y)\,d\mu(y)\right|\\ &\quad+\sup_{0<R_1<R_2}\sup_{x'\in B(x,R_1)} \left|\int_{X\setminus B(x',R_2)}K(x',y)g(y)\,d\mu(y)\right|. \end{aligned} The first integral does not depend on R_2. In the second summand, enlarge the supremum to all x'\in B(x,R_2), after which the integral does not depend on R_1. Therefore \begin{aligned} T_*g(x) &\le\sup_{0<R_1}\sup_{x'\in B(x,R_1)} \left|\int_{X\setminus B(x',R_1)}K(x',y)g(y)\,d\mu(y)\right|\\ &\quad+\sup_{0<R_2}\sup_{x'\in B(x,R_2)} \left|\int_{X\setminus B(x',R_2)}K(x',y)g(y)\,d\mu(y)\right|. \end{aligned} Applying the triangle inequality to the L^2 norm and the bound for T_*^0g twice proves the claimed estimate and completes the proof.

Proof. By definition, for each x\in X with Mf(x)>\alpha, there is a ball B_x containing x such that \alpha\mu(B_x)<\int_{B_x}|f(y)|\,d\mu(y). Since \{x\in X:Mf(x)>\alpha\} is open and \mu is inner regular on open sets, it suffices to prove \mu(E)\le\frac{2^{2a}}{\alpha}\int|f(y)|\,d\mu(y) for every compact E contained in this set. By compactness, choose a finite subcollection \mathcal B\subset\{B_x:x\in E\} covering E. Applying the finite ball-union estimate gives \alpha\mu\left(\bigcup\mathcal B\right) \le2^{2a}\int|f(y)|\,d\mu(y). Consequently, \mu(E)\le\mu\left(\bigcup\mathcal B\right) \le\frac{2^{2a}}{\alpha}\int|f(y)|\,d\mu(y).

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

Proof. Choose an arbitrary x\in X as reference point. For q,Q\in\mathbb Q_+, let J_{q,Q} be the set of all j\in J such that B_j\subset B(x,Q) and r_j\ge q. It suffices to prove that all J_{q,Q} are finite. Indeed, for every j\in J_{q,Q}, \mu(B(x,Q)) \le\mu(B(x_j,2Q)) =\mu\left(B\left(x_j,\frac{2Q}{r_j}r_j\right)\right) \le2^{a\log_2\left\lceil\frac{2Q}{r_j}\right\rceil}\mu(B_j). Since the balls B_j are disjoint, |J_{q,Q}|\mu(B(x,Q)) \le2^{a\log_2\left\lceil\frac{2Q}{q}\right\rceil} \sum_{j\in J_{q,Q}}\mu(B_j) \le2^{a\log_2\left\lceil\frac{2Q}{q}\right\rceil}\mu(B(x,Q)), and hence |J_{q,Q}|\le2^{a\log_2\lceil2Q/q\rceil}.

Proof. For x\in O, define \delta(x):=\sup\{\delta\in\mathbb R:B(x,\delta)\subset O\}. Since O is open and O\ne X, we have 0<\delta(x)<\infty. By Zorn's lemma, choose a maximal disjoint subfamily of \{B(x,\delta(x)/6):x\in O\}. By Lemma 1.10.2.3, this gives a countable family B_j=B(x_j,\delta(x_j)/6), j\in J. Pairwise disjointness, B_{7,j}\cap(X\setminus O)\ne\emptyset, and \bigcup_jB_{3,j}\subset O are immediate.

For the reverse inclusion, if B(x,\delta(x)/6)\cap B(y,\delta(y)/6)\ne\emptyset, then \delta(x)\le\rho(x,y)+\delta(y) \le\frac{\delta(x)}6+\frac{7\delta(y)}6, so \delta(x)\le2\delta(y). Given z\in O, maximality yields some j\in J with B(z,\delta(z)/6)\cap B_j\ne\emptyset. Hence \rho(z,x_j)<\frac{\delta(z)}6+\frac{\delta(x_j)}6 \le\frac{3\delta(x_j)}6=3r_j, so z\in B_{3,j}.

For bounded intersection, suppose z\in\bigcap_{k=1}^NB_{3,j_k}. For 1\le k\le N, we have \delta(z)\le\rho(z,x_{j_k})+\delta(x_{j_k}) \le\frac{3\delta(x_{j_k})}{2} and \delta(x_{j_k})\le\rho(x_{j_k},z)+\delta(z) \le\frac{\delta(x_{j_k})}{2}+\delta(z), so \delta(x_{j_k})\le2\delta(z). Thus B(z,\delta(z)/6)\subset B(x_{j_k},5r_{j_k}) and B_{j_k}\subset B(z,8\delta(z)/6). Using pairwise disjointness, \begin{aligned} N\mu(B(z,\tfrac{\delta(z)}6)) &\le\sum_{k=1}^N\mu(B(x_{j_k},5r_{j_k}))\\ &\le2^{3a}\sum_{k=1}^N\mu(B_{j_k})\\ &\le2^{3a}\mu(B(z,\tfrac{8\delta(z)}6))\\ &\le2^{6a}\mu(B(z,\tfrac{\delta(z)}6)). \end{aligned} Therefore N\le2^{6a}.