From 5b3989277b8c98a605412d2372a51a9882eb4e41 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpvdoorn@gmail.com>
Date: Wed, 3 Apr 2024 17:29:28 +0200
Subject: [PATCH] add package, some updates to webpage

---
 blueprint/src/chapter/main.tex    |  2 ++
 blueprint/src/preamble/common.tex |  1 +
 docs/_config.yml                  |  4 ++--
 docs/index.md                     | 31 ++++++++++---------------------
 4 files changed, 15 insertions(+), 23 deletions(-)

diff --git a/blueprint/src/chapter/main.tex b/blueprint/src/chapter/main.tex
index 4709ac2e..bb8aac9f 100644
--- a/blueprint/src/chapter/main.tex
+++ b/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}
diff --git a/blueprint/src/preamble/common.tex b/blueprint/src/preamble/common.tex
index d89bca07..0cc74e74 100644
--- a/blueprint/src/preamble/common.tex
+++ b/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.}}
diff --git a/docs/_config.yml b/docs/_config.yml
index d94df2bd..f7f54410 100644
--- a/docs/_config.yml
+++ b/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: your-email@example.com
-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
diff --git a/docs/index.md b/docs/index.md
index ae18f4d4..e92ed304 100644
--- a/docs/index.md
+++ b/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,17 +25,15 @@ 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 git@github.com:plastex/plastex
-pip3 install ./plastex
-git clone git@github.com:PatrickMassot/leanblueprint
-pip3 install ./leanblueprint
-cd sphere-eversion
+pip install -r blueprint/requirements.txt
 ```
 
 To actually build the blueprint, run
@@ -46,10 +41,4 @@ 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
+``` -->