Setup blueprint

.github/workflows/blueprint.yml

@@ -0,0 +1,105 @@
+on:
+  push:
+    branches:
+      - master
+
+# Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages
+permissions:
+  contents: read
+  pages: write
+  id-token: write
+
+jobs:
+  build_project:
+    runs-on: ubuntu-latest
+    name: Build project
+    steps:
+      - name: Checkout project
+        uses: actions/checkout@v2
+        with:
+          fetch-depth: 0
+
+      - name: Install elan
+        run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover/lean4:4.5.0
+
+      - name: Update docgen4
+        run: ~/.elan/bin/lake -R -Kenv=dev update «doc-gen4»
+
+      - name: Update checkdecls
+        run: ~/.elan/bin/lake update checkdecls
+
+      - name: Get cache
+        run: ~/.elan/bin/lake -R -Kenv=dev exe cache get || true
+
+      - name: Build project
+        run: ~/.elan/bin/lake -R -Kenv=dev build FLT3
+
+      - name: Cache mathlib docs
+        uses: actions/cache@v3
+        with:
+          path: |
+            .lake/build/doc/Init
+            .lake/build/doc/Lake
+            .lake/build/doc/Lean
+            .lake/build/doc/Std
+            .lake/build/doc/Mathlib
+            .lake/build/doc/declarations
+            !.lake/build/doc/declarations/declaration-data-FLT3*
+          key: MathlibDoc-${{ hashFiles('lake-manifest.json') }}
+          restore-keys: |
+            MathlibDoc-
+
+      - name: Build documentation
+        run: ~/.elan/bin/lake -R -Kenv=dev build FLT3:docs
+
+      - name: Build blueprint and copy to `docs/blueprint`
+        uses: xu-cheng/texlive-action@v2
+        with:
+          docker_image: ghcr.io/xu-cheng/texlive-full:20231201
+          run: | # "mkdir docs" before "cp blueprint/print/print.pdf docs/blueprint.pdf"
+            apk update
+            apk add --update make py3-pip git pkgconfig graphviz graphviz-dev gcc musl-dev
+            git config --global --add safe.directory $GITHUB_WORKSPACE
+            git config --global --add safe.directory `pwd`
+            python3 -m venv env
+            source env/bin/activate
+            pip install --upgrade pip requests wheel
+            pip install pygraphviz --global-option=build_ext --global-option="-L/usr/lib/graphviz/" --global-option="-R/usr/lib/graphviz/"
+            pip install leanblueprint
+            leanblueprint pdf
+            cp blueprint/print/print.pdf docs/blueprint.pdf
+            leanblueprint web
+            cp -r blueprint/web docs/blueprint
+
+      - name: Check declarations
+        run: |
+            ~/.elan/bin/lake exe checkdecls blueprint/lean_decls
+
+      - name: Move documentation to `docs/docs`
+        run: |
+          sudo chown -R runner docs
+          cp -r .lake/build/doc docs/docs
+
+      - name: Bundle dependencies
+        uses: ruby/setup-ruby@v1
+        with:
+          working-directory: docs
+          ruby-version: "3.0" # Not needed with a .ruby-version file
+          bundler-cache: true # runs 'bundle install' and caches installed gems automatically
+
+      - name: Bundle website
+        working-directory: docs
+        run: JEKYLL_ENV=production bundle exec jekyll build
+
+      - name: Upload docs & blueprint artifact
+        uses: actions/upload-pages-artifact@v1
+        with:
+          path: docs/_site
+
+      - name: Deploy to GitHub Pages
+        id: deployment
+        uses: actions/deploy-pages@v1
+
+      - name: Make sure the cache works
+        run: |
+          mv docs/docs .lake/build/doc

.gitignore

@@ -9,3 +9,6 @@
 /lakefile.olean
 # After v4.3.0-rc2 lake stores its files here:
 /.lake/
+# Python virtual environment 
+/.venv/
+references.md

README.md

@@ -1,3 +1,3 @@
- Proof in Lean of Fermat Last Theorem for exponent 3 
- 
+Formalisation of Fermat's Last Theorem (FLT) for Exponent 3 in Lean
+
 <a href='https://codespaces.new/riccardobrasca/flt3' target="_blank" rel="noreferrer noopener"><img src='https://github.com/codespaces/badge.svg' alt='Open in GitHub Codespaces' style='max-width: 100%;'></a>

blueprint/.gitignore

@@ -0,0 +1,16 @@
+*.pdf
+*.paux
+*.aux
+*.log
+print
+web
+__pycache__
+*.fdb_latexmk
+*.fls
+*.out
+*.synctex.gz
+*.xdv
+*.maf
+*.mtc
+*.mtc0
+build

blueprint/requirements.txt

@@ -0,0 +1,8 @@
+# https://github.com/pyinvoke/invoke/issues/891
+invoke==2.2.0
+plasTeX @ git+https://github.com/plastex/plastex.git
+plastexdepgraph @ git+https://github.com/PatrickMassot/plastexdepgraph.git
+plastexshowmore @ git+https://github.com/PatrickMassot/plastexshowmore.git
+leanblueprint @ git+https://github.com/PatrickMassot/leanblueprint.git
+watchfiles==0.16.1
+pandoc==2.3

blueprint/src/chapter/ap.tex

@@ -0,0 +1,185 @@
+\chapter{Almost-Periodicity}
+\label{chap:ap}
+
+
+\begin{lemma}[Marcinkiewicz-Zygmund inequality]
+\label{mzi}
+\lean{other_marcinkiewicz_zygmund'}
+\leanok
+Let $m\geq 1$. If $f:G\to\bbr$ is such that $\bbe_x f(x)=0$ and $\abs{f(x)}\leq 2$ for all $x$ then
+\[\bbe_{x_1,\ldots,x_n} \abs{\sum_{i=1}^n f(x_i)}^{2m} \leq (4mn)^{m}.\]
+\end{lemma}
+
+\begin{proof}
+\leanok
+Let $S$ be the left-hand side. Since $0=\bbe_y f(y)$ we have, by the triangle inequality, and H\"{o}lder's inequality,
+\[S=\bbe_{x_1,\ldots,x_n}\left\lvert \sum_i f(x_i) - \bbe_{y_i} f(y_i)\right\rvert^{2m} = \bbe_{x_1,\ldots,x_n} \left\lvert\bbe_{y_i}\brac{\sum_i f(x_i)-f(y_i)}\right\rvert^{2m}\leq \bbe_{x_1,\dots,y_n} \left\lvert \sum_i f(x_i)-f(y_i)\right\rvert^{2m}.\]
+Changing the role of $x_i$ and $y_i$ makes no difference here, but multiplies the $i$ summand by $\{-1,+1\}$, and therefore for any $\epsilon_i\in\{-1,+1\}$,
+\[ S \leq\bbe_{x_1,\ldots,y_n}\left\lvert \sum_i \epsilon_i(f(x_i)-f(y_i))\right\rvert^{2m}.\]
+In particular, if we sample $\epsilon_i\in\{-1,+1\}$ uniformly at random, then
+\[ S \leq\bbe_{\epsilon_i} \bbe_{x_1,\ldots,y_n}\left\lvert \sum_i \epsilon_i(f(x_i)-f(y_i))\right\rvert^{2m}.\]
+We now change the order of expectation and consider the expectation over just $\epsilon_i$, viewing the $f(x_i)-f(y_i)=z_i$, say, as fixed quantities. For any $z_i$ we can expand $\bbe_{\epsilon_i} \lvert \sum_i \epsilon_iz_i\rvert^{2m}$ and then bound it from above, using the triangle inequality and $\abs{z_i}\leq 4$, by
+\[4^{2m}\sum_{k_1+\cdots+k_n=2m}\binom{2m}{k_1,\ldots,k_n}\abs{\bbe\epsilon_1^{k_1}\cdots \epsilon_n^{k_n}}.\]
+The inner expectation vanishes unless each $k_i$ is even, when it is trivially one. Therefore the above quantity is exactly
+\[\sum_{l_1+\cdots+l_n=m}\binom{2m}{2l_1,\ldots,2l_n}\leq m^mn^m,\]
+since for any $l_1+\cdots+l_n=m$,
+\[\binom{2m}{2l_1,\ldots,2l_n}\leq m^m\binom{m}{l_1,\ldots,l_n}.\]
+This can be seen, for example, by writing both sides out using factorials, yielding
+
+\[\frac{(2m)!}{(2l_1)!\cdots (2l_n)!}\leq \frac{(2m)!}{2^mm!}\frac{m!}{l_1!\cdots l_n!}\leq m^m\frac{m!}{l_1!\cdots l_n!}.\]
+\end{proof}
+
+
+\begin{lemma}[Complex-valued Marcinkiewicz-Zygmund inequality]
+\label{mzi_complex}
+\leanok
+\lean{complex_marcinkiewicz_zygmund}
+Let $m\geq 1$. If $f:G\to\bbc$ is such that $\bbe_x f(x)=0$ and $\abs{f(x)}\leq 2$ for all $x$ then
+\[\bbe_{x_1,\ldots,x_n} \abs{\sum_{i=1}^n f(x_i)}^{2m} \leq (16mn)^{m}.\]
+\end{lemma}
+
+\begin{proof}
+\uses{mzi}
+\leanok
+Test.
+\end{proof}
+
+
+\begin{lemma}
+\label{random_approx_expect}
+\lean{lemma28}
+\leanok
+Let $\epsilon>0$ and $m\geq 1$. Let $A\subseteq G$ and $f:G\to \bbc$. If $k\geq 64m\epsilon^{-2}$ then the set
+\[L=\{ \tup{a}\in A^k : \|\tfrac{1}{k}\sum_{i=1}^kf(x-a_i)-\mu_A\ast f\|_{2m}\leq \epsilon \| f\|_{2m}\}.\]
+has size at least $\lvert A \rvert^k/2$.
+\end{lemma}
+
+\begin{proof}
+\uses{mzi_complex}
+\leanok
+Note that if $a\in A$ is chosen uniformly at random then, for any fixed $x\in G$,
+\[\bbe f(x-a_i)= \frac{1}{\abs{A}}\sum_{a\in A}f(x-a)=\frac{1}{\abs{A}}\ind{A}\ast f(x)=\mu_A\ast f(x).\]
+Therefore, if we choose $a_1,\ldots,a_k\in A$ independently uniformly at random, for any fixed $x\in G$ and $1\leq i\leq k$,  the random variable $f(x-a_i)-f\ast \mu_A(x)$ has mean zero. By the Marcinkiewicz-Zygmund inequality Lemma~\ref{mzi}, therefore,
+\begin{multline*}
+\bbe\abs{ \frac{1}{k}\sum_i f(x-a_i)-f\ast \mu_A(x)}^{2m} \leq \\(16m/k)^mk^{-1} \bbe \sum_i \abs{f(x-a_i)-f\ast \mu_A(x)}^{2m}.
+\end{multline*}
+We now sum both sides over all $x\in G$. By the triangle inequality, for any fixed $1\leq i\leq k$ and $a_i\in A$,
+\begin{align*}
+\sum_{x\in G} \abs{f(x-a_i)-f\ast \mu_A(x)}^{2m}
+&\leq 2^{2m-1}\sum_{x\in G}\abs{f(x-a_i)}^{2m}+\sum_{x\in G}\abs{f\ast \mu_A(x)}^{2m}\\
+&\leq 2^{2m-1}\brac{\norm{f}_{2m}^{2m}+\norm{f\ast \mu_A}_{2m}^{2m}}.
+\end{align*}
+We note that $\norm{\mu_A}_1=\frac{1}{\abs{A}}\sum_{x\in A}\ind{A}(x)=\abs{A}/\abs{A}=1$, and hence by Young's inequality, $\norm{f\ast \mu_A}_{2m}\leq \norm{f}_{2m}$, and so
+\[\sum_{x\in G} \abs{f(x-a_i)-f\ast \mu_A(x)}^{2m}\leq 2^{2m}\norm{f}_{2m}^{2m}.\]
+It follows that
+\[\bbe_{a_1,\ldots,a_k\in A}\norm{\frac{1}{k}\sum_i\tau_{a_i}f-f\ast \mu_A}_{2m}^{2m}\leq
+(64m/k)^m\norm{f}_{2m}^{2m}.\]
+In particular, if $k\geq 64\epsilon^{-2}m$ then the right-hand side is at most $(\frac{\epsilon}{2}\norm{f}_{2m})^{2m}$ as required.
+\end{proof}
+
+
+\begin{lemma}
+\label{aps_in_translates}
+\lean{just_the_triangle_inequality}
+\leanok
+Let $A\subseteq G$ and $f:G\to \bbc$. Let $\epsilon>0$ and $m\geq 1$ and $k\geq 1$. Let
+\[L=\{ \tup{a}\in A^k : \|\tfrac{1}{k}\sum_{i=1}^kf(x-a_i)-\mu_A\ast f\|_{2m}\leq \epsilon \| f\|_{2m}\}.\]
+If $t\in G$ is such that $\tup{a}\in L$ and $\tup{a}+(t,\ldots,t)\in L$ then
+\[\| \tau_t(\mu_A\ast f)-\mu_A\ast f\|_{2m}\leq 2\epsilon \|f\|_{2m}.\]
+\end{lemma}
+
+\begin{proof}
+\leanok
+Test.
+\end{proof}
+
+
+\begin{lemma}
+\label{lots_of_diagonals}
+\lean{big_shifts}
+\leanok
+Let $A\subseteq G$ and $k\geq 1$ and $L\subseteq A^k$. Then there exists some $\tup{a}\in L$ such that
+\[\#\{ t\in G : \tup{a}+(t,\ldots,t)\in L\}\geq \frac{\lvert L\rvert}{\lvert A+S\rvert^k}\lvert S\rvert.\]
+\end{lemma}
+
+\begin{proof}
+\leanok
+Test.
+\end{proof}
+
+
+\begin{theorem}[$L_p$ almost periodicity]
+\label{lp_ap}
+\lean{AlmostPeriodicity.almost_periodicity}
+\leanok
+Let $\epsilon\in (0,1]$ and $m\geq 1$. Let $K\geq 2$ and $A,S\subseteq G$ with $\lvert A+S\rvert\leq K\lvert A\rvert$.
+Let $f:G\to \bbc$. There exists $T\subseteq G$ such that
+\[\lvert T\rvert \geq K^{-512m\epsilon^{-2}}\lvert S\rvert\]
+such that for any $t\in T$ we have
+\[\| \tau_t(\mu_A\ast f)-\mu_A\ast f\|_{2m}\leq \epsilon \| f\|_{2m}.\]
+\end{theorem}
+
+\begin{proof}
+\uses{random_approx_expect, lots_of_diagonals, aps_in_translates}
+\leanok
+Test.
+\end{proof}
+
+
+\begin{theorem}[$L_\infty$ almost periodicity]
+\label{linfty_ap}
+\lean{AlmostPeriodicity.linfty_almost_periodicity}
+\leanok
+Let $\epsilon\in (0,1]$. Let $K\geq 2$ and $A,S\subseteq G$ with $\lvert A+S\rvert\leq K\lvert A\rvert$.
+Let $B,C\subseteq G$. Let $\eta=\min(1,\lvert C\rvert/\lvert B\rvert)$. There exists $T\subseteq G$ such that
+\[\lvert T\rvert \geq K^{-4096\lceil \lo{\eta}\rceil\epsilon^{-2}}\lvert S\rvert\]
+such that for any $t\in T$ we have
+\[\| \tau_t(\mu_A\ast 1_B\ast \mu_C)-\mu_A\ast 1_B\ast \mu_C\|_{\infty}\leq \epsilon.\]
+\end{theorem}
+
+\begin{proof}
+\leanok
+\uses{lp_ap} Let $T$ be as given in \ref{lp_ap}
+with $f=1_B$ and $m=\lceil \lo{\eta}\rceil$ and $\epsilon=\epsilon/e$. (The size bound on $T$ follows since $e^2\leq 8$.) Fix $t\in T$ and let $F=\tau_t(\mu_A\ast 1_B)-\mu_A\ast 1_B$. We have, for any $x\in G$,
+\[(\tau_t(\mu_A\ast 1_B\ast \mu_C)-\mu_A\ast 1_B\ast \mu_C)(x)=F\ast \mu_C(x)=\sum_y F(y)\mu_{C}(x-y)=\sum_yF(y)\mu_{x-C}(y).\]
+By Hölder's inequality, this is (in absolute value), for any $m\geq 1$,
+\[\norm{F}_{2m}\norm{\mu_{x-C}}_{1+\frac{1}{2m-1}}.\]
+By the construction of $T$ the first factor is at most
+$\frac{\epsilon}{e}\| 1_B\|_{2m}=\frac{\epsilon}{e}\lvert B\rvert^{1/2m}$.
+We have by calculation
+\[\norm{\mu_{x-C}}_{1+\frac{1}{2m-1}}=\lvert x-C\rvert^{-1/2m}=\lvert C\rvert^{-1/2m}.\]
+Therefore we have shown that
+
+\[\| \tau_t(\mu_A\ast 1_B\ast \mu_C)-\mu_A\ast 1_B\ast \mu_C\|_{\infty}\leq \frac{\epsilon}{e}(\lvert C\rvert/\lvert B\rvert)^{-1/2m}.\]
+The claim now follows since, by choice of $m$,
+\[(\lvert C\rvert/\lvert B\rvert)^{-1/2m}\leq e\]
+(dividing into cases as to whether $\eta=1$ or not).
+\end{proof}
+
+
+\begin{theorem}
+\label{linfty_ap_boosted}
+\lean{AlmostPeriodicity.linfty_almost_periodicity_boosted}
+\leanok
+Let $\epsilon\in (0,1]$ and $k\geq 1$. Let $K\geq 2$ and $A,S\subseteq G$ with $\lvert A+S\rvert\leq K\lvert A\rvert$.
+Let $B,C\subseteq G$. Let $\eta=\min(1,\lvert C\rvert/\lvert B\rvert)$. There exists $T\subseteq G$ such that
+\[\lvert T\rvert \geq K^{-4096\lceil \lo{\eta}\rceil k^2\epsilon^{-2}}\lvert S\rvert\]
+such that
+\[\| \mu_T^{(k)}\ast \mu_A\ast 1_B\ast \mu_C-\mu_A\ast 1_B\ast \mu_C\|_{\infty}\leq \epsilon.\]
+\end{theorem}
+
+\begin{proof}
+\uses{linfty_ap}
+\leanok
+Let $T$ be as in Theorem~\ref{linfty_ap} with $\epsilon$ replaced by $\epsilon/k$. Note that, for any $x\in G$,
+\[\mu_T^{(k)}\ast \mu_A\ast 1_B\ast \mu_C(x)=\frac{1}{\lvert T\rvert^k}\sum_{t_1,\ldots,t_k\in T}\tau_{t_1+\cdots+t_k}\mu_A\ast 1_B\ast \mu_C(x).\]
+It therefore suffices (by the triangle inequality) to show, for any fixed $x\in G$ and $t_1,\ldots,t_k\in T$, that with $F=\mu_A\ast 1_B\ast \mu_C$, we have
+\[\lvert \tau_{t_1+\cdots+t_k}F(x)-F(x)\rvert \leq \epsilon.\]
+This follows by the triangle inequality applied $k$ times if we knew that, for $1\leq l\leq k$,
+\[\lvert \tau_{t_1+\cdots+t_l}F(x)-\tau_{t_1+\cdots+t_{l-1}}F(x)\rvert \leq \epsilon/k.\]
+We can write the left-hand side as
+\[\lvert \tau_{t_1+\cdots+t_l}F(x)-\tau_{t_1+\cdots+t_{l-1}}F(x)\rvert=\lvert \tau_{t_l}F(x-t_1-\cdots-t-{l-1})-F(x-t_1-\cdots-t-{l-1})\rvert.\]
+The right-hand side is at most
+\[\| \tau_{t_l}F-F\|_\infty\]
+and we are done by choice of $T$.
+\end{proof}