add package, some updates to webpage

blueprint/src/chapter/main.tex

@@ -1,6 +1,8 @@
 % 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.
+
+% Note: still have to upstream \section ~> \chapter and \subsection ~> \section to Overleaf
 \title{Carleson operators on doubling metric measure spaces}
 
 \author{Lars Becker \and Floris van Doorn \and Asgar Jamneshan \and Rajula Srivastava \and Christoph Thiele}

blueprint/src/preamble/common.tex

@@ -12,6 +12,7 @@
 \usepackage{enumerate}
 \usepackage[hidelinks, colorlinks=false]{hyperref}
 % \usepackage{showlabels} % not compatible with Plastex
+\usepackage[normalem]{ulem}
 
 \newcommand{\rs}[1]{{\color{blue}  RS: #1.}}
 \newcommand{\lars}[1]{{\color{red}  LB: #1.}}

docs/_config.yml

@@ -18,9 +18,9 @@
 # You can create any custom variable you would like, and they will be accessible
 # in the templates via {{ site.myvariable }}.
 
-title: The Polynomial Freiman-Ruzsa Conjecture
+title: Carleson operators on doubling metric measure spaces
 #email: [email protected]
-description: A digitisation of the proof of the Polynomial Freiman-Ruzsa Conjecture in Lean 4
+description: A formalization in Lean 4
 baseurl: "" # the subpath of your site, e.g. /blog
 url: "https://fpvandoorn.github.io/carleson/" # the base hostname & protocol for your site, e.g. http://example.com
 #twitter_username: jekyllrb

docs/index.md

@@ -12,12 +12,9 @@ usemathjax: true
 
 WIP formalization of a generalized Carleson's theorem
 
-<!-- The purpose of this repository is to hold a Lean4 formalization of [the proof of the Polynomial Freiman-Ruzsa (PFR) conjecture](https://arxiv.org/abs/2311.05762) (see also [this blog post](https://terrytao.wordpress.com/2023/11/13/on-a-conjecture-of-marton).  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 on Zulip](https://leanprover.zulipchat.com/#narrow/stream/412902-Polynomial-Freiman-Ruzsa-conjecture)
-* [Blueprint of the proof](https://teorth.github.io/pfr/blueprint)
-* [Documentation of the methods](https://teorth.github.io/pfr/docs)
-* [A quick "tour" of the project](https://terrytao.wordpress.com/2023/11/18/formalizing-the-proof-of-pfr-in-lean4-using-blueprint-a-short-tour) -->
+* [Blueprint of the proof](https://florisvandoorn.com/carleson/blueprint/)
+* [Blueprint (pdf)](https://florisvandoorn.com/carleson/blueprint.pdf)
+* [Documentation of the methods](https://florisvandoorn.com/carleson/docs/)
 
 ## Build the Lean files
 
@@ -28,28 +25,20 @@ To build the project, run `lake exe cache get` and then `lake build`.
 
 ## Build the blueprint
 
-To build the web version of the blueprint, you need a working LaTeX installation.
+The blueprint is automatically built on each push to the project.
+You can test whether the build is working by building the pdf locally:
+`xelatex blueprint/src/print.tex`.
+
+<!-- To build the web version of the blueprint locally, you need a working LaTeX installation.
 Furthermore, you need some packages:
 ```
 sudo apt install graphviz libgraphviz-dev
-pip3 install invoke pandoc
-cd .. # go to folder where you are happy clone git repos
-git clone [email protected]:plastex/plastex
-pip3 install ./plastex
-git clone [email protected]:PatrickMassot/leanblueprint
-pip3 install ./leanblueprint
-cd sphere-eversion
+pip install -r blueprint/requirements.txt
 ```
 
 To actually build the blueprint, run
 ```
 lake exe cache get
 lake build
 inv all
-```
-
-## Source reference
-
-`[GGMT]`: <https://arxiv.org/abs/2311.05762>
-
-[GGMT]: https://arxiv.org/abs/2311.05762
+``` -->