Skip to content

Commit 7161a98

Browse files
committed
Setup blueprint
1 parent ef7c7be commit 7161a98

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

41 files changed

+2042
-2
lines changed

.github/workflows/blueprint.yml

+105
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,105 @@
1+
on:
2+
push:
3+
branches:
4+
- master
5+
6+
# Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages
7+
permissions:
8+
contents: read
9+
pages: write
10+
id-token: write
11+
12+
jobs:
13+
build_project:
14+
runs-on: ubuntu-latest
15+
name: Build project
16+
steps:
17+
- name: Checkout project
18+
uses: actions/checkout@v2
19+
with:
20+
fetch-depth: 0
21+
22+
- name: Install elan
23+
run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover/lean4:4.5.0
24+
25+
- name: Update docgen4
26+
run: ~/.elan/bin/lake -R -Kenv=dev update «doc-gen4»
27+
28+
- name: Update checkdecls
29+
run: ~/.elan/bin/lake update checkdecls
30+
31+
- name: Get cache
32+
run: ~/.elan/bin/lake -R -Kenv=dev exe cache get || true
33+
34+
- name: Build project
35+
run: ~/.elan/bin/lake -R -Kenv=dev build FLT3
36+
37+
- name: Cache mathlib docs
38+
uses: actions/cache@v3
39+
with:
40+
path: |
41+
.lake/build/doc/Init
42+
.lake/build/doc/Lake
43+
.lake/build/doc/Lean
44+
.lake/build/doc/Std
45+
.lake/build/doc/Mathlib
46+
.lake/build/doc/declarations
47+
!.lake/build/doc/declarations/declaration-data-FLT3*
48+
key: MathlibDoc-${{ hashFiles('lake-manifest.json') }}
49+
restore-keys: |
50+
MathlibDoc-
51+
52+
- name: Build documentation
53+
run: ~/.elan/bin/lake -R -Kenv=dev build FLT3:docs
54+
55+
- name: Build blueprint and copy to `docs/blueprint`
56+
uses: xu-cheng/texlive-action@v2
57+
with:
58+
docker_image: ghcr.io/xu-cheng/texlive-full:20231201
59+
run: | # "mkdir docs" before "cp blueprint/print/print.pdf docs/blueprint.pdf"
60+
apk update
61+
apk add --update make py3-pip git pkgconfig graphviz graphviz-dev gcc musl-dev
62+
git config --global --add safe.directory $GITHUB_WORKSPACE
63+
git config --global --add safe.directory `pwd`
64+
python3 -m venv env
65+
source env/bin/activate
66+
pip install --upgrade pip requests wheel
67+
pip install pygraphviz --global-option=build_ext --global-option="-L/usr/lib/graphviz/" --global-option="-R/usr/lib/graphviz/"
68+
pip install leanblueprint
69+
leanblueprint pdf
70+
cp blueprint/print/print.pdf docs/blueprint.pdf
71+
leanblueprint web
72+
cp -r blueprint/web docs/blueprint
73+
74+
- name: Check declarations
75+
run: |
76+
~/.elan/bin/lake exe checkdecls blueprint/lean_decls
77+
78+
- name: Move documentation to `docs/docs`
79+
run: |
80+
sudo chown -R runner docs
81+
cp -r .lake/build/doc docs/docs
82+
83+
- name: Bundle dependencies
84+
uses: ruby/setup-ruby@v1
85+
with:
86+
working-directory: docs
87+
ruby-version: "3.0" # Not needed with a .ruby-version file
88+
bundler-cache: true # runs 'bundle install' and caches installed gems automatically
89+
90+
- name: Bundle website
91+
working-directory: docs
92+
run: JEKYLL_ENV=production bundle exec jekyll build
93+
94+
- name: Upload docs & blueprint artifact
95+
uses: actions/upload-pages-artifact@v1
96+
with:
97+
path: docs/_site
98+
99+
- name: Deploy to GitHub Pages
100+
id: deployment
101+
uses: actions/deploy-pages@v1
102+
103+
- name: Make sure the cache works
104+
run: |
105+
mv docs/docs .lake/build/doc

.gitignore

+3
Original file line numberDiff line numberDiff line change
@@ -9,3 +9,6 @@
99
/lakefile.olean
1010
# After v4.3.0-rc2 lake stores its files here:
1111
/.lake/
12+
# Python virtual environment
13+
/.venv/
14+
references.md

README.md

+2-2
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,3 @@
1-
Proof in Lean of Fermat Last Theorem for exponent 3
2-
1+
Formalisation of Fermat's Last Theorem (FLT) for Exponent 3 in Lean
2+
33
<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

+16
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
*.pdf
2+
*.paux
3+
*.aux
4+
*.log
5+
print
6+
web
7+
__pycache__
8+
*.fdb_latexmk
9+
*.fls
10+
*.out
11+
*.synctex.gz
12+
*.xdv
13+
*.maf
14+
*.mtc
15+
*.mtc0
16+
build

blueprint/requirements.txt

+8
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
# https://github.com/pyinvoke/invoke/issues/891
2+
invoke==2.2.0
3+
plasTeX @ git+https://github.com/plastex/plastex.git
4+
plastexdepgraph @ git+https://github.com/PatrickMassot/plastexdepgraph.git
5+
plastexshowmore @ git+https://github.com/PatrickMassot/plastexshowmore.git
6+
leanblueprint @ git+https://github.com/PatrickMassot/leanblueprint.git
7+
watchfiles==0.16.1
8+
pandoc==2.3

blueprint/src/chapter/ap.tex

+185
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,185 @@
1+
\chapter{Almost-Periodicity}
2+
\label{chap:ap}
3+
4+
5+
\begin{lemma}[Marcinkiewicz-Zygmund inequality]
6+
\label{mzi}
7+
\lean{other_marcinkiewicz_zygmund'}
8+
\leanok
9+
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
10+
\[\bbe_{x_1,\ldots,x_n} \abs{\sum_{i=1}^n f(x_i)}^{2m} \leq (4mn)^{m}.\]
11+
\end{lemma}
12+
13+
\begin{proof}
14+
\leanok
15+
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,
16+
\[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}.\]
17+
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\}$,
18+
\[ S \leq\bbe_{x_1,\ldots,y_n}\left\lvert \sum_i \epsilon_i(f(x_i)-f(y_i))\right\rvert^{2m}.\]
19+
In particular, if we sample $\epsilon_i\in\{-1,+1\}$ uniformly at random, then
20+
\[ 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}.\]
21+
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
22+
\[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}}.\]
23+
The inner expectation vanishes unless each $k_i$ is even, when it is trivially one. Therefore the above quantity is exactly
24+
\[\sum_{l_1+\cdots+l_n=m}\binom{2m}{2l_1,\ldots,2l_n}\leq m^mn^m,\]
25+
since for any $l_1+\cdots+l_n=m$,
26+
\[\binom{2m}{2l_1,\ldots,2l_n}\leq m^m\binom{m}{l_1,\ldots,l_n}.\]
27+
This can be seen, for example, by writing both sides out using factorials, yielding
28+
29+
\[\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!}.\]
30+
\end{proof}
31+
32+
33+
\begin{lemma}[Complex-valued Marcinkiewicz-Zygmund inequality]
34+
\label{mzi_complex}
35+
\leanok
36+
\lean{complex_marcinkiewicz_zygmund}
37+
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
38+
\[\bbe_{x_1,\ldots,x_n} \abs{\sum_{i=1}^n f(x_i)}^{2m} \leq (16mn)^{m}.\]
39+
\end{lemma}
40+
41+
\begin{proof}
42+
\uses{mzi}
43+
\leanok
44+
Test.
45+
\end{proof}
46+
47+
48+
\begin{lemma}
49+
\label{random_approx_expect}
50+
\lean{lemma28}
51+
\leanok
52+
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
53+
\[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}\}.\]
54+
has size at least $\lvert A \rvert^k/2$.
55+
\end{lemma}
56+
57+
\begin{proof}
58+
\uses{mzi_complex}
59+
\leanok
60+
Note that if $a\in A$ is chosen uniformly at random then, for any fixed $x\in G$,
61+
\[\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).\]
62+
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,
63+
\begin{multline*}
64+
\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}.
65+
\end{multline*}
66+
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$,
67+
\begin{align*}
68+
\sum_{x\in G} \abs{f(x-a_i)-f\ast \mu_A(x)}^{2m}
69+
&\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}\\
70+
&\leq 2^{2m-1}\brac{\norm{f}_{2m}^{2m}+\norm{f\ast \mu_A}_{2m}^{2m}}.
71+
\end{align*}
72+
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
73+
\[\sum_{x\in G} \abs{f(x-a_i)-f\ast \mu_A(x)}^{2m}\leq 2^{2m}\norm{f}_{2m}^{2m}.\]
74+
It follows that
75+
\[\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
76+
(64m/k)^m\norm{f}_{2m}^{2m}.\]
77+
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.
78+
\end{proof}
79+
80+
81+
\begin{lemma}
82+
\label{aps_in_translates}
83+
\lean{just_the_triangle_inequality}
84+
\leanok
85+
Let $A\subseteq G$ and $f:G\to \bbc$. Let $\epsilon>0$ and $m\geq 1$ and $k\geq 1$. Let
86+
\[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}\}.\]
87+
If $t\in G$ is such that $\tup{a}\in L$ and $\tup{a}+(t,\ldots,t)\in L$ then
88+
\[\| \tau_t(\mu_A\ast f)-\mu_A\ast f\|_{2m}\leq 2\epsilon \|f\|_{2m}.\]
89+
\end{lemma}
90+
91+
\begin{proof}
92+
\leanok
93+
Test.
94+
\end{proof}
95+
96+
97+
\begin{lemma}
98+
\label{lots_of_diagonals}
99+
\lean{big_shifts}
100+
\leanok
101+
Let $A\subseteq G$ and $k\geq 1$ and $L\subseteq A^k$. Then there exists some $\tup{a}\in L$ such that
102+
\[\#\{ t\in G : \tup{a}+(t,\ldots,t)\in L\}\geq \frac{\lvert L\rvert}{\lvert A+S\rvert^k}\lvert S\rvert.\]
103+
\end{lemma}
104+
105+
\begin{proof}
106+
\leanok
107+
Test.
108+
\end{proof}
109+
110+
111+
\begin{theorem}[$L_p$ almost periodicity]
112+
\label{lp_ap}
113+
\lean{AlmostPeriodicity.almost_periodicity}
114+
\leanok
115+
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$.
116+
Let $f:G\to \bbc$. There exists $T\subseteq G$ such that
117+
\[\lvert T\rvert \geq K^{-512m\epsilon^{-2}}\lvert S\rvert\]
118+
such that for any $t\in T$ we have
119+
\[\| \tau_t(\mu_A\ast f)-\mu_A\ast f\|_{2m}\leq \epsilon \| f\|_{2m}.\]
120+
\end{theorem}
121+
122+
\begin{proof}
123+
\uses{random_approx_expect, lots_of_diagonals, aps_in_translates}
124+
\leanok
125+
Test.
126+
\end{proof}
127+
128+
129+
\begin{theorem}[$L_\infty$ almost periodicity]
130+
\label{linfty_ap}
131+
\lean{AlmostPeriodicity.linfty_almost_periodicity}
132+
\leanok
133+
Let $\epsilon\in (0,1]$. Let $K\geq 2$ and $A,S\subseteq G$ with $\lvert A+S\rvert\leq K\lvert A\rvert$.
134+
Let $B,C\subseteq G$. Let $\eta=\min(1,\lvert C\rvert/\lvert B\rvert)$. There exists $T\subseteq G$ such that
135+
\[\lvert T\rvert \geq K^{-4096\lceil \lo{\eta}\rceil\epsilon^{-2}}\lvert S\rvert\]
136+
such that for any $t\in T$ we have
137+
\[\| \tau_t(\mu_A\ast 1_B\ast \mu_C)-\mu_A\ast 1_B\ast \mu_C\|_{\infty}\leq \epsilon.\]
138+
\end{theorem}
139+
140+
\begin{proof}
141+
\leanok
142+
\uses{lp_ap} Let $T$ be as given in \ref{lp_ap}
143+
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$,
144+
\[(\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).\]
145+
By Hölder's inequality, this is (in absolute value), for any $m\geq 1$,
146+
\[\norm{F}_{2m}\norm{\mu_{x-C}}_{1+\frac{1}{2m-1}}.\]
147+
By the construction of $T$ the first factor is at most
148+
$\frac{\epsilon}{e}\| 1_B\|_{2m}=\frac{\epsilon}{e}\lvert B\rvert^{1/2m}$.
149+
We have by calculation
150+
\[\norm{\mu_{x-C}}_{1+\frac{1}{2m-1}}=\lvert x-C\rvert^{-1/2m}=\lvert C\rvert^{-1/2m}.\]
151+
Therefore we have shown that
152+
153+
\[\| \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}.\]
154+
The claim now follows since, by choice of $m$,
155+
\[(\lvert C\rvert/\lvert B\rvert)^{-1/2m}\leq e\]
156+
(dividing into cases as to whether $\eta=1$ or not).
157+
\end{proof}
158+
159+
160+
\begin{theorem}
161+
\label{linfty_ap_boosted}
162+
\lean{AlmostPeriodicity.linfty_almost_periodicity_boosted}
163+
\leanok
164+
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$.
165+
Let $B,C\subseteq G$. Let $\eta=\min(1,\lvert C\rvert/\lvert B\rvert)$. There exists $T\subseteq G$ such that
166+
\[\lvert T\rvert \geq K^{-4096\lceil \lo{\eta}\rceil k^2\epsilon^{-2}}\lvert S\rvert\]
167+
such that
168+
\[\| \mu_T^{(k)}\ast \mu_A\ast 1_B\ast \mu_C-\mu_A\ast 1_B\ast \mu_C\|_{\infty}\leq \epsilon.\]
169+
\end{theorem}
170+
171+
\begin{proof}
172+
\uses{linfty_ap}
173+
\leanok
174+
Let $T$ be as in Theorem~\ref{linfty_ap} with $\epsilon$ replaced by $\epsilon/k$. Note that, for any $x\in G$,
175+
\[\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).\]
176+
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
177+
\[\lvert \tau_{t_1+\cdots+t_k}F(x)-F(x)\rvert \leq \epsilon.\]
178+
This follows by the triangle inequality applied $k$ times if we knew that, for $1\leq l\leq k$,
179+
\[\lvert \tau_{t_1+\cdots+t_l}F(x)-\tau_{t_1+\cdots+t_{l-1}}F(x)\rvert \leq \epsilon/k.\]
180+
We can write the left-hand side as
181+
\[\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.\]
182+
The right-hand side is at most
183+
\[\| \tau_{t_l}F-F\|_\infty\]
184+
and we are done by choice of $T$.
185+
\end{proof}

0 commit comments

Comments
 (0)