diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index ac5060e..884d62f 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -19,13 +19,12 @@ jobs:
     name: Build project
     steps:
       - name: Checkout project
-        uses: actions/checkout@v2
-        with:
-          fetch-depth: 0
+        uses: actions/checkout@v4
       - name: Install elan
-        run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover/lean4:4.0.0
+        run: |
+          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y
+          echo "$HOME/.elan/bin" >> $GITHUB_PATH
       - name: Get cache
-        run: ~/.elan/bin/lake -Kenv=dev exe cache get || true
+        run: lake exe cache get || true
       - name: Build project
-        run: ~/.elan/bin/lake -Kenv=dev build Birkhoff
- 
+        run: lake build
\ No newline at end of file
diff --git a/.gitignore b/.gitignore
index bd37e55..fdab8e0 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,6 +1,10 @@
-/build
-/lake-packages
+# Created by `lake exe cache get` if no home directory is available
 /.cache
-/.lake
+# Prior to v4.3.0-rc2 lake stored files in these locations.
+/build/
+/lake-packages/
 /lakefile.olean
-.DS_Store
\ No newline at end of file
+# After v4.3.0-rc2 lake stores its files here:
+/.lake/
+# macOS leaves these files everywhere:
+.DS_Store
diff --git a/.vscode/extensions.json b/.vscode/extensions.json
new file mode 100644
index 0000000..54b27a8
--- /dev/null
+++ b/.vscode/extensions.json
@@ -0,0 +1,5 @@
+{
+    "recommendations": [
+        "leanprover.lean4",
+    ]
+}
\ No newline at end of file
diff --git a/.vscode/settings.json b/.vscode/settings.json
new file mode 100644
index 0000000..f06ff95
--- /dev/null
+++ b/.vscode/settings.json
@@ -0,0 +1,10 @@
+{
+  "editor.insertSpaces": true,
+  "editor.tabSize": 2,
+  "editor.rulers": [100],
+  "files.encoding": "utf8",
+  "files.eol": "\n",
+  "files.insertFinalNewline": true,
+  "files.trimFinalNewlines": true,
+  "files.trimTrailingWhitespace": true
+}
diff --git a/BET.lean b/BET.lean
new file mode 100644
index 0000000..d834994
--- /dev/null
+++ b/BET.lean
@@ -0,0 +1,4 @@
+-- This module serves as the root of the `BET` library.
+-- Import modules here that should be built as part of the library.
+import «BET».Birkhoff
+import «BET».Topological
diff --git a/BET/Birkhoff.lean b/BET/Birkhoff.lean
new file mode 100644
index 0000000..28286e1
--- /dev/null
+++ b/BET/Birkhoff.lean
@@ -0,0 +1,61 @@
+import Mathlib.Tactic
+import Mathlib.Dynamics.OmegaLimit
+import Mathlib.Dynamics.Ergodic.AddCircle
+
+/-!
+# Birkhoff's ergodic theorem
+
+This file defines Birkhoff sums, other related notions and proves Birkhoff's ergodic theorem.
+
+## Implementation notes
+
+...
+
+## References
+
+* ....
+
+-/
+
+section Ergodic_Theory
+
+open BigOperators MeasureTheory
+
+/- standing assumptions: `f` is a measure preserving map of a probability space `(α, μ)`, and
+`g : α → ℝ` is integrable. -/
+
+variable {α : Type _} [MetricSpace α] [CompactSpace α] [MeasurableSpace α] [BorelSpace α]
+  {μ : MeasureTheory.Measure α} [IsProbabilityMeasure μ] {f : α → α}
+  (hf : MeasurePreserving f μ) {g : α → ℝ} (hg : Integrable g μ)
+
+
+/- Define Birkhoff sums. -/
+noncomputable def birkhoffSum {α : Type _} (f : α → α) (g : α → ℝ) (n : ℕ) (x : α) : ℝ :=
+  1 / n * (∑ i in Finset.range n, g (f^[i] x))
+
+
+/- Define the invariant sigma-algebra of `f` -/
+
+
+
+/- Main lemma to prove Birkhoff ergodic theorem:
+assume that the integral of `g` on any invariant set is strictly negative. Then, almost everywhere,
+the Birkhoff sums `S_n g x` are bounded above.
+-/
+
+
+/- Deduce Birkhoff theorem from the main lemma, in the form that almost surely, `S_n f / n`
+converges to the conditional expectation of `f` given the invariant sigma-algebra. -/
+
+
+/- If `f` is ergodic, show that the invariant sigma-algebra is ae trivial -/
+
+
+/- Show that the conditional expectation with respect to an ae trivial subalgebra is ae
+the integral. -/
+
+
+/- Give Birkhoff theorem for ergodic maps -/
+
+
+end Ergodic_Theory
diff --git a/Birkhoff.lean b/BET/Topological.lean
similarity index 83%
rename from Birkhoff.lean
rename to BET/Topological.lean
index a00411d..10cb83e 100644
--- a/Birkhoff.lean
+++ b/BET/Topological.lean
@@ -2,34 +2,43 @@ import Mathlib.Tactic
 import Mathlib.Dynamics.OmegaLimit
 import Mathlib.Dynamics.Ergodic.AddCircle
 
+/-!
+# Topological dynamics
+
+This file defines Birkhoff sums, other related notions and proves Birkhoff's ergodic theorem.
+
+## Implementation notes
+
+We could do everything in a topological space, using filters and neighborhoods, but it will
+be more comfortable with a metric space.
+
+TODO: at some point translate to topological spaces
+
+## References
+
+* ....
+
+-/
+
 open MeasureTheory Filter Metric Function Set
 open scoped omegaLimit
 set_option autoImplicit false
 
-/- For every objective, first write down a statement that Lean understands, with a proof given
-by `sorry`. Then try to prove it! -/
-
 section Topological_Dynamics
 
-/- TODO: at some point translate to topological spaces -/
-
-/- We could do everything in a topological space, using filters and neighborhoods, but it will
-be more comfortable with a metric space. -/
 variable {α : Type _} [MetricSpace α]
 
-/- Define the non-wandering set of `f`-/
+/-- The non-wandering set of `f` is the set of points which return arbitrarily close after some iterate. -/
 def nonWanderingSet (f : α → α) : Set α :=
   {x | ∀ ε, 0 < ε → ∃ (y : α), ∃ (n : ℕ), y ∈ ball x ε ∧ f^[n] y ∈ ball x ε ∧ n ≠ 0}
 
 variable [CompactSpace α] (f : α → α) (hf : Continuous f)
 
-/- Show that periodic points belong to the non-wandering set -/
+/-- Periodic points belong to the non-wandering set. -/
 theorem periodicpts_is_mem (x : α) (n : ℕ) (nnz: n ≠ 0) (pp: IsPeriodicPt f n x) :
     x ∈ nonWanderingSet f := by
   intro ε hε
   use x, n
-  -- unfold IsPeriodicPt at pp
-  -- unfold IsFixedPt at pp
   refine' ⟨_, _, _⟩
   . exact mem_ball_self hε
   . rw [pp]
@@ -56,7 +65,6 @@ lemma inter_subset_empty_of_inter_empty (A : Set α) (B: Set α) (C : Set α) (D
   exact Iff.mp subset_empty_iff hincl
   done
 
-/- Un lemme d'exercice: boules separees  -/
 lemma separated_balls (x : α) (hfx : x ≠ f x) :  ∃ ε, 0 < ε ∧ (ball x ε) ∩ (f '' (ball x ε)) = ∅ := by
    have hfC : ContinuousAt f x := Continuous.continuousAt hf
    rw [Metric.continuousAt_iff] at hfC
@@ -94,7 +102,7 @@ lemma separated_balls (x : α) (hfx : x ≠ f x) :  ∃ ε, 0 < ε ∧ (ball x 
      · exact fun l => l.elim
    done
 
--- Perhaps this should go inside Mathlib.Dynamics.PeriodicPts.lean
+/-- The set of points which are not periodic of any period. -/
 def IsNotPeriodicPt (f : α → α)  (x : α) := ∀ n : ℕ, 0 < n -> ¬IsPeriodicPt f n x
 
 lemma separated_ball_image_ball (n : ℕ) (hn : 0 < n) (x : α) (hfx : IsNotPeriodicPt f x) :  ∃ (ε : ℝ), 0 < ε ∧ (ball x ε) ∩ (f^[n] '' (ball x ε)) = ∅ := by
@@ -272,22 +280,20 @@ theorem is_closed : IsClosed (nonWanderingSet f : Set α) := by
   done
 
 
-/- Show that the non-wandering set of `f` is compact. -/
+/-- The non-wandering set of `f` is compact. -/
 theorem is_cpt : IsCompact (nonWanderingSet f : Set α) := by
   apply isCompact_of_isClosed_isBounded
   . exact is_closed f
   . exact isBounded_of_compactSpace
   done
 
-/- Show that the omega-limit set of any point is nonempty. -/
-/- Click F12 on ω⁺ below to go to its definition, and browse a little bit the file to get a
-feel of what is already there. -/
+/-- The omega-limit set of any point is nonempty. -/
 theorem omegaLimit_nonempty (x : α) : Set.Nonempty (ω⁺ (fun n ↦ f^[n]) ({x})) := by
   apply nonempty_omegaLimit atTop (fun n ↦ f^[n]) {x}
   exact Set.singleton_nonempty x
   done
 
-/- Show that the omega-limit set of any point is contained in the non-wandering set. -/
+/-- The omega-limit set of any point is contained in the non-wandering set. -/
 theorem omegaLimit_nonwandering (x : α) :
     (ω⁺ (fun n ↦ f^[n]) ({x})) ⊆ (nonWanderingSet f) := by
   intro z hz
@@ -315,11 +321,10 @@ theorem omegaLimit_nonwandering (x : α) :
     rw [this]
     apply (hf 2)
   . simp
-    apply hφ
-    norm_num
+    exact Nat.sub_ne_zero_of_lt (hφ Nat.le.refl)
   done
 
-/- Show that the non-wandering set is non-empty -/
+/-- The non-wandering set is non-empty -/
 theorem nonWandering_nonempty [hα : Nonempty α] : Set.Nonempty (nonWanderingSet f) := by
   have (x : α) : Set.Nonempty (ω⁺ (fun n ↦ f^[n]) ({x})) -> Set.Nonempty (nonWanderingSet f) := by
     apply Set.Nonempty.mono
@@ -330,8 +335,7 @@ theorem nonWandering_nonempty [hα : Nonempty α] : Set.Nonempty (nonWanderingSe
   done
 
 
-/- Define the recurrent set of `f`. The recurrent set is the set of points that are recurrent,
-   i.e. that belong to their omega-limit set. -/
+/-- The recurrent set is the set of points that are recurrent, i.e. that belong to their omega-limit set. -/
 def recurrentSet {α : Type _} [TopologicalSpace α] (f : α → α) : Set α :=
   { x | x ∈ ω⁺ (fun n ↦ f^[n]) ({x}) }
 
@@ -363,7 +367,7 @@ theorem recurrentSet_iff_accumulation_point (x : α) :
     exact ⟨m, hm, mem_of_subset_of_mem ball_in_U fm_in_ball⟩
   done
 
-/- Show that periodic points belong to the recurrent set. -/
+/-- Periodic points belong to the recurrent set. -/
 theorem periodicpts_mem_recurrentSet
     (x : α) (n : ℕ) (nnz: n ≠ 0) (hx: IsPeriodicPt f n x) :
     x ∈ recurrentSet f := by
@@ -390,7 +394,7 @@ theorem periodicpts_mem_recurrentSet
   apply x_in_omegaLimit
   done
 
-/- Show that the recurrent set is included in the non-wandering set -/
+/-- The recurrent set is included in the non-wandering set -/
 theorem recurrentSet_nonwandering : recurrentSet f ⊆ (nonWanderingSet f) := by
   intro z hz
   unfold recurrentSet at hz
@@ -399,29 +403,22 @@ theorem recurrentSet_nonwandering : recurrentSet f ⊆ (nonWanderingSet f) := by
   exact hz
   done
 
-/- Define minimal subsets for `f`, as closed invariant subsets in which all orbits are dense.
-   Note that `IsInvariant.isInvariant_iff_image` is a useful function when we use `invariant`.
-   Using a structure here allows us to get the various properties via dot notation,
-   search e.g. for `hf.minimal` below -/
+/-- The minimal subsets are the closed invariant subsets in which all orbits are dense. -/
 structure IsMinimalSubset (f : α → α) (U : Set α) : Prop :=
   (closed : IsClosed U)
   (invariant: IsInvariant (fun n x => f^[n] x) U)
   (minimal: ∀ (x y : α) (_: x ∈ U) (_: y ∈ U) (ε : ℝ), ε > 0 -> ∃ n : ℕ, f^[n] y ∈ ball x ε)
 
-/- Define a minimal dynamics (all orbits are dense) -/
+/-- A dynamical system (α,f) is minimal if α is a minimal subset. -/
 def IsMinimal (f : α → α) : Prop := IsMinimalSubset f univ
 
-/- Show that in a minimal dynamics, the recurrent set is all the space -/
+/-- In a minimal dynamics, the recurrent set is all the space. -/
 theorem recurrentSet_of_minimal_is_all_space (hf: IsMinimal f) :
     ∀ x : α, x ∈ recurrentSet f := by
   intro z
-  -- unfold recurrentSet
-  -- unfold IsMinimal at hf
-  -- simp
   have : ∀ (x : α) (ε : ℝ) (N : ℕ), ε > 0
          -> ∃ m : ℕ, m ≥ N ∧ f^[m] x ∈ ball x ε := by
     intro x ε N hε
-    -- rcases (hf x (f^[N] x) ε hε) with ⟨n, hball⟩
     obtain ⟨n, hball⟩ : ∃ n, f^[n] (f^[N] x) ∈ ball x ε :=
       hf.minimal x (f^[N] x) (mem_univ _) (mem_univ _) ε hε
     refine' ⟨n + N, _, _⟩
@@ -433,11 +430,11 @@ theorem recurrentSet_of_minimal_is_all_space (hf: IsMinimal f) :
   exact this z
   done
 
--- An example to learn to define maps on the unit interval
+/-- The doubling map is the classic interval map -/
 noncomputable def doubling_map (x : unitInterval) : unitInterval :=
   ⟨Int.fract (2 * x), by exact unitInterval.fract_mem (2 * x)⟩
 
-/- Give an example of a continuous dynamics on a compact space in which the recurrent set is all
+/-- An example of a continuous dynamics on a compact space in which the recurrent set is all
 the space, but the dynamics is not minimal -/
 example : ¬IsMinimal (id : unitInterval -> unitInterval) := by
   intro H
@@ -469,7 +466,7 @@ example (x : unitInterval) :
   done
 
 
-/- Show that every point in a minimal subset is recurrent -/
+/-- Every point in a minimal subset is recurrent. -/
 theorem minimalSubset_mem_recurrentSet (U : Set α) (hU: IsMinimalSubset f U) :
       U ⊆ recurrentSet f := by
   intro x hx
@@ -497,60 +494,17 @@ theorem minimalSubset_mem_recurrentSet (U : Set α) (hU: IsMinimalSubset f U) :
     exact hball
   done
 
-/- Show that every invariant nonempty closed subset contains at least a minimal invariant subset,
-using Zorn lemma. -/
+/-- Every invariant nonempty closed subset contains at least a minimal invariant subset. -/
 theorem nonempty_invariant_closed_subset_has_minimalSubset
     (U : Set α) (hne: Nonempty U) (hC: IsClosed U) (hI: IsInvariant (fun n x => f^[n] x) U) :
     ∃ V : Set α, V ⊆ U -> (hinv: MapsTo f U U) -> IsMinimalSubset f U := by
+  -- This follows from Zorn's lemma
   sorry
 
 
 
-/- Show that the recurrent set of `f` is nonempty -/
+/-- The recurrent set of `f` is nonempty -/
 theorem recurrentSet_nonempty [Nonempty α]: Set.Nonempty (recurrentSet f) := by
   sorry
 
 end Topological_Dynamics
-
-section Ergodic_Theory
-
-open BigOperators
-
-/- standing assumptions: `f` is a measure preserving map of a probability space `(α, μ)`, and
-`g : α → ℝ` is integrable. -/
-
-variable {α : Type _} [MetricSpace α] [CompactSpace α] [MeasurableSpace α] [BorelSpace α]
-  {μ : MeasureTheory.Measure α} [IsProbabilityMeasure μ] {f : α → α}
-  (hf : MeasurePreserving f μ) {g : α → ℝ} (hg : Integrable g μ)
-
-
-/- Define Birkhoff sums. -/
-noncomputable def birkhoffSum {α : Type _} (f : α → α) (g : α → ℝ) (n : ℕ) (x : α) : ℝ :=
-  1 / n * (∑ i in Finset.range n, g (f^[i] x))
-
-
-/- Define the invariant sigma-algebra of `f` -/
-
-
-
-/- Main lemma to prove Birkhoff ergodic theorem:
-assume that the integral of `g` on any invariant set is strictly negative. Then, almost everywhere,
-the Birkhoff sums `S_n g x` are bounded above.
--/
-
-
-/- Deduce Birkhoff theorem from the main lemma, in the form that almost surely, `S_n f / n`
-converges to the conditional expectation of `f` given the invariant sigma-algebra. -/
-
-
-/- If `f` is ergodic, show that the invariant sigma-algebra is ae trivial -/
-
-
-/- Show that the conditional expectation with respect to an ae trivial subalgebra is ae
-the integral. -/
-
-
-/- Give Birkhoff theorem for ergodic maps -/
-
-
-end Ergodic_Theory
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
new file mode 100644
index 0000000..b3aaa7a
--- /dev/null
+++ b/CONTRIBUTING.md
@@ -0,0 +1,19 @@
+# Contributing to this project
+
+We welcome anyone who can contribute something to this project.
+
+## Discussion
+
+Mostly discussion related to the project happens on Zulip.
+
+## Style
+
+We aim to follow the Mathlib style guidelines for all definitions, statements, proofs and documentation.
+
+- [Library Style Guidelines](https://leanprover-community.github.io/contribute/style.html)
+- [Documentation style](https://leanprover-community.github.io/contribute/doc.html)
+- [Mathlib naming conventions](https://leanprover-community.github.io/contribute/naming.html)
+
+## Collaborating on this project
+
+Contributions should be made by forking the repo and then opening a pull request. Most often some discussion in advance is useful.
diff --git a/LICENSE b/LICENSE
new file mode 100644
index 0000000..8dada3e
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,201 @@
+                                 Apache License
+                           Version 2.0, January 2004
+                        http://www.apache.org/licenses/
+
+   TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION
+
+   1. Definitions.
+
+      "License" shall mean the terms and conditions for use, reproduction,
+      and distribution as defined by Sections 1 through 9 of this document.
+
+      "Licensor" shall mean the copyright owner or entity authorized by
+      the copyright owner that is granting the License.
+
+      "Legal Entity" shall mean the union of the acting entity and all
+      other entities that control, are controlled by, or are under common
+      control with that entity. For the purposes of this definition,
+      "control" means (i) the power, direct or indirect, to cause the
+      direction or management of such entity, whether by contract or
+      otherwise, or (ii) ownership of fifty percent (50%) or more of the
+      outstanding shares, or (iii) beneficial ownership of such entity.
+
+      "You" (or "Your") shall mean an individual or Legal Entity
+      exercising permissions granted by this License.
+
+      "Source" form shall mean the preferred form for making modifications,
+      including but not limited to software source code, documentation
+      source, and configuration files.
+
+      "Object" form shall mean any form resulting from mechanical
+      transformation or translation of a Source form, including but
+      not limited to compiled object code, generated documentation,
+      and conversions to other media types.
+
+      "Work" shall mean the work of authorship, whether in Source or
+      Object form, made available under the License, as indicated by a
+      copyright notice that is included in or attached to the work
+      (an example is provided in the Appendix below).
+
+      "Derivative Works" shall mean any work, whether in Source or Object
+      form, that is based on (or derived from) the Work and for which the
+      editorial revisions, annotations, elaborations, or other modifications
+      represent, as a whole, an original work of authorship. For the purposes
+      of this License, Derivative Works shall not include works that remain
+      separable from, or merely link (or bind by name) to the interfaces of,
+      the Work and Derivative Works thereof.
+
+      "Contribution" shall mean any work of authorship, including
+      the original version of the Work and any modifications or additions
+      to that Work or Derivative Works thereof, that is intentionally
+      submitted to Licensor for inclusion in the Work by the copyright owner
+      or by an individual or Legal Entity authorized to submit on behalf of
+      the copyright owner. For the purposes of this definition, "submitted"
+      means any form of electronic, verbal, or written communication sent
+      to the Licensor or its representatives, including but not limited to
+      communication on electronic mailing lists, source code control systems,
+      and issue tracking systems that are managed by, or on behalf of, the
+      Licensor for the purpose of discussing and improving the Work, but
+      excluding communication that is conspicuously marked or otherwise
+      designated in writing by the copyright owner as "Not a Contribution."
+
+      "Contributor" shall mean Licensor and any individual or Legal Entity
+      on behalf of whom a Contribution has been received by Licensor and
+      subsequently incorporated within the Work.
+
+   2. Grant of Copyright License. Subject to the terms and conditions of
+      this License, each Contributor hereby grants to You a perpetual,
+      worldwide, non-exclusive, no-charge, royalty-free, irrevocable
+      copyright license to reproduce, prepare Derivative Works of,
+      publicly display, publicly perform, sublicense, and distribute the
+      Work and such Derivative Works in Source or Object form.
+
+   3. Grant of Patent License. Subject to the terms and conditions of
+      this License, each Contributor hereby grants to You a perpetual,
+      worldwide, non-exclusive, no-charge, royalty-free, irrevocable
+      (except as stated in this section) patent license to make, have made,
+      use, offer to sell, sell, import, and otherwise transfer the Work,
+      where such license applies only to those patent claims licensable
+      by such Contributor that are necessarily infringed by their
+      Contribution(s) alone or by combination of their Contribution(s)
+      with the Work to which such Contribution(s) was submitted. If You
+      institute patent litigation against any entity (including a
+      cross-claim or counterclaim in a lawsuit) alleging that the Work
+      or a Contribution incorporated within the Work constitutes direct
+      or contributory patent infringement, then any patent licenses
+      granted to You under this License for that Work shall terminate
+      as of the date such litigation is filed.
+
+   4. Redistribution. You may reproduce and distribute copies of the
+      Work or Derivative Works thereof in any medium, with or without
+      modifications, and in Source or Object form, provided that You
+      meet the following conditions:
+
+      (a) You must give any other recipients of the Work or
+          Derivative Works a copy of this License; and
+
+      (b) You must cause any modified files to carry prominent notices
+          stating that You changed the files; and
+
+      (c) You must retain, in the Source form of any Derivative Works
+          that You distribute, all copyright, patent, trademark, and
+          attribution notices from the Source form of the Work,
+          excluding those notices that do not pertain to any part of
+          the Derivative Works; and
+
+      (d) If the Work includes a "NOTICE" text file as part of its
+          distribution, then any Derivative Works that You distribute must
+          include a readable copy of the attribution notices contained
+          within such NOTICE file, excluding those notices that do not
+          pertain to any part of the Derivative Works, in at least one
+          of the following places: within a NOTICE text file distributed
+          as part of the Derivative Works; within the Source form or
+          documentation, if provided along with the Derivative Works; or,
+          within a display generated by the Derivative Works, if and
+          wherever such third-party notices normally appear. The contents
+          of the NOTICE file are for informational purposes only and
+          do not modify the License. You may add Your own attribution
+          notices within Derivative Works that You distribute, alongside
+          or as an addendum to the NOTICE text from the Work, provided
+          that such additional attribution notices cannot be construed
+          as modifying the License.
+
+      You may add Your own copyright statement to Your modifications and
+      may provide additional or different license terms and conditions
+      for use, reproduction, or distribution of Your modifications, or
+      for any such Derivative Works as a whole, provided Your use,
+      reproduction, and distribution of the Work otherwise complies with
+      the conditions stated in this License.
+
+   5. Submission of Contributions. Unless You explicitly state otherwise,
+      any Contribution intentionally submitted for inclusion in the Work
+      by You to the Licensor shall be under the terms and conditions of
+      this License, without any additional terms or conditions.
+      Notwithstanding the above, nothing herein shall supersede or modify
+      the terms of any separate license agreement you may have executed
+      with Licensor regarding such Contributions.
+
+   6. Trademarks. This License does not grant permission to use the trade
+      names, trademarks, service marks, or product names of the Licensor,
+      except as required for reasonable and customary use in describing the
+      origin of the Work and reproducing the content of the NOTICE file.
+
+   7. Disclaimer of Warranty. Unless required by applicable law or
+      agreed to in writing, Licensor provides the Work (and each
+      Contributor provides its Contributions) on an "AS IS" BASIS,
+      WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
+      implied, including, without limitation, any warranties or conditions
+      of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A
+      PARTICULAR PURPOSE. You are solely responsible for determining the
+      appropriateness of using or redistributing the Work and assume any
+      risks associated with Your exercise of permissions under this License.
+
+   8. Limitation of Liability. In no event and under no legal theory,
+      whether in tort (including negligence), contract, or otherwise,
+      unless required by applicable law (such as deliberate and grossly
+      negligent acts) or agreed to in writing, shall any Contributor be
+      liable to You for damages, including any direct, indirect, special,
+      incidental, or consequential damages of any character arising as a
+      result of this License or out of the use or inability to use the
+      Work (including but not limited to damages for loss of goodwill,
+      work stoppage, computer failure or malfunction, or any and all
+      other commercial damages or losses), even if such Contributor
+      has been advised of the possibility of such damages.
+
+   9. Accepting Warranty or Additional Liability. While redistributing
+      the Work or Derivative Works thereof, You may choose to offer,
+      and charge a fee for, acceptance of support, warranty, indemnity,
+      or other liability obligations and/or rights consistent with this
+      License. However, in accepting such obligations, You may act only
+      on Your own behalf and on Your sole responsibility, not on behalf
+      of any other Contributor, and only if You agree to indemnify,
+      defend, and hold each Contributor harmless for any liability
+      incurred by, or claims asserted against, such Contributor by reason
+      of your accepting any such warranty or additional liability.
+
+   END OF TERMS AND CONDITIONS
+
+   APPENDIX: How to apply the Apache License to your work.
+
+      To apply the Apache License to your work, attach the following
+      boilerplate notice, with the fields enclosed by brackets "{}"
+      replaced with your own identifying information. (Don't include
+      the brackets!)  The text should be enclosed in the appropriate
+      comment syntax for the file format. We also recommend that a
+      file or class name and description of purpose be included on the
+      same "printed page" as the copyright notice for easier
+      identification within third-party archives.
+
+   Copyright {yyyy} {name of copyright owner}
+
+   Licensed under the Apache License, Version 2.0 (the "License");
+   you may not use this file except in compliance with the License.
+   You may obtain a copy of the License at
+
+       http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS,
+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+   See the License for the specific language governing permissions and
+   limitations under the License.
diff --git a/README.md b/README.md
index 9adeadd..cd1eaf6 100644
--- a/README.md
+++ b/README.md
@@ -1,30 +1,33 @@
-# Birkhoff's ergodic theorem in LEAN4
+# Birkhoff's ergodic theorem in Lean 4
 
 ![Lean build](https://github.com/mseri/birkhoff/actions/workflows/build.yml/badge.svg)
 
-This repository contains the output of our project
-at the [Machine-Checked Mathematics Workshop](https://www.lorentzcenter.nl/machine-checked-mathematics.html)
-at the Lorentz Center, 10-14 July 2023.
+This project was initiated at the [Machine-Checked Mathematics Workshop](https://www.lorentzcenter.nl/machine-checked-mathematics.html) at the Lorentz Center, 10-14 July 2023.
 
-The project was developed with @marcolenci and Guillaume Dubach,
-under the support and supervision of Sébastien Gouëzel.
+Developed with @mseri, @marcolenci and Guillaume Dubach, under the support and supervision of Sébastien Gouëzel.
 
 ## How to use
 
-I am assuming you have already lean4 and mathlib4 installed.
-If not, [start here](https://leanprover-community.github.io/).
+Make sure that Lean 4 is installed, if not, [start here](https://leanprover-community.github.io/).
+
+Clone this repo
 
-To start your project, clone this repo with
 ```
 git clone https://github.com/mseri/birkhoff.git
 ```
+
 then enter the folder
+
 ```
 cd birkhoff
 ```
-and download mathlib's cache with
+
+download mathlib's cache
+
 ```
 lake exe cache get
 ```
 
-The project file is `Birkhoff.lean`.
+and open the folder in vscode to view and edit the Lean code.
+
+[Contribution guidelines](CONTRIBUTING.md) for this project.
diff --git a/lake-manifest.json b/lake-manifest.json
index d30d713..4be01b7 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "0d0ac1c43e1ec1965e0806af9e7a32999ea31096",
+   "rev": "4c366aba55d28778421b8a1841e5512fd5c53c43",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -13,7 +13,7 @@
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
-   "rev": "1c88406514a636d241903e2e288d21dc6d861e01",
+   "rev": "fd760831487e6835944e7eeed505522c9dd47563",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -22,7 +22,7 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "24a4e8fea81999723bfc38bebf7adc86c2f26c6c",
+   "rev": "e4660fa21444bcfe5c70d37b09cc0517accd8ad7",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -31,10 +31,10 @@
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "8dd18350791c85c0fc9adbd6254c94a81d260d35",
+   "rev": "f5b2b6ff817890d85ffd8ed47637e36fcac544a6",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.25",
+   "inputRev": "v0.0.28",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
@@ -49,7 +49,7 @@
   {"url": "https://github.com/leanprover-community/import-graph.git",
    "type": "git",
    "subDir": null,
-   "rev": "7d051a52c49ac25ee5a04c7a2a70148cc95ddab3",
+   "rev": "64d082eeaad1a8e6bbb7c23b7a16b85a1715a02f",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -58,7 +58,7 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "19ab970d5f9f0204e7bb92cb15cf9862bf3ef449",
+   "rev": "410db9009f4e34a6bcd70cd795bba47e0222502a",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
diff --git a/lakefile.lean b/lakefile.lean
index 192a6db..e1f614c 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -1,14 +1,18 @@
 import Lake
 open Lake DSL
 
-package «Birkhoff» {
-  -- add any package configuration options here
-}
+package «BET» where
+  -- Settings applied to both builds and interactive editing
+  leanOptions := #[
+    ⟨`pp.unicode.fun, true⟩, -- pretty-prints `fun a ↦ b`
+    ⟨`pp.proofs.withType, false⟩
+  ]
+  -- add any additional package configuration options here
 
 require mathlib from git
   "https://github.com/leanprover-community/mathlib4.git"
 
 @[default_target]
-lean_lib «Birkhoff» {
+lean_lib «BET» {
   -- add any library configuration options here
 }
diff --git a/lean-toolchain b/lean-toolchain
index 3f21e50..cfcdd32 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.5.0-rc1
+leanprover/lean4:v4.6.0-rc1