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 - +* [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`. + +