Fix a few issues

.gitignore

@@ -8,4 +8,9 @@
 *.fdb_latexmk
 *.fls
 *.log
-*.synctex.gz
+*.synctex.gz
+# Python virtual environment 
+/.venv/
+# Lean blueprint 
+/blueprint/lean_decls
+/blueprint/src/web.bbl

.vscode/settings.json

@@ -1,23 +1,22 @@
 {
     "files.exclude": {
-        "**/.git": true,
+        ".devcontainer": true,
+        ".docker": true,
         "**/.DS_Store": true,
-        "**/*.olean": true,
         "**/.DS_yml": true,
+        "**/.git": true,
         "**/.gitpod.yml": true,
         "**/.vscode": true,
-	".docker": true,
-	"build": true,
-	"html": true,
-	"lake-packages": true,
-	".gitignore": true,
-	"lake-manifest.json": true,
-	"lakefile.lean": true,
-	"lean-toolchain": true,
-	"mathematics_in_lean.pdf": true,
-    "LICENSE":true,
-    ".devcontainer":true,
-    "lean-tactics.tex":true
+        "**/*.olean": true,
+        "build": true,
+        "html": true,
+        "lake-manifest.json": true,
+        "lake-packages": true,
+        "lakefile.lean": true,
+        "lean-tactics.tex": true,
+        "lean-toolchain": true,
+        "LICENSE": true,
+        "mathematics_in_lean.pdf": true
     },
     "editor.minimap.enabled": false,
     "editor.acceptSuggestionOnEnter": "off",

blueprint/src/chapter/main.tex

@@ -9,15 +9,16 @@
 
 \date{\today}
 
+\maketitle
+
 \begin{abstract}
-    We prove  bounds for a generalized of Carleson operator on doubling metric measure spaces. We also
-    reduce explicitly Carleson's classical result on
-    pointwise control of Fourier series.
-    Both proofs are very detailed in a way suitable as blueprint for a computer verification of our results with present capability of the software package Lean. Even Carleson's classical result has not yet been computer verified.
+    We prove bounds for a generalized version of the Carleson operator on doubling metric measure spaces.
+    We also explicitly reduce Carleson's classical result on pointwise control of Fourier series.
+    Both proofs are very detailed, suitable as a blueprint for computer verification of our results with
+    the current capabilities of the software package Lean.
+    Even Carleson's classical result has not yet been computer verified.
 \end{abstract}
 
-\maketitle
-
 \tableofcontents
 
 \chapter{Introduction}
@@ -8116,7 +8117,7 @@ \section{Carleson on the real line}
 \end{proof}
 
 
-The preceeding four lemmas show that $(\R, \rho, \mu, 4)$ is a doubling metric measure space. Indeed, we even show
+The preceding four lemmas show that $(\R, \rho, \mu, 4)$ is a doubling metric measure space. Indeed, we even show
 that $(\R, \rho, \mu, 1)$ is a doubling metric measure space, but we may relax the estimate in Lemma \ref{real line doubling} to conclude that $(\R, \rho, \mu, 4)$
 is a doubling metric measure space.
 

blueprint/src/print.tex

@@ -19,11 +19,11 @@
 \usepackage{mathtools}
 \usepackage[warnings-off={mathtools-colon,mathtools-overbracket}]{unicode-math}
 \usepackage{fontspec}
-\setmathfont{Latin Modern Math}
-\setmathfont[range=\varnothing]{Asana-Math.otf}
-\setmathfont[range=\pitchfork]{Asana-Math.otf}
-\setmathfont[range=\intprod]{Asana-Math.otf}
-\setmathfont[range=\int]{Latin Modern Math}
+% \setmathfont{Latin Modern Math}
+% \setmathfont[range=\varnothing]{Asana-Math.otf}
+% \setmathfont[range=\pitchfork]{Asana-Math.otf}
+% \setmathfont[range=\intprod]{Asana-Math.otf}
+% \setmathfont[range=\int]{Latin Modern Math}
 
 \usepackage{amsthm}
 \usepackage{etexcmds}