fix decls

.github/workflows/push.yml

@@ -80,7 +80,7 @@ jobs:
 
       - name: Install blueprint dependencies
         run: |
-          pip install -r blueprint/requirements.txt
+          cd blueprint && pip install -r requirements.txt
 
       - name: Build blueprint and copy to `docs/blueprint`
         run: |

blueprint/src/chapter/main.tex

@@ -582,7 +582,7 @@ \chapter{Proof of Metric Space Carleson, overview}
 \begin{proposition}[Hardy--Littlewood]
 \label{Hardy-Littlewood}
 \leanok
-\lean{measure_biUnion_le_lintegral, maximalFunction_lt_top, snorm_maximalFunction, M_lt_top,
+\lean{measure_biUnion_le_lintegral, maximalFunction_le_snorm, hasStrongType_maximalFunction, M_lt_top,
   laverage_le_M, snorm_M_le}
 \uses{layer-cake-representation,covering-separable-space}
    Let $\mathcal{B}$ be a finite collection of balls in $X$.
@@ -6055,7 +6055,7 @@ \chapter{Proof of Vitali covering and Hardy--Littlewood}
 We begin with a classical representation of the Lebesgue norm.
 \begin{lemma}[layer cake representation]\label{layer-cake-representation}
 \leanok
-\lean{snorm_pow_eq_distribution}
+\lean{MeasureTheory.snorm_pow_eq_distribution}
 Let $1\le p< \infty$. Then for any measurable function $u:X\to [0,\infty)$ on the measure space $X$
 relative to the measure $\mu$
 we have
@@ -6408,7 +6408,7 @@ \section{The classical Carleson theorem}
 \begin{lemma}[smooth approximation]
     \label{smooth-approximation}
     \leanok
-    \lean{}
+    % \lean{}
     The function $f_0$ is $2\pi$-periodic.
     The function $f_0$ is smooth (and therefore measurable).
     The function $f_0$ satisfies for all $x\in \R$:
@@ -6426,7 +6426,7 @@ \section{The classical Carleson theorem}
 \begin{lemma}[convergence for smooth]
     \label{convergence-for-smooth}
     \leanok
-    \lean{}
+    % \lean{}
     \uses{convergence-for-twice-contdiff}
     There exists some $N_0 \in \N$ such that for all $N>N_0$ and $x\in [0,2\pi]$ we have
     \begin{equation}
@@ -6438,7 +6438,7 @@ \section{The classical Carleson theorem}
 \begin{lemma}[control approximation effect]
     \label{control-approximation-effect}
     \leanok
-    \lean{}
+    % \lean{}
     \uses{real-Carleson}
     There is a set $E \subset \R$ with Lebesgue measure
     $|E|\le \epsilon$ such that for all
@@ -6492,7 +6492,7 @@ \section{The classical Carleson theorem}
  \Cref{metric-space-Carleson}.
 \begin{lemma}[real Carleson]\label{real-Carleson}
 \leanok
-\lean{}
+% \lean{}
 \uses{metric-space-Carleson,real-line-metric,real-line-measure,real-line-doubling,oscillation-control,frequency-monotone,frequency-ball-doubling,frequency-ball-growth,integer-ball-cover,real-van-der-Corput,nontangential-Hilbert}
     Let $F,G$ be Borel subsets of $\R$ with finite measure. Let $f$ be a bounded measurable function on $\R$ with $|f|\le \mathbf{1}_F$. Then
 \begin{equation}
@@ -6680,7 +6680,7 @@ \section{The classical Carleson theorem}
 \begin{lemma}[Hilbert kernel bound]
 \label{Hilbert-kernel-bound}
 \leanok
-\lean{}
+% \lean{}
 \uses{lower-secant-bound}
     For $x,y\in \R$ with $x\neq y$ we have
     \begin{equation}\label{eqcarl30}
@@ -6705,7 +6705,7 @@ \section{The classical Carleson theorem}
 \begin{lemma}[Hilbert kernel regularity]
 \label{Hilbert-kernel-regularity}
 \leanok
-\lean{}
+% \lean{}
 \uses{lower-secant-bound}
     For $x,y,y'\in \R$ with $x\neq y,y'$ and
     \begin{equation}
@@ -6764,7 +6764,7 @@ \section{Smooth functions.}
 \begin{lemma}
 \label{fourier-coeff-derivative}
 \leanok
-\lean{}
+% \lean{}
 Let $f:\R \to \C$ be $2\pi$-periodic and differentiable, and let $n \in \Z \setminus \{0\}$. Then
 \begin{equation}
     \widehat{f}_n = \frac{1}{i n} \widehat{f'}_n.
@@ -6778,7 +6778,7 @@ \section{Smooth functions.}
 \begin{lemma}
 \label{convergence-of-coeffs-summable}
 \leanok
-\lean{}
+% \lean{}
 Let $f:\R \to \C$ such that
 \begin{equation}
     \sum_{n\in \Z} |\widehat{f}_n| < \infty.
@@ -6799,7 +6799,7 @@ \section{Smooth functions.}
     \label{convergence-for-twice-contdiff}
     \uses{fourier-coeff-derivative,convergence-of-coeffs-summable}
     \leanok
-    \lean{}
+    % \lean{}
     Let $f:\R \to \C$ be $2\pi$-periodic and twice continuously differentiable. Then
     \begin{equation}
         \sup_{x\in [0,2\pi]} |f(x) - S_Nf(x)| \rightarrow 0