Merge branch 'master' of https://github.com/teorth/pfr

.github/workflows/push.yml

@@ -27,26 +27,7 @@ jobs:
   build_project:
     runs-on: ubuntu-latest
     name: Build project
-    concurrency:
-      group: ${{ github.workflow }}-${{ github.ref }}
-      cancel-in-progress: true
     steps:
-      - name: Free disk space
-        uses: jlumbroso/free-disk-space@main
-        with:
-          # this might remove tools that are actually needed,
-          # if set to "true" but frees about 6 GB
-          tool-cache: false
-
-          # all of these default to true, but feel free to set to
-          # "false" if necessary for your workflow
-          android: true
-          dotnet: true
-          haskell: true
-          large-packages: true
-          docker-images: true
-          swap-storage: true
-
       - name: Checkout project
         uses: actions/checkout@v2
         with:

.github/workflows/push_pr.yml

@@ -5,9 +5,6 @@ jobs:
   build_project:
     runs-on: ubuntu-latest
     name: Build project
-    concurrency:
-      group: ${{ github.workflow }}-${{ github.ref }}
-      cancel-in-progress: true
     steps:
       - name: Checkout project
         uses: actions/checkout@v2

blueprint/src/chapter/distance.tex

@@ -2,7 +2,7 @@ \chapter{Ruzsa calculus}
 
 In this section $G$ will be a finite additive group.  (May eventually want to generalize to infinite $G$.)
 
-\begin{lemma}[Negation preserves entropy]\label{neg-ent}\uses{entropy-def}  If $X$ is $G$-valued, then $\H[-X]=\H[X]$.
+\begin{lemma}[Negation preserves entropy]\label{neg-ent}\uses{entropy-def}  If $X$ is $G$-valued, then $\bbH[-X]=\bbH[X]$.
 \end{lemma}
 
 \begin{proof}\uses{relabeled-entropy} Immediate from Lemma \ref{relabeled-entropy}.
@@ -22,7 +22,7 @@ \chapter{Ruzsa calculus}
 
 \begin{corollary}[Conditional lower bound on sumset]\label{sumset-lower-gen-cond}\uses{conditional-mutual-def, conditional-entropy-def} If $X,Y$ are $G$-valued random variables on $\Omega$ and $Z$ is another random variable on $\Omega$ then
 \[
-  \max(H[X|Z], H[Y|Z]) - I[X:Y|Z] \leq \H[X\pm Y|Z],
+  \max(H[X|Z], H[Y|Z]) - I[X:Y|Z] \leq \bbH[X\pm Y|Z],
 \]
 \end{corollary}
 
@@ -67,7 +67,7 @@ \chapter{Ruzsa calculus}
 \begin{proof} \uses{copy-ent} Immediate from Definitions \ref{ruz-dist-def} and Lemma \ref{copy-ent}.
 \end{proof}
 
-\begin{lemma}[Ruzsa distance in inependent case]\label{ruz-indep}\uses{ruz-dist-def, entropy-def, independent-def} If $X,Y$ are independent $G$-random variables then
+\begin{lemma}[Ruzsa distance in independent case]\label{ruz-indep}\uses{ruz-dist-def, entropy-def, independent-def} If $X,Y$ are independent $G$-random variables then
   $$ d[X;Y] := H[X - Y] - H[X]/2 - H[Y]/2.$$
 \end{lemma}
 
@@ -89,7 +89,7 @@ \chapter{Ruzsa calculus}
 \end{proof}
 
 \begin{lemma}[Distance controls entropy growth]\label{ruzsa-growth}\uses{ruz-dist-def, entropy-def} If $X,Y$ are $G$-valued random variables, then
-$$  \H[X-Y] - \H[X], \H[X-Y] - \H[Y] \leq 2d[X;Y].$$
+$$  \bbH[X-Y] - \bbH[X], \bbH[X-Y] - \bbH[Y] \leq 2d[X;Y].$$
 \end{lemma}
 
 \begin{proof} \uses{sumset-lower, neg-ent} Immediate from Lemma \ref{sumset-lower} and Definition \ref{ruz-dist-def}, and also Lemma \ref{neg-ent}.
@@ -160,13 +160,13 @@ \chapter{Ruzsa calculus}
   \begin{equation}
   \begin{split} H[X_1, X_2, Y'] &= H[X_1,X_2|Y] + H[Y] \\
     &= 2 H[X|Y] + H[Y] \\
-    &= 2 H[X] + H[Y] + 2 \I[X:Y].
+    &= 2 H[X] + H[Y] + 2 I[X:Y].
   \end{split}  \end{equation}
 \end{proof}
 
 
 \begin{lemma}[Balog-Szemer\'edi-Gowers]\label{lem-bsg}\uses{ruz-dist-def, information-def, entropy-def}
-  Let $A,B$ be $G$-valued random variables on $\Omega$, and set $Z \coloneqq A+B$.
+  Let $A,B$ be $G$-valued random variables on $\Omega$, and set $Z \coloneq A+B$.
 Then
 \begin{equation}\label{2-bsg-takeaway} \sum_{z} P[Z=z] d[(A | Z = z); (B | Z = z)] \leq 3 I[A:B] + 2 H[Z] - H[A] - H[B]. \end{equation}
 \end{lemma}
@@ -197,7 +197,7 @@ \chapter{Ruzsa calculus}
 \[ H[A_1 - B_2] \leq 2I[A:B] + H[Z]\] and so by~\eqref{cond-dec}
 \[H[A_1 - B_2 | Z]  \leq 2I[A:B] + H[Z].\]
 Since
-\begin{align*} H[A_1 | Z] & = H[A_1, A_1 + B_1] - H[Z] \\ & = H[A,B] - H[Z] \\ & = H[Z] - I[A:B] - 2 H[Z]-H[A]-\H[B]\end{align*}
-and similarly for $\H[B_2 | Z]$, we see that~\eqref{lhs-to-bound} is bounded by
+\begin{align*} H[A_1 | Z] & = H[A_1, A_1 + B_1] - H[Z] \\ & = H[A,B] - H[Z] \\ & = H[Z] - I[A:B] - 2 H[Z]-H[A]-\bbH[B]\end{align*}
+and similarly for $\bbH[B_2 | Z]$, we see that~\eqref{lhs-to-bound} is bounded by
 $3I[A:B] + 2H[Z]-H[A]-H[B]$ as claimed.
 \end{proof}

blueprint/src/chapter/entropy.tex

@@ -163,7 +163,7 @@ \chapter{Shannon entropy inequalities}
 \begin{proof} \uses{add-entropy} Immediate from Lemma \ref{add-entropy} and Definition \ref{information-def}.
 \end{proof}
 
-\begin{definition}[Conditional mutual information]\label{conditional-mutual-def}\uses{information-def,{condition-event-def}  If $X,Y,Z$ are random variables, with $Z$ $U$-valued, then
+\begin{definition}[Conditional mutual information]\label{conditional-mutual-def}\uses{information-def,condition-event-def}  If $X,Y,Z$ are random variables, with $Z$ $U$-valued, then
   $$ I[X:Y|Z] := \sum_{z \in U} P[Z=z] I[(X|Z=z): (Y|Z=z)].$$
 \end{definition}
 

blueprint/src/chapter/main.tex

@@ -0,0 +1,9 @@
+% This is the main point of entry to the blueprint.
+% Add chapters of the blueprint here.
+% This file is not meant to be built. Build src/web.tex or src/print.text instead.
+
+\input{chapter/jensen}
+\input{chapter/entropy}
+\input{chapter/distance}
+\input{chapter/pfr-entropy}
+\input{chapter/pfr}

blueprint/src/macro/common.tex → blueprint/src/preamble/common.tex

@@ -1,20 +1,32 @@
-% Put any macro needed for the project here. Those macros for both the web and print versions of the blueprint.
+% Put any macro and import needed for the project here.
+% This will be used by both the web and print versions of the blueprint.
+% This file is not meant to be built. Build src/web.tex or src/print.text instead.
 
-\newcommand{\ind}[1]{1_{#1}}
-\newcommand{\bbn}{\mathbb{N}}
-\newcommand{\bbz}{\mathbb{Z}}
-\newcommand{\bbr}{\mathbb{R}}
+% Letters
+\newcommand{\C}{\mathbb{C}}
+\newcommand{\bbc}{\mathbb{C}}
+\newcommand{\E}{\mathbb{E}}
+\newcommand*{\bbe}{\mathbb{E}}
+\newcommand{\F}{\mathbb{F}}
 \newcommand{\bbf}{\mathbb{F}}
+\newcommand{\bbH}{\mathbb{H}}
+\newcommand{\bbn}{\mathbb{N}}
 \newcommand{\bbq}{\mathbb{Q}}
-\newcommand{\bbc}{\mathbb{C}}
+\newcommand{\bbr}{\mathbb{R}}
 \newcommand{\bbt}{\mathbb{T}}
-\newcommand*{\bbe}{\mathbb{E}}
+\newcommand{\bbz}{\mathbb{Z}}
+
+\newcommand{\lo}[1]{\mathcal{L}{#1}}
+
+% Paired delimiters
 \newcommand{\abs}[1]{\left\lvert #1\right\rvert}
 \newcommand{\Abs}[1]{\lvert #1 \rvert}
 \newcommand{\brac}[1]{\left( #1\right)}
 \newcommand{\norm}[1]{\lVert #1\rVert}
-\providecommand{\tup}[1]{{\vec{#1}}}
-\newcommand{\lo}[1]{\mathcal{L}{#1}}
 \newcommand{\inn}[1]{\left\langle #1 \right\rangle}
-\newcommand{\C}{\mathbb{C}}
-\newcommand{\E}{\mathbb{E}}
+
+% Operators
+\DeclareMathOperator{\dist}{dist}
+
+\newcommand{\ind}[1]{1_{#1}}
+\providecommand{\tup}[1]{{\vec{#1}}}

blueprint/src/macro/print.tex → blueprint/src/preamble/print.tex

@@ -1,4 +1,5 @@
 % Those macros are used for the print version of the blueprint.
+% This file is not meant to be built. Build src/web.tex or src/print.text instead.
 
 \declaretheorem[numberwithin=chapter]{theorem}
 \declaretheorem[sibling=theorem]{proposition}

blueprint/src/macro/web.tex → blueprint/src/preamble/web.tex

@@ -1,4 +1,5 @@
 % Those macros are used for the web version of the blueprint.
+% This file is not meant to be built. Build src/web.tex or src/print.text instead.
 
 \newtheorem{theorem}{Theorem}[chapter]
 \newtheorem{definition}[theorem]{Definition}

blueprint/src/print.tex

@@ -13,6 +13,7 @@
 
 \usepackage{tikz-cd}
 
+\usepackage{mathtools}
 \usepackage[warnings-off={mathtools-colon,mathtools-overbracket}]{unicode-math}
 \usepackage{fontspec}
 \setmathfont{Latin Modern Math}
@@ -23,18 +24,17 @@
 
 \usepackage[nameinlink, capitalize]{cleveref}
 
-\input{macro/common}
-
 \usepackage{amsthm}
 \usepackage{etexcmds}
 \usepackage{thmtools}
 
-\input{macro/print}
+\input{preamble/common}
+\input{preamble/print}
 
 \title{PFR}
 \author{Terence Tao}
 
 \begin{document}
 \maketitle
-\input{content}
+\input{chapter/main}
 \end{document}

blueprint/src/web.tex

@@ -1,4 +1,5 @@
-% This file makes the web version of the blueprint
+% This file makes the web version of the blueprint.
+% This file can be built locally.
 
 \documentclass{report}
 
@@ -12,12 +13,12 @@
 \usepackage{tikz-cd}
 \usepackage{tikz}
 
-\input{macro/common}
-\input{macro/web}
+\input{preamble/common}
+\input{preamble/web}
 
-%\home{https://github.com/teorth/PFR/}
-\github{https://github.com/teorth/PFR/}
-\dochome{https://teorth.github.io/PFR/docs}
+%\home{https://github.com/teorth/pfr/}
+\github{https://github.com/teorth/pfr/}
+\dochome{https://teorth.github.io/pfr/docs}
 
 \title{PFR}
 \author{}

docs/_config.yml

@@ -22,7 +22,7 @@ title: The Polynomial Freiman-Ruzsa Conjecture
 #email: [email protected]
 description: A digitisation of the proof of the Polynomial Freiman-Ruzsa Conjecture in Lean 4
 baseurl: "" # the subpath of your site, e.g. /blog
-url: "https://teorth.github.io/PFR/" # the base hostname & protocol for your site, e.g. http://example.com
+url: "https://teorth.github.io/pfr/" # the base hostname & protocol for your site, e.g. http://example.com
 #twitter_username: jekyllrb
 github_username: teorth
 repository: teorth/pfr
@@ -31,6 +31,8 @@ repository: teorth/pfr
 remote_theme: pages-themes/[email protected]
 plugins:
   - jekyll-remote-theme
+
+markdown: kramdown
 # Exclude from processing.
 # The following items will not be processed, by default.
 # Any item listed under the `exclude:` key here will be automatically added to

docs/_includes/mathjax.html

@@ -0,0 +1,10 @@
+<!-- for mathjax support -->
+{% if page.usemathjax %}
+<script type="text/x-mathjax-config">
+  MathJax.Hub.Config({
+  TeX: { equationNumbers: { autoNumber: "AMS" } }
+  });
+</script>
+<script type="text/javascript" async
+  src="http://cdn.mathjax.org/mathjax/latest/MathJax.js?config=TeX-AMS-MML_HTMLorMML"></script>
+{% endif %}

docs/_layouts/default.html

@@ -13,7 +13,7 @@
   <meta name="apple-mobile-web-app-status-bar-style" content="black-translucent">
   {% if jekyll.environment == "production" %}
   <link rel="stylesheet"
-    href="{{ 'PFR/assets/css/style.css?v=' | append: site.github.build_revision | relative_url }}">
+    href="{{ 'pfr/assets/css/style.css?v=' | append: site.github.build_revision | relative_url }}">
   {% else %}
   <link rel="stylesheet" href="{{ 'assets/css/style.css?v=' | append: site.github.build_revision | relative_url }}">
   {% endif %}

docs/index.md

@@ -3,18 +3,21 @@
 # To modify the layout, see https://jekyllrb.com/docs/themes/#overriding-theme-defaults
 
 # layout: home
+usemathjax: true
 ---
 
+{% include mathjax.html %}
+
 # The Polynomial Freiman-Ruzsa Conjecture
 
-The purpose of this repository is to hold a Lean4 formalization of the proof of the Polynomial Freiman-Ruzsa (PFR) conjecture, recently proven in https://arxiv.org/abs/2311.05762 .  The statement is as follows: if $A$ is a non-empty subset of ${\bf F}_2^n$ such that $|A+A| \leq K|A|$, then $A$ can be covered by at most $2K^{12}$ cosets of a subspace $H$ of ${\bf F}_2^n$ of cardinality at most $|A|$.  The proof relies on the theory of Shannon entropy, so in particular development of the Shannon entropy inequalities will be needed.
+The purpose of this repository is to hold a Lean4 formalization of the proof of the Polynomial Freiman-Ruzsa (PFR) conjecture, recently proven in <https://arxiv.org/abs/2311.05762>.  The statement is as follows: if $$A$$ is a non-empty subset of $${\bf F}_2^n$$ such that $$\vert A+A\vert \leq K\vert A\vert$$, then $$A$$ can be covered by at most $$2K^{12}$$ cosets of a subspace $$H$$ of $${\bf F}_2^n$$ of cardinality at most $$\vert A\vert$$.  The proof relies on the theory of Shannon entropy, so in particular development of the Shannon entropy inequalities will be needed.
 
-Discussion of the project will be held on this Zulip stream: https://leanprover.zulipchat.com/#narrow/stream/412902-Polynomial-Freiman-Ruzsa-conjecture
+Discussion of the project will be held on this Zulip stream: <https://leanprover.zulipchat.com/#narrow/stream/412902-Polynomial-Freiman-Ruzsa-conjecture>
 
-Additional discussion of the project may be found at https://terrytao.wordpress.com/2023/11/13/on-a-conjecture-of-marton/
+Additional discussion of the project may be found at <https://terrytao.wordpress.com/2023/11/13/on-a-conjecture-of-marton/>
 
 ## Source reference
 
-`[GGMT]`: https://arxiv.org/abs/2311.05762
+`[GGMT]`: <https://arxiv.org/abs/2311.05762>
 
 [GGMT]: https://arxiv.org/abs/2311.05762