diff --git a/.github/workflows/blueprint.yml b/.github/workflows/blueprint.yml
deleted file mode 100644
index d0287232..00000000
--- a/.github/workflows/blueprint.yml
+++ /dev/null
@@ -1,136 +0,0 @@
-name: Compile blueprint
-
-on:
- pull_request:
- push:
- branches:
- - main # Trigger on pushes to the default branch
- workflow_dispatch: # Allow manual triggering of the workflow from the GitHub Actions interface
-
-# Cancel previous runs if a new commit is pushed to the same PR or branch
-concurrency:
- group: ${{ github.ref }} # Group runs by the ref (branch or PR)
- cancel-in-progress: true # Cancel any ongoing runs in the same group
-
-# Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages
-permissions:
- contents: read # Read access to repository contents
- pages: write # Write access to GitHub Pages
- id-token: write # Write access to ID tokens
-
-jobs:
- build_project:
- runs-on: ubuntu-latest
- name: Build project
- steps:
- - name: Checkout project
- uses: actions/checkout@v4
- with:
- fetch-depth: 0 # Fetch all history for all branches and tags
-
- - name: Install elan
- run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y
-
- - name: Get Mathlib cache
- run: ~/.elan/bin/lake exe cache get || true
-
- - name: Build project
- run: ~/.elan/bin/lake build Analysis
-
- - name: Cache mathlib API docs
- uses: actions/cache@v4
- with:
- path: |
- .lake/build/doc/Init
- .lake/build/doc/Lake
- .lake/build/doc/Lean
- .lake/build/doc/Std
- .lake/build/doc/Mathlib
- .lake/build/doc/declarations
- .lake/build/doc/find
- .lake/build/doc/*.*
- !.lake/build/doc/declarations/declaration-data-Analysis*
- key: MathlibDoc-${{ hashFiles('lake-manifest.json') }}
- restore-keys: MathlibDoc-
-
- - name: Build project API documentation
- run: ~/.elan/bin/lake -R -Kenv=dev build Analysis:docs
-
- - name: Check for `home_page` folder # this is meant to detect a Jekyll-based website
- if: github.event_name != 'pull_request'
- id: check_home_page
- run: |
- if [ -d home_page ]; then
- echo "The 'home_page' folder exists in the repository."
- echo "HOME_PAGE_EXISTS=true" >> $GITHUB_ENV
- else
- echo "The 'home_page' folder does not exist in the repository."
- echo "HOME_PAGE_EXISTS=false" >> $GITHUB_ENV
- fi
-
- - name: Build blueprint and copy to `home_page/blueprint`
- if: github.event_name != 'pull_request'
- uses: xu-cheng/texlive-action@v2
- with:
- docker_image: ghcr.io/xu-cheng/texlive-full:20250101
- run: |
- # Install necessary dependencies and build the blueprint
- apk update
- apk add --update make py3-pip git pkgconfig graphviz graphviz-dev gcc musl-dev
- git config --global --add safe.directory $GITHUB_WORKSPACE
- git config --global --add safe.directory `pwd`
- python3 -m venv env
- source env/bin/activate
- pip install --upgrade pip requests wheel
- pip install pygraphviz --global-option=build_ext --global-option="-L/usr/lib/graphviz/" --global-option="-R/usr/lib/graphviz/"
- pip install leanblueprint
- leanblueprint pdf
- mkdir -p home_page
- cp blueprint/print/print.pdf home_page/blueprint.pdf
- leanblueprint web
- cp -r blueprint/web home_page/blueprint
-
- - name: Check declarations mentioned in the blueprint exist in Lean code
- if: github.event_name != 'pull_request'
- run: |
- ~/.elan/bin/lake exe checkdecls blueprint/lean_decls
-
- - name: Copy API documentation to `home_page/docs`
- if: github.event_name != 'pull_request'
- run: cp -r .lake/build/doc home_page/docs
-
- - name: Remove unnecessary lake files from documentation in `home_page/docs`
- if: github.event_name != 'pull_request'
- run: |
- find home_page/docs -name "*.trace" -delete
- find home_page/docs -name "*.hash" -delete
-
- - name: Bundle dependencies
- if: github.event_name != 'pull_request'
- uses: ruby/setup-ruby@v1
- with:
- working-directory: home_page
- ruby-version: "3.0" # Specify Ruby version
- bundler-cache: true # Enable caching for bundler
-
- - name: Build website using Jekyll
- if: github.event_name != 'pull_request' && env.HOME_PAGE_EXISTS == 'true'
- working-directory: home_page
- env:
- JEKYLL_GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
- run: JEKYLL_ENV=production bundle exec jekyll build # Note this will also copy the blueprint and API doc into home_page/_site
-
- - name: "Upload website (API documentation, blueprint and any home page)"
- if: github.event_name != 'pull_request'
- uses: actions/upload-pages-artifact@v3
- with:
- path: ${{ env.HOME_PAGE_EXISTS == 'true' && 'home_page/_site' || 'home_page/' }}
-
- - name: Deploy to GitHub Pages
- if: github.event_name != 'pull_request'
- id: deployment
- uses: actions/deploy-pages@v4
-
- - name: Make sure the API documentation cache works
- if: github.event_name != 'pull_request'
- run: mv home_page/docs .lake/build/doc
diff --git a/.github/workflows/workflows/build_book.yml b/.github/workflows/workflows/build_book.yml
new file mode 100644
index 00000000..f76a1990
--- /dev/null
+++ b/.github/workflows/workflows/build_book.yml
@@ -0,0 +1,84 @@
+name: Build book
+
+on:
+ push:
+ branches:
+ - main
+ pull_request:
+ workflow_dispatch:
+
+concurrency:
+ group: ${{ github.ref }} # Group runs by the ref (branch or PR)
+ cancel-in-progress: true # Cancel any ongoing runs in the same group
+
+defaults:
+ run:
+ working-directory: ./book
+
+jobs:
+ build:
+ runs-on: ubuntu-latest
+ steps:
+ - uses: actions/checkout@v4
+ - name: Install elan
+ run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y
+
+ - name: Get Mathlib cache
+ run: ~/.elan/bin/lake exe cache get || true
+ working-directory: ./analysis
+
+ - name: Cache mathlib API docs
+ uses: actions/cache@v4
+ with:
+ path: |
+ ./analysis/.lake/build/doc/Init
+ ./analysis/.lake/build/doc/Lake
+ ./analysis/.lake/build/doc/Lean
+ ./analysis/.lake/build/doc/Std
+ ./analysis/.lake/build/doc/Mathlib
+ ./analysis/.lake/build/doc/declarations
+ ./analysis/.lake/build/doc/find
+ ./analysis/.lake/build/doc/*.*
+ !./analysis/.lake/build/doc/declarations/declaration-data-Analysis*
+ key: MathlibDoc-${{ hashFiles('lake-manifest.json') }}
+ restore-keys: MathlibDoc-
+
+ - name: Build doc-gen
+ run: ~/.elan/bin/lake -R -Kenv=dev build Analysis:docs
+ working-directory: ./analysis
+
+ - name: Build book
+ run: |
+ ~/.elan/bin/lake exe analysis-book
+ - name: Copy docs to analysis-book
+ run: |
+ cp -r ../analysis/.lake/build/doc _site/docs
+ - name: Remove unnecessary lake files from documentation in `_site/docs`
+ run: |
+ find _site/docs -name "*.trace" -delete
+ find _site/docs -name "*.hash" -delete
+ - name: Upload website
+ uses: actions/upload-pages-artifact@v3
+ with:
+ path: './book/_site'
+ deploy:
+ # Add a dependency to the build job
+ needs: build
+
+ # Grant GITHUB_TOKEN the permissions required to make a Pages deployment
+ permissions:
+ pages: write # to deploy to Pages
+ id-token: write # to verify the deployment originates from an appropriate source
+
+ # Deploy to the github-pages environment
+ environment:
+ name: github-pages
+ url: ${{ steps.deployment.outputs.page_url }}
+
+ # Specify runner + deployment step
+ runs-on: ubuntu-latest
+ if: github.ref == 'refs/heads/main'
+ steps:
+ - name: Deploy to GitHub Pages
+ id: deployment
+ uses: actions/deploy-pages@v4
diff --git a/.gitignore b/.gitignore
index c93dfd53..f8b2b0d1 100644
--- a/.gitignore
+++ b/.gitignore
@@ -2,6 +2,7 @@
# Compiled files and directories
.lake/
build/
+_site/
# IDE files
.vscode/
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
new file mode 100644
index 00000000..a65ab7ec
--- /dev/null
+++ b/CONTRIBUTING.md
@@ -0,0 +1,23 @@
+# Contributing
+
+I would be interested in having volunteers “playtest” the companion to see if this can actually be done (and if the helper lemmas or “API” provided in the Lean files are sufficient to fill in the sorries in a conceptually straightforward manner without having to rely on more esoteric Lean programming techniques). Any other feedback will of course also be welcome.
+
+# Building the book locally
+
+Change directory to `analysis`
+Build the doc-gen
+```
+lake exe Analysis:docs
+```
+
+Change the working directory to `./book/`
+Build:
+```
+lake exe analysis-book
+```
+
+View the book:
+```
+python3 serve.py
+```
+then visit `http://localhost:8000`
\ No newline at end of file
diff --git a/README.md b/README.md
index 17a1113c..8d2e19d2 100644
--- a/README.md
+++ b/README.md
@@ -14,18 +14,18 @@ In order to align the formalization with Mathlib conventions, a small number of
Currently formalized sections:
-- [Section 2.1: The Peano axioms](https://teorth.github.io/analysis/docs/Analysis/Section_2_1.html)
-- [Section 2.2: Addition](https://teorth.github.io/analysis/docs/Analysis/Section_2_2.html)
-- [Section 2.3: Multiplication](https://teorth.github.io/analysis/docs/Analysis/Section_2_3.html)
-- [Chapter 2 epilogue: Isomorphism with the Mathlib natural numbers](https://teorth.github.io/analysis/docs/Analysis/Section_2_epilogue.html)
-- [Section 3.1: Set theory fundamentals](https://teorth.github.io/analysis/docs/Analysis/Section_3_1.html)
-- [Section 4.1: The integers](https://teorth.github.io/analysis/docs/Analysis/Section_4_1.html)
-- [Section 4.2: The rationals](https://teorth.github.io/analysis/docs/Analysis/Section_4_2.html)
-- [Section 4.3: Absolute value and exponentiation](https://teorth.github.io/analysis/docs/Analysis/Section_4_3.html)
-- [Section 5.1: Cauchy sequences of rationals](https://teorth.github.io/analysis/docs/Analysis/Section_5_1.html)
-- [Section 5.2: Equivalent Cauchy sequences](https://teorth.github.io/analysis/docs/Analysis/Section_5_2.html)
-- [Section 5.3: Construction of the real numbers](https://teorth.github.io/analysis/docs/Analysis/Section_5_3.html)
-- [Section 5.4: Ordering the reals](https://teorth.github.io/analysis/docs/Analysis/Section_5_4.html)
+- [Section 2.1: The Peano axioms](https://teorth.github.io/analysis/sec21/)
+- [Section 2.2: Addition](https://teorth.github.io/analysis/sec22/)
+- [Section 2.3: Multiplication](https://teorth.github.io/analysis/sec23/)
+- [Chapter 2 epilogue: Isomorphism with the Mathlib natural numbers](https://teorth.github.io/analysis/sec2e/)
+- [Section 3.1: Set theory fundamentals](https://teorth.github.io/analysis/sec31/)
+- [Section 4.1: The integers](https://teorth.github.io/analysis/sec41/)
+- [Section 4.2: The rationals](https://teorth.github.io/analysis/sec42/)
+- [Section 4.3: Absolute value and exponentiation](https://teorth.github.io/analysis/sec43/)
+- [Section 5.1: Cauchy sequences of rationals](https://teorth.github.io/analysis/sec51/)
+- [Section 5.2: Equivalent Cauchy sequences](https://teorth.github.io/analysis/sec52/)
+- [Section 5.3: Construction of the real numbers](https://teorth.github.io/analysis/sec53/)
+- [Section 5.4: Ordering the reals](https://teorth.github.io/analysis/sec54/)
Other resources:
@@ -34,6 +34,7 @@ Other resources:
- [Springer edition](https://link.springer.com/book/10.1007/978-981-19-7261-4)
- [Blog post announcing this project](https://terrytao.wordpress.com/2025/05/31/a-lean-companion-to-analysis-i/), Terence Tao, May 31 2025.
- [Lean Zulip discussion about this project](https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Lean.20companion.20to.20.22Analysis.20I.22.20-.20discussion/with/521458888)
+- [Notes for contributors](./CONTRIBUTING.md)
General Lean resources:
- [The Lean community](https://leanprover-community.github.io/)
diff --git a/Analysis.lean b/analysis/Analysis.lean
similarity index 70%
rename from Analysis.lean
rename to analysis/Analysis.lean
index 3c2b548a..abd4319b 100644
--- a/Analysis.lean
+++ b/analysis/Analysis.lean
@@ -1,5 +1,3 @@
--- This module serves as the root of the `Analysis` library.
--- Import modules here that should be built as part of the library.
import Analysis.Section_2_1
import Analysis.Section_2_2
import Analysis.Section_2_3
@@ -11,3 +9,4 @@ import Analysis.Section_4_3
import Analysis.Section_5_1
import Analysis.Section_5_2
import Analysis.Section_5_3
+import Analysis.Section_5_4
diff --git a/Analysis/Section_2_1.lean b/analysis/Analysis/Section_2_1.lean
similarity index 100%
rename from Analysis/Section_2_1.lean
rename to analysis/Analysis/Section_2_1.lean
diff --git a/Analysis/Section_2_2.lean b/analysis/Analysis/Section_2_2.lean
similarity index 100%
rename from Analysis/Section_2_2.lean
rename to analysis/Analysis/Section_2_2.lean
diff --git a/Analysis/Section_2_3.lean b/analysis/Analysis/Section_2_3.lean
similarity index 100%
rename from Analysis/Section_2_3.lean
rename to analysis/Analysis/Section_2_3.lean
diff --git a/Analysis/Section_2_epilogue.lean b/analysis/Analysis/Section_2_epilogue.lean
similarity index 100%
rename from Analysis/Section_2_epilogue.lean
rename to analysis/Analysis/Section_2_epilogue.lean
diff --git a/Analysis/Section_3_1.lean b/analysis/Analysis/Section_3_1.lean
similarity index 100%
rename from Analysis/Section_3_1.lean
rename to analysis/Analysis/Section_3_1.lean
diff --git a/Analysis/Section_4_1.lean b/analysis/Analysis/Section_4_1.lean
similarity index 100%
rename from Analysis/Section_4_1.lean
rename to analysis/Analysis/Section_4_1.lean
diff --git a/Analysis/Section_4_2.lean b/analysis/Analysis/Section_4_2.lean
similarity index 100%
rename from Analysis/Section_4_2.lean
rename to analysis/Analysis/Section_4_2.lean
diff --git a/Analysis/Section_4_3.lean b/analysis/Analysis/Section_4_3.lean
similarity index 100%
rename from Analysis/Section_4_3.lean
rename to analysis/Analysis/Section_4_3.lean
diff --git a/Analysis/Section_5_1.lean b/analysis/Analysis/Section_5_1.lean
similarity index 100%
rename from Analysis/Section_5_1.lean
rename to analysis/Analysis/Section_5_1.lean
diff --git a/Analysis/Section_5_2.lean b/analysis/Analysis/Section_5_2.lean
similarity index 100%
rename from Analysis/Section_5_2.lean
rename to analysis/Analysis/Section_5_2.lean
diff --git a/Analysis/Section_5_3.lean b/analysis/Analysis/Section_5_3.lean
similarity index 100%
rename from Analysis/Section_5_3.lean
rename to analysis/Analysis/Section_5_3.lean
diff --git a/Analysis/Section_5_4.lean b/analysis/Analysis/Section_5_4.lean
similarity index 100%
rename from Analysis/Section_5_4.lean
rename to analysis/Analysis/Section_5_4.lean
diff --git a/lake-manifest.json b/analysis/lake-manifest.json
similarity index 61%
rename from lake-manifest.json
rename to analysis/lake-manifest.json
index 253663f2..c253c106 100644
--- a/lake-manifest.json
+++ b/analysis/lake-manifest.json
@@ -1,145 +1,105 @@
{"version": "1.1.0",
"packagesDir": ".lake/packages",
"packages":
- [{"url": "https://github.com/leanprover/doc-gen4",
+ [{"url": "https://github.com/leanprover/subverso.git",
"type": "git",
"subDir": null,
"scope": "",
- "rev": "efe744c75a6ab384619513b9762db1cfc40b0fe4",
- "name": "«doc-gen4»",
+ "rev": "9ff8c4e0d9912170d5cfc2e5067231d5f6eaac3c",
+ "name": "subverso",
"manifestFile": "lake-manifest.json",
- "inputRev": "v4.20.0",
- "inherited": false,
- "configFile": "lakefile.lean"},
- {"url": "https://github.com/PatrickMassot/checkdecls.git",
- "type": "git",
- "subDir": null,
- "scope": "",
- "rev": "3d425859e73fcfbef85b9638c2a91708ef4a22d4",
- "name": "checkdecls",
- "manifestFile": "lake-manifest.json",
- "inputRev": null,
+ "inputRev": "main",
"inherited": false,
"configFile": "lakefile.lean"},
- {"url": "https://github.com/leanprover-community/quote4",
+ {"url": "https://github.com/leanprover-community/mathlib4.git",
"type": "git",
"subDir": null,
"scope": "",
- "rev": "2865ea099ab1dd8d6fc93381d77a4ac87a85527a",
- "name": "Qq",
+ "rev": "c211948581bde9846a99e32d97a03f0d5307c31e",
+ "name": "mathlib",
"manifestFile": "lake-manifest.json",
"inputRev": "v4.20.0",
"inherited": false,
- "configFile": "lakefile.toml"},
- {"url": "https://github.com/leanprover-community/ProofWidgets4.git",
- "type": "git",
- "subDir": null,
- "scope": "",
- "rev": "21e6a0522cd2ae6cf88e9da99a1dd010408ab306",
- "name": "proofwidgets",
- "manifestFile": "lake-manifest.json",
- "inputRev": "v0.0.60",
- "inherited": false,
"configFile": "lakefile.lean"},
- {"url": "https://github.com/leanprover-community/plausible.git",
+ {"url": "https://github.com/leanprover-community/plausible",
"type": "git",
"subDir": null,
- "scope": "",
+ "scope": "leanprover-community",
"rev": "2ac43674e92a695e96caac19f4002b25434636da",
"name": "plausible",
"manifestFile": "lake-manifest.json",
- "inputRev": "v4.20.0",
- "inherited": false,
+ "inputRev": "main",
+ "inherited": true,
"configFile": "lakefile.toml"},
- {"url": "https://github.com/leanprover-community/mathlib4.git",
+ {"url": "https://github.com/leanprover-community/LeanSearchClient",
"type": "git",
"subDir": null,
- "scope": "",
- "rev": "c211948581bde9846a99e32d97a03f0d5307c31e",
- "name": "mathlib",
+ "scope": "leanprover-community",
+ "rev": "6c62474116f525d2814f0157bb468bf3a4f9f120",
+ "name": "LeanSearchClient",
"manifestFile": "lake-manifest.json",
- "inputRev": "v4.20.0",
- "inherited": false,
- "configFile": "lakefile.lean"},
+ "inputRev": "main",
+ "inherited": true,
+ "configFile": "lakefile.toml"},
{"url": "https://github.com/leanprover-community/import-graph",
"type": "git",
"subDir": null,
- "scope": "",
+ "scope": "leanprover-community",
"rev": "a11bcb5238149ae5d8a0aa5e2f8eddf8a3a9b27d",
"name": "importGraph",
"manifestFile": "lake-manifest.json",
- "inputRev": "v4.20.0",
- "inherited": false,
- "configFile": "lakefile.toml"},
- {"url": "https://github.com/leanprover-community/batteries",
- "type": "git",
- "subDir": null,
- "scope": "",
- "rev": "7a0d63fbf8fd350e891868a06d9927efa545ac1e",
- "name": "batteries",
- "manifestFile": "lake-manifest.json",
- "inputRev": "v4.20.0",
- "inherited": false,
- "configFile": "lakefile.toml"},
- {"url": "https://github.com/mhuisi/lean4-cli",
- "type": "git",
- "subDir": null,
- "scope": "",
- "rev": "4f22c09e7ded721e6ecd3cf59221c4647ca49664",
- "name": "Cli",
- "manifestFile": "lake-manifest.json",
"inputRev": "main",
"inherited": true,
"configFile": "lakefile.toml"},
- {"url": "https://github.com/fgdorais/lean4-unicode-basic",
+ {"url": "https://github.com/leanprover-community/ProofWidgets4",
"type": "git",
"subDir": null,
- "scope": "",
- "rev": "45c426d1cb016fcb4fcbe043f1cd2d97acb2dbc3",
- "name": "UnicodeBasic",
+ "scope": "leanprover-community",
+ "rev": "21e6a0522cd2ae6cf88e9da99a1dd010408ab306",
+ "name": "proofwidgets",
"manifestFile": "lake-manifest.json",
- "inputRev": "main",
+ "inputRev": "v0.0.60",
"inherited": true,
"configFile": "lakefile.lean"},
- {"url": "https://github.com/dupuisf/BibtexQuery",
+ {"url": "https://github.com/leanprover-community/aesop",
"type": "git",
"subDir": null,
- "scope": "",
- "rev": "dbfe2b7630c5f7c5c1cf71e7747ffc0a30337f69",
- "name": "BibtexQuery",
+ "scope": "leanprover-community",
+ "rev": "ddfca7829bf8aa4083cdf9633935dddbb28b7b2a",
+ "name": "aesop",
"manifestFile": "lake-manifest.json",
"inputRev": "master",
"inherited": true,
"configFile": "lakefile.toml"},
- {"url": "https://github.com/acmepjz/md4lean",
+ {"url": "https://github.com/leanprover-community/quote4",
"type": "git",
"subDir": null,
- "scope": "",
- "rev": "8ba0ef10d178ab95a5d6fe3cfbd586c6ecef2717",
- "name": "MD4Lean",
+ "scope": "leanprover-community",
+ "rev": "2865ea099ab1dd8d6fc93381d77a4ac87a85527a",
+ "name": "Qq",
"manifestFile": "lake-manifest.json",
- "inputRev": "main",
+ "inputRev": "master",
"inherited": true,
- "configFile": "lakefile.lean"},
- {"url": "https://github.com/leanprover-community/LeanSearchClient",
+ "configFile": "lakefile.toml"},
+ {"url": "https://github.com/leanprover-community/batteries",
"type": "git",
"subDir": null,
"scope": "leanprover-community",
- "rev": "6c62474116f525d2814f0157bb468bf3a4f9f120",
- "name": "LeanSearchClient",
+ "rev": "7a0d63fbf8fd350e891868a06d9927efa545ac1e",
+ "name": "batteries",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
"inherited": true,
"configFile": "lakefile.toml"},
- {"url": "https://github.com/leanprover-community/aesop",
+ {"url": "https://github.com/leanprover/lean4-cli",
"type": "git",
"subDir": null,
- "scope": "leanprover-community",
- "rev": "ddfca7829bf8aa4083cdf9633935dddbb28b7b2a",
- "name": "aesop",
+ "scope": "leanprover",
+ "rev": "f9e25dcbed001489c53bceeb1f1d50bbaf7451d4",
+ "name": "Cli",
"manifestFile": "lake-manifest.json",
- "inputRev": "master",
+ "inputRev": "main",
"inherited": true,
"configFile": "lakefile.toml"}],
- "name": "analysis",
+ "name": "Analysis",
"lakeDir": ".lake"}
diff --git a/analysis/lakefile.lean b/analysis/lakefile.lean
new file mode 100644
index 00000000..a8ac2eea
--- /dev/null
+++ b/analysis/lakefile.lean
@@ -0,0 +1,27 @@
+import Lake
+open Lake DSL
+
+package «Analysis» where
+ -- Settings applied to both builds and interactive editing
+ leanOptions := #[
+ ⟨`pp.unicode.fun, true⟩ -- pretty-prints `fun a ↦ b`
+ ]
+ -- add any additional package configuration options here
+
+-- Require Mathlib (the comprehensive library of mathematics in Lean)
+require mathlib from git
+ "https://github.com/leanprover-community/mathlib4.git" @ "v4.20.0"
+-- Needed to build book
+require subverso from git
+ "https://github.com/leanprover/subverso.git" @ "main"
+
+
+
+@[default_target]
+lean_lib «Analysis» where
+ -- add any library configuration options here
+
+
+meta if get_config? env = some "dev" then
+require «doc-gen4» from git
+ "https://github.com/leanprover/doc-gen4" @ "v4.20.0"
diff --git a/analysis/lean-toolchain b/analysis/lean-toolchain
new file mode 100644
index 00000000..5e485899
--- /dev/null
+++ b/analysis/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.20.0
\ No newline at end of file
diff --git a/blueprint/src/blueprint.sty b/blueprint/src/blueprint.sty
deleted file mode 100644
index 1353f398..00000000
--- a/blueprint/src/blueprint.sty
+++ /dev/null
@@ -1,2 +0,0 @@
-\DeclareOption*{}
-\ProcessOptions
\ No newline at end of file
diff --git a/blueprint/src/content.tex b/blueprint/src/content.tex
deleted file mode 100644
index b5cd27b9..00000000
--- a/blueprint/src/content.tex
+++ /dev/null
@@ -1,7 +0,0 @@
-% In this file you should put the actual content of the blueprint.
-% It will be used both by the web and the print version.
-% It should *not* include the \begin{document}
-%
-% If you want to split the blueprint content into several files then
-% the current file can be a simple sequence of \input. Otherwise It
-% can start with a \section or \chapter for instance.
\ No newline at end of file
diff --git a/blueprint/src/extra_styles.css b/blueprint/src/extra_styles.css
deleted file mode 100644
index b96c7767..00000000
--- a/blueprint/src/extra_styles.css
+++ /dev/null
@@ -1,25 +0,0 @@
-/* This file contains CSS tweaks for this blueprint.
- * As an example, we included CSS rules that put
- * a vertical line on the left of theorem statements
- * and proofs.
- * */
-
-div.theorem_thmcontent {
- border-left: .15rem solid black;
-}
-
-div.proposition_thmcontent {
- border-left: .15rem solid black;
-}
-
-div.lemma_thmcontent {
- border-left: .1rem solid black;
-}
-
-div.corollary_thmcontent {
- border-left: .1rem solid black;
-}
-
-div.proof_content {
- border-left: .08rem solid grey;
-}
diff --git a/blueprint/src/latexmkrc b/blueprint/src/latexmkrc
deleted file mode 100644
index 38d59630..00000000
--- a/blueprint/src/latexmkrc
+++ /dev/null
@@ -1,5 +0,0 @@
-# This file configures the latexmk command you can use to compile
-# the pdf version of the blueprint
-$pdf_mode = 1;
-$pdflatex = 'xelatex -synctex=1';
-@default_files = ('print.tex');
\ No newline at end of file
diff --git a/blueprint/src/macros/common.tex b/blueprint/src/macros/common.tex
deleted file mode 100644
index 83d71e14..00000000
--- a/blueprint/src/macros/common.tex
+++ /dev/null
@@ -1,18 +0,0 @@
-% In this file you should put all LaTeX macros and settings to be used both by
-% the pdf version and the web version.
-% This should be most of your macros.
-
-% The theorem-like environments defined below are those that appear by default
-% in the dependency graph. See the README of leanblueprint if you need help to
-% customize this.
-% The configuration below use the theorem counter for all those environments
-% (this is what the [theorem] arguments mean) and never resets it.
-% If you want for instance to number them within chapters then you can add
-% [chapter] at the end of the next line.
-\newtheorem{theorem}{Theorem}
-\newtheorem{proposition}[theorem]{Proposition}
-\newtheorem{lemma}[theorem]{Lemma}
-\newtheorem{corollary}[theorem]{Corollary}
-
-\theoremstyle{definition}
-\newtheorem{definition}[theorem]{Definition}
\ No newline at end of file
diff --git a/blueprint/src/macros/print.tex b/blueprint/src/macros/print.tex
deleted file mode 100644
index 668fec13..00000000
--- a/blueprint/src/macros/print.tex
+++ /dev/null
@@ -1,29 +0,0 @@
-% In this file you should put macros to be used only by
-% the printed version. Of course they should have a corresponding
-% version in macros/web.tex.
-% Typically the printed version could have more fancy decorations.
-% This should be a very short file.
-%
-% This file starts with dummy macros that ensure the pdf
-% compiler will ignore macros provided by plasTeX that make
-% sense only for the web version, such as dependency graph
-% macros.
-
-
-% Dummy macros that make sense only for web version.
-\newcommand{\lean}[1]{}
-\newcommand{\discussion}[1]{}
-\newcommand{\leanok}{}
-\newcommand{\mathlibok}{}
-\newcommand{\notready}{}
-% Make sure that arguments of \uses and \proves are real labels, by using invisible refs:
-% latex prints a warning if the label is not defined, but nothing is shown in the pdf file.
-% It uses LaTeX3 programming, this is why we use the expl3 package.
-\ExplSyntaxOn
-\NewDocumentCommand{\uses}{m}
- {\clist_map_inline:nn{#1}{\vphantom{\ref{##1}}}%
- \ignorespaces}
-\NewDocumentCommand{\proves}{m}
- {\clist_map_inline:nn{#1}{\vphantom{\ref{##1}}}%
- \ignorespaces}
-\ExplSyntaxOff
\ No newline at end of file
diff --git a/blueprint/src/macros/web.tex b/blueprint/src/macros/web.tex
deleted file mode 100644
index ceee9755..00000000
--- a/blueprint/src/macros/web.tex
+++ /dev/null
@@ -1,5 +0,0 @@
-% In this file you should put macros to be used only by
-% the web version. Of course they should have a corresponding
-% version in macros/print.tex.
-% Typically the printed version could have more fancy decorations.
-% This will probably be a very short file.
\ No newline at end of file
diff --git a/blueprint/src/plastex.cfg b/blueprint/src/plastex.cfg
deleted file mode 100644
index de3dbae2..00000000
--- a/blueprint/src/plastex.cfg
+++ /dev/null
@@ -1,17 +0,0 @@
-[general]
-renderer=HTML5
-copy-theme-extras=yes
-plugins=plastexdepgraph plastexshowmore leanblueprint
-
-[document]
-toc-depth=3
-toc-non-files=True
-
-[files]
-directory=../web/
-split-level= 0
-
-[html5]
-localtoc-level=0
-extra-css=extra_styles.css
-mathjax-dollars=False
\ No newline at end of file
diff --git a/blueprint/src/print.tex b/blueprint/src/print.tex
deleted file mode 100644
index f230f867..00000000
--- a/blueprint/src/print.tex
+++ /dev/null
@@ -1,33 +0,0 @@
-% This file makes a printable version of the blueprint
-% It should include all the \usepackage needed for the pdf version.
-% The template version assume you want to use a modern TeX compiler
-% such as xeLaTeX or luaLaTeX including support for unicode
-% and Latin Modern Math font with standard bugfixes applied.
-% It also uses expl3 in order to support macros related to the dependency graph.
-% It also includes standard AMS packages (and their improved version
-% mathtools) as well as support for links with a sober decoration
-% (no ugly rectangles around links).
-% It is otherwise a very minimal preamble (you should probably at least
-% add cleveref and tikz-cd).
-
-\documentclass[a4paper]{report}
-
-\usepackage{geometry}
-
-\usepackage{expl3}
-
-\usepackage{amssymb, amsthm, mathtools}
-\usepackage[unicode,colorlinks=true,linkcolor=blue,urlcolor=magenta, citecolor=blue]{hyperref}
-
-\usepackage[warnings-off={mathtools-colon,mathtools-overbracket}]{unicode-math}
-
-\input{macros/common}
-\input{macros/print}
-
-\title{Analysis Lean companion}
-\author{Terence Tao}
-
-\begin{document}
-\maketitle
-\input{content}
-\end{document}
\ No newline at end of file
diff --git a/blueprint/src/web.tex b/blueprint/src/web.tex
deleted file mode 100644
index 7c420dc1..00000000
--- a/blueprint/src/web.tex
+++ /dev/null
@@ -1,27 +0,0 @@
-% This file makes a web version of the blueprint
-% It should include all the \usepackage needed for this version.
-% The template includes standard AMS packages.
-% It is otherwise a very minimal preamble (you should probably at least
-% add cleveref and tikz-cd).
-
-\documentclass{report}
-
-\usepackage{amssymb, amsthm, amsmath}
-\usepackage{hyperref}
-\usepackage[showmore, dep_graph]{blueprint}
-
-
-\input{macros/common}
-\input{macros/web}
-
-\home{https://teorth.github.io/analysis}
-\github{https://github.com/teorth/analysis}
-\dochome{https://teorth.github.io/analysis/docs}
-
-\title{Analysis Lean companion}
-\author{Terence Tao}
-
-\begin{document}
-\maketitle
-\input{content}
-\end{document}
\ No newline at end of file
diff --git a/book/AnalysisBook.lean b/book/AnalysisBook.lean
new file mode 100644
index 00000000..82e4398f
--- /dev/null
+++ b/book/AnalysisBook.lean
@@ -0,0 +1,75 @@
+
+import VersoBlog
+import AnalysisBook.Home
+
+open Verso Genre Blog Site Syntax
+
+open Output Html Template Theme in
+def theme : Theme := { Theme.default with
+ primaryTemplate := do
+ return {{
+
+
+
+ {{ (← param (α := String) "title") }} " — Verso "
+
+
+ {{← builtinHeader }}
+
+
+
+
+
+
+
+
+
+
+ {{ (← param "content") }}
+
+
+
+
+ }}
+ }
+ |>.override #[] ⟨do return {{
{{← param "title"}}
{{← param "content"}}
}}, id⟩
+
+
+
+def_literate_page sec21 from Analysis.Section_2_1 in "../analysis" as "The Peano Axioms"
+
+def_literate_page sec22 from Analysis.Section_2_2 in "../analysis" as "Addition"
+def_literate_page sec23 from Analysis.Section_2_3 in "../analysis" as "Multiplication"
+def_literate_page sec2e from Analysis.Section_2_epilogue in "../analysis" as "Equivalence of naturals"
+def_literate_page sec31 from Analysis.Section_3_1 in "../analysis" as "Fundamentals"
+def_literate_page sec41 from Analysis.Section_4_1 in "../analysis" as "The integers"
+def_literate_page sec42 from Analysis.Section_4_2 in "../analysis" as "The rationals"
+def_literate_page sec43 from Analysis.Section_4_3 in "../analysis" as "Absolute value and exponentiation"
+def_literate_page sec51 from Analysis.Section_5_1 in "../analysis" as "Cauchy sequences"
+def_literate_page sec52 from Analysis.Section_5_2 in "../analysis" as "Equivalent Cauchy sequences"
+def_literate_page sec53 from Analysis.Section_5_3 in "../analysis" as "The construction of the real numbers"
+def_literate_page sec54 from Analysis.Section_5_4 in "../analysis" as "Ordering the reals"
+
+def demoSite : Site := site AnalysisBook.Home /
+ static "static" ← "./static_files"
+ "sec21" sec21
+ "sec22" sec22
+ "sec23" sec23
+ "sec2e" sec2e
+ "sec31" sec31
+ "sec41" sec41
+ "sec42" sec42
+ "sec43" sec43
+ "sec51" sec51
+ "sec52" sec52
+ "sec53" sec53
+ "sec54" sec54
+
+
+def main := blogMain theme demoSite
diff --git a/book/AnalysisBook/Home.lean b/book/AnalysisBook/Home.lean
new file mode 100644
index 00000000..1af65c6d
--- /dev/null
+++ b/book/AnalysisBook/Home.lean
@@ -0,0 +1,30 @@
+import VersoBlog
+open Verso Genre Blog
+
+#doc (Page) " Partial Lean formalization of Analysis I" =>
+
+The files in this directory contain a formalization of selected portions of my text [_Analysis I_](https://terrytao.wordpress.com/books/analysis-i/) into [Lean](https://lean-lang.org/). The formalization is intended to be as faithful a paraphrasing as possible to the original text, while also showcasing Lean's features and syntax. In particular, the formalization is _not_ optimized for efficiency, and in some cases may deviate from idiomatic Lean usage.
+
+Portions of the text that were left as exercises to the reader are rendered in this translation as `sorry`s. Readers are welcome to fork the repository here to try their hand at these exercises, but I do not intend to place solutions in this repository directly.
+
+While the arrangement of definitions, theorems, and proofs here are closely paraphrasing the textbook, I am refraining from directly quoting material from the textbook, instead providing references to the original text where appropriate. As such, this formalization should be viewed as an annotated companion to the primary text, rather than a replacement for it.
+
+Much of the material in this text is duplicated in Lean's standard math library [Mathlib](https://leanprover-community.github.io/mathlib4_docs/), though with slightly different definitions. To reconcile these discrepancies, this formalization will gradually transition from the textbook-provided definitions to the Mathlib-provided definitions as one progresses further into the text, thus sacrificing the self-containedness of the formalization in favor of compatibility with Mathlib. For instance, Chapter 2 develops a theory of the natural numbers independent of Mathlib, but all subsequent chapters will use the Mathlib natural numbers instead. (An epilogue to Chapter 2 is provided to show that the two notions of the natural numbers are isomorphic.) As such, this formalization can also be used as an introduction to various portions of Mathlib.
+
+In order to align the formalization with Mathlib conventions, a small number of technical changes have been made to some of the definitions as compared with the textbook version. Most notably:
+- Sequences are indexed to start from zero rather than from one, as Mathlib has much more support for the 0-based natural numbers `ℕ` than the 1-based natural numbers.
+- Many operations that are left undefined in the text, such as division by zero, or taking the formal limit of a non-Cauchy sequence, are instead assigned a "junk" value (e.g., `0`) to make the operation totally defined. This is because Lean has better support for total functions than partial functions (indiscriminate use of the latter can lead into "dependent type hell" in which even very basic manipulations require quite subtle and delicate proofs). See for instance [this blog post](https://xenaproject.wordpress.com/2020/07/05/division-by-zero-in-type-theory-a-faq/) by Kevin Buzzard for more discussion.
+
+Currently formalized sections:
+
+- [Section 2.1: The Peano axioms](./sec21/)
+- [Section 2.2: Addition](./sec22/)
+- [Section 2.3: Multiplication](./sec23/)
+- [Chapter 2 epilogue: Isomorphism with the Mathlib natural numbers](./sec2e)
+- [Section 3.1: Set theory fundamentals](./sec31/)
+- [Section 4.1: The integers](./sec41/)
+- [Section 4.2: The rationals](./sec42/)
+- [Section 4.3: Absolute value and exponentiation](./sec43/)
+- [Section 5.1: Cauchy sequences of rationals](./sec51)
+- [Section 5.2: Equivalent Cauchy sequences](./sec52/)
+- [Section 5.3: Construction of the real numbers](./sec53/)
diff --git a/book/lake-manifest.json b/book/lake-manifest.json
new file mode 100644
index 00000000..b1d90f4f
--- /dev/null
+++ b/book/lake-manifest.json
@@ -0,0 +1,35 @@
+{"version": "1.1.0",
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"url": "https://github.com/pimotte/verso.git",
+ "type": "git",
+ "subDir": null,
+ "scope": "",
+ "rev": "a71fb6d4153ff528186aef3df20732076f71509f",
+ "name": "verso",
+ "manifestFile": "lake-manifest.json",
+ "inputRev": "analysis",
+ "inherited": false,
+ "configFile": "lakefile.lean"},
+ {"url": "https://github.com/acmepjz/md4lean",
+ "type": "git",
+ "subDir": null,
+ "scope": "",
+ "rev": "8ba0ef10d178ab95a5d6fe3cfbd586c6ecef2717",
+ "name": "MD4Lean",
+ "manifestFile": "lake-manifest.json",
+ "inputRev": "main",
+ "inherited": true,
+ "configFile": "lakefile.lean"},
+ {"url": "https://github.com/leanprover/subverso.git",
+ "type": "git",
+ "subDir": null,
+ "scope": "",
+ "rev": "a3e5c4c50791e536fc7f13a7aadd6236091796f9",
+ "name": "subverso",
+ "manifestFile": "lake-manifest.json",
+ "inputRev": "main",
+ "inherited": true,
+ "configFile": "lakefile.lean"}],
+ "name": "«analysis-book»",
+ "lakeDir": ".lake"}
diff --git a/book/lakefile.lean b/book/lakefile.lean
new file mode 100644
index 00000000..b04ec18b
--- /dev/null
+++ b/book/lakefile.lean
@@ -0,0 +1,14 @@
+import Lake
+open Lake DSL
+
+require verso from git "https://github.com/pimotte/verso.git"@"analysis"
+
+package "analysis-book" where
+ version := v!"0.1.0"
+
+lean_lib «AnalysisBook» where
+ -- add library configuration options here
+
+@[default_target]
+lean_exe "analysis-book" where
+ root := `AnalysisBook
diff --git a/book/lean-toolchain b/book/lean-toolchain
new file mode 100644
index 00000000..cfb5ca96
--- /dev/null
+++ b/book/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.20.0-rc2
\ No newline at end of file
diff --git a/book/static_files/style.css b/book/static_files/style.css
new file mode 100644
index 00000000..4a4bfc49
--- /dev/null
+++ b/book/static_files/style.css
@@ -0,0 +1,53 @@
+nav {
+ position: fixed;
+ top: 0;
+ left: 0;
+ width: 14em;
+ height: 100vh;
+ background: #f7f7fa;
+ border-right: 1px solid #ddd;
+ padding: 2em 1em 1em 1em;
+ box-sizing: border-box;
+ overflow-y: auto;
+ z-index: 100;
+}
+
+nav ol {
+ list-style: none;
+ padding: 0;
+ margin: 0;
+}
+
+nav ol li {
+ margin-bottom: 1em;
+}
+
+nav ol li a {
+ display: block;
+ color: #222;
+ text-decoration: none;
+ padding: 0.5em 0.75em;
+ border-radius: 4px;
+ transition: background 0.2s;
+}
+
+nav ol li a:hover,
+nav ol li a:focus {
+ background: #e0e0f0;
+ color: #000;
+}
+
+/* Add left margin to main content to avoid overlap */
+header,
+div.main {
+ margin-left: 16em;
+}
+
+code span {
+ font-family: "Source Code Pro" "Noto sans mono", monospace;
+ font-size: 15px;
+}
+
+body {
+ font-family: "Source Sans 3","Helvetica Neue","Segoe UI","Roboto",Arial,sans-serif;
+}
\ No newline at end of file
diff --git a/home_page/404.html b/home_page/404.html
deleted file mode 100644
index fcebf3fc..00000000
--- a/home_page/404.html
+++ /dev/null
@@ -1,25 +0,0 @@
----
-permalink: /404.html
-layout: default
----
-
-
-
-