1.4.1

analysis/Analysis/MeasureTheory/README.md

@@ -2,11 +2,7 @@
 
 The files in this directory contain a formalization of my text [_An introduction to measure theory_](https://terrytao.wordpress.com/books/an-introduction-to-measure-theory/) 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, as well as many of the proofs in the text are rendered in this translation as `sorry`s.  As an optional project for my measure theory class, students can claim one or of the theorems or exercises to complete their proofs as pull requests.  Readers who are not in my classes are also welcome to submit such proofs, as long as they are not on the following list of claimed theorems:
-
-- Exercise 1.1.1 (claimed by James Thelen)
-- Exercise 1.1.5 (claimed by Solomon Xu)
-- Exercise 1.1.6 (claimed by Soham Patil)
+Portions of the text that were left as exercises to the reader, as well as many of the proofs in the text are rendered in this translation as `sorry`s.  Readers who are not in my classes are also welcome to submit such proofs.
 
 Some 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.
 
@@ -30,11 +26,11 @@ Some of the material in this text is duplicated in Lean's standard math library
     - Section 1.3.4: Absolute integrability ([Documentation](https://teorth.github.io/analysis/docs/Analysis/MeasureTheory/Section_1_3_4.html)) ([Lean source](https://github.com/teorth/analysis/blob/main/analysis/Analysis/MeasureTheory/Section_1_3_4.lean))
     - Section 1.3.5: Littlewood's three principles ([Documentation](https://teorth.github.io/analysis/docs/Analysis/MeasureTheory/Section_1_3_5.html)) ([Lean source](https://github.com/teorth/analysis/blob/main/analysis/Analysis/MeasureTheory/Section_1_3_5.lean))
   - Section 1.4: Abstract measure spaces
-    - Section 1.4.1: Boolean algebras (Documentation) (Lean source)
-    - Section 1.4.2: $\sigma$-algebras and measurable spaces (Documentation) (Lean source)
-    - Section 1.4.3: Countably additive measures and measure spaces (Documentation) (Lean source)
-    - Section 1.4.4: Measurable functions, and integration on a measure space (Documentation) (Lean source)
-    - Section 1.4.5: The convergence theorems (Documentation) (Lean source)
+    - Section 1.4.1: Boolean algebras ([Documentation](https://teorth.github.io/analysis/docs/Analysis/MeasureTheory/Section_1_4_1.html)) ([Lean source](https://github.com/teorth/analysis/blob/main/analysis/Analysis/MeasureTheory/Section_1_4_1.lean))
+    - Section 1.4.2: $\sigma$-algebras and measurable spaces ([Documentation](https://teorth.github.io/analysis/docs/Analysis/MeasureTheory/Section_1_4_2.html)) ([Lean source](https://github.com/teorth/analysis/blob/main/analysis/Analysis/MeasureTheory/Section_1_4_2.lean))
+    - Section 1.4.3: Countably additive measures and measure spaces ([Documentation](https://teorth.github.io/analysis/docs/Analysis/MeasureTheory/Section_1_4_3.html)) ([Lean source](https://github.com/teorth/analysis/blob/main/analysis/Analysis/MeasureTheory/Section_1_4_3.lean))
+    - Section 1.4.4: Measurable functions, and integration on a measure space ([Documentation](https://teorth.github.io/analysis/docs/Analysis/MeasureTheory/Section_1_4_4.html)) ([Lean source](https://github.com/teorth/analysis/blob/main/analysis/Analysis/MeasureTheory/Section_1_4_4.lean))
+    - Section 1.4.5: The convergence theorems ([Documentation](https://teorth.github.io/analysis/docs/Analysis/MeasureTheory/Section_1_4_5.html)) ([Lean source](https://github.com/teorth/analysis/blob/main/analysis/Analysis/MeasureTheory/Section_1_4_5.lean))
   - Section 1.5: Modes of convergence
     - Introduction: (Documentation) (Lean source)
     - Section 1.5.1: Uniqueness (Documentation) (Lean source)

analysis/Analysis/MeasureTheory/Section_1_2_1.lean

@@ -4022,15 +4022,15 @@ theorem IsElementary.almost_disjoint {d k:ℕ} {E: Set (EuclideanSpace' d)} (hE:
         intro V hV_open hz_V
         by_contra h_empty
         push_neg at h_empty
-        rw [Set.eq_empty_iff_forall_not_mem] at h_empty
+        rw [Set.eq_empty_iff_forall_notMem] at h_empty
         have hV_sub : V ⊆ (B' i).toSet := fun w hw => by
           by_contra h_not_in
           exact h_empty w ⟨hw, h_not_in⟩
         have hz_int_Bi : z ∈ interior (B' i).toSet := by
           rw [mem_interior_iff_mem_nhds]
           exact Filter.mem_of_superset (hV_open.mem_nhds hz_V) hV_sub
         have h_disj := h_almost_disj_last i
-        rw [AlmostDisjoint, Set.eq_empty_iff_forall_not_mem] at h_disj
+        rw [AlmostDisjoint, Set.eq_empty_iff_forall_notMem] at h_disj
         exact h_disj z ⟨hz_int_Bi, hz_int_Blast⟩
       -- Use the helper: finite union of box frontiers has empty interior
       have h_union_empty_int : interior (⋃ i : Fin n, frontier (B' i).toSet) = ∅ :=

analysis/Analysis/MeasureTheory/Section_1_4_1.lean

@@ -0,0 +1,275 @@
+import Mathlib.Order.BooleanAlgebra.Defs
+
+import Analysis.MeasureTheory.Section_1_3_5
+
+/-!
+# Introduction to Measure Theory, Section 1.4.1: Boolean algebras
+
+A companion to (the introduction to) Section 1.4.1 of the book "An introduction to Measure Theory".
+
+-/
+
+/-- Definition 1.4.1 -/
+class ConcreteBooleanAlgebra (X:Type*) where
+  measurable : Set X → Prop
+  empty_mem : measurable (∅ : Set X)
+  compl_mem : ∀ E, measurable E → measurable Eᶜ
+  union_mem : ∀ E F, measurable E → measurable F → measurable (E ∪ F)
+
+instance ConcreteBooleanAlgebra.instLE (X:Type*) : LE (ConcreteBooleanAlgebra X) :=
+  ⟨fun B1 B2 => ∀ E, B1.measurable E → B2.measurable E⟩
+
+instance ConcreteBooleanAlgebra.instPartialOrder (X:Type*) : PartialOrder (ConcreteBooleanAlgebra X) :=
+  {
+    le_refl := sorry
+    le_trans := sorry
+    le_antisymm := sorry
+  }
+
+def ConcreteBooleanAlgebra.measurableSets {X:Type*} (B: ConcreteBooleanAlgebra X) : Set (Set X) :=
+  { E | B.measurable E }
+
+/-- Example 1.4.3 -/
+instance ConcreteBooleanAlgebra.instOrderTop {X:Type*} : OrderTop (ConcreteBooleanAlgebra X) :=
+  {
+    top := {
+      measurable := fun _ => True
+      empty_mem := trivial
+      compl_mem := fun _ _ => trivial
+      union_mem := fun _ _ _ _ => trivial
+    }
+    le_top := sorry
+  }
+
+/-- Example 1.4.3 -/
+instance ConcreteBooleanAlgebra.instOrderBot {X:Type*} : OrderBot (ConcreteBooleanAlgebra X) :=
+  {
+    bot := {
+      measurable := fun E => E = ∅ ∨ E = Set.univ
+      empty_mem := by grind
+      compl_mem := fun E hE => by grind
+      union_mem := fun E F hE hF => by grind
+    }
+    bot_le := sorry
+  }
+
+/-- Exercise 1.4.1 (Elementary algebra) -/
+def EuclideanSpace'.elementary_boolean_algebra (d:ℕ) : ConcreteBooleanAlgebra (EuclideanSpace' d) :=
+  {
+    measurable := fun E => IsElementary E ∨ IsElementary Eᶜ
+    empty_mem := by sorry
+    compl_mem := by sorry
+    union_mem := by sorry
+  }
+
+/-- Example 1.4.4 (Jordan algebra) -/
+def JordanMeasurable.boolean_algebra (d:ℕ) : ConcreteBooleanAlgebra (EuclideanSpace' d) :=
+  {
+    measurable := fun E => JordanMeasurable E ∨ JordanMeasurable Eᶜ
+    empty_mem := by sorry
+    compl_mem := by sorry
+    union_mem := by sorry
+  }
+
+def JordanMeasurable.gt_elementary_boolean_algebra (d:ℕ) :
+  JordanMeasurable.boolean_algebra d ≥ EuclideanSpace'.elementary_boolean_algebra d :=
+  by sorry
+
+/-- Example 1.4.5 (Lebesgue algebra) -/
+def LebesgueMeasurable.boolean_algebra (d:ℕ) : ConcreteBooleanAlgebra (EuclideanSpace' d) :=
+  {
+    measurable := fun E => LebesgueMeasurable E
+    empty_mem := by sorry
+    compl_mem := by sorry
+    union_mem := by sorry
+  }
+
+def LebesgueMeasurable.gt_jordan_boolean_algebra (d:ℕ) :
+  LebesgueMeasurable.boolean_algebra d ≥ JordanMeasurable.boolean_algebra d :=
+  by sorry
+
+/-- Example 1.4.6 (Null algebra) -/
+def IsNull.boolean_algebra (d:ℕ) : ConcreteBooleanAlgebra (EuclideanSpace' d) :=
+  {
+    measurable := fun E => IsNull E ∨ IsNull Eᶜ
+    empty_mem := by sorry
+    compl_mem := by sorry
+    union_mem := by sorry
+  }
+
+def IsNull.lt_lebesgue_boolean_algebra (d:ℕ) :
+  IsNull.boolean_algebra d ≤ LebesgueMeasurable.boolean_algebra d :=
+  by sorry
+
+/-- Exercise 1.4.2 (Restriction) -/
+def ConcreteBooleanAlgebra.restrict {X:Type*} (B: ConcreteBooleanAlgebra X) (A:Set X) : ConcreteBooleanAlgebra A :=
+  {
+    measurable := fun E => ∃ E' : Set X, B.measurable E ∧ E = E' ∩ A
+    empty_mem := by sorry
+    compl_mem := by sorry
+    union_mem := by sorry
+  }
+
+def ConcreteBooleanAlgebra.restrict_iff {X:Type*} {B: ConcreteBooleanAlgebra X} {A:Set X} (h: B.measurable A) (E: Set A) :
+  (B.restrict A).measurable E ↔ B.measurable A :=
+  by sorry
+
+/-- Remark 1.4.2: ConcreteBooleanAlgebras are BooleanAlgebras -/
+def ConcreteBooleanAlgebra.toBooleanAlgebra {X:Type*} (B: ConcreteBooleanAlgebra X) : BooleanAlgebra (B.measurableSets) :=
+{
+   sup := sorry
+   le_sup_left := sorry
+   le_sup_right := sorry
+   sup_le := sorry
+   inf := sorry
+   inf_le_left := sorry
+   inf_le_right := sorry
+   le_inf := sorry
+   le_sup_inf := sorry
+   compl := sorry
+   top := sorry
+   bot := sorry
+   inf_compl_le_bot := sorry
+   top_le_sup_compl := sorry
+   le_top := sorry
+   bot_le := sorry
+}
+
+def IsPartition {I X:Type*} (parts: I → Set X) : Prop := (Set.PairwiseDisjoint Set.univ parts) ∧ (⋃ i, parts i = Set.univ)
+
+/-- Example 1.4.7 (Atomic algebra) -/
+def IsPartition.to_ConcreteBooleanAlgebra {I X: Type*} {atoms: I → Set X} (h_part: IsPartition atoms) : ConcreteBooleanAlgebra X :=
+  {
+    measurable := fun E => ∃ J: Set I, E = ⋃ i ∈ J, atoms i
+    empty_mem := by sorry
+    compl_mem := by sorry
+    union_mem := by sorry
+  }
+
+def IsPartition.discrete (X:Type*) : IsPartition (fun x:X ↦ {x}) := by sorry
+
+def ConcreteBooleanAlgebra.top_atomic (X:Type*) : (IsPartition.discrete X).to_ConcreteBooleanAlgebra = ⊤ := by sorry
+
+def IsPartition.trivial (X:Type*) : IsPartition (fun (x:Unit) ↦ (Set.univ: Set X)) := by sorry
+
+def ConcreteBooleanAlgebra.bot_atomic (X:Type*) : (IsPartition.trivial X).to_ConcreteBooleanAlgebra = ⊥ := by sorry
+
+def IsPartition.finer_than {I J X:Type*} {parts_I: I → Set X} {parts_J: J → Set X}
+  (_: IsPartition parts_I) (_: IsPartition parts_J) : Prop :=
+  ∀ i:I, ∃ j:J, parts_I i ⊆ parts_J j
+
+def IsPartition.mono {I J X:Type*} {parts_I: I → Set X} {parts_J: J → Set X}
+  (hI: IsPartition parts_I) (hJ: IsPartition parts_J)
+  (h_finer: hI.finer_than hJ) :
+  hI.to_ConcreteBooleanAlgebra ≤ hJ.to_ConcreteBooleanAlgebra :=
+  by sorry
+
+def IsPartition.remove_empty {I X:Type*} {parts: I → Set X} (h_part: IsPartition parts) : IsPartition (fun (i:{i:I // parts i ≠ ∅}) ↦ parts i.val) :=
+  by sorry
+
+def IsPartition.remove_empty_to_ConcreteBooleanAlgebra {I X:Type*} {parts: I → Set X} (h_part: IsPartition parts) :
+  h_part.to_ConcreteBooleanAlgebra =
+  h_part.remove_empty.to_ConcreteBooleanAlgebra :=
+  by sorry
+
+/-- A variant of DyadicCube with Ico intervals -/
+noncomputable def DyadicCube' {d:ℕ} (n:ℤ) (a: Fin d → ℤ) : Box d := { side := fun i ↦ BoundedInterval.Ico (a i/2^n) ((a i + 1)/2^n) }
+
+/-- Example 1.4.8 -/
+def DyadicCube'.partition (d n:ℕ) : IsPartition (fun (a: Fin d → ℤ) ↦ (DyadicCube' n a).toSet) :=
+  by sorry
+
+def DyadicCube'.boolean_algebra (d n:ℕ) : ConcreteBooleanAlgebra (EuclideanSpace' d) :=
+  (DyadicCube'.partition d n).to_ConcreteBooleanAlgebra
+
+def DyadicCube'.boolean_algebra_mono (d:ℕ) {m n:ℕ} (h: m ≤ n) :
+  DyadicCube'.boolean_algebra d m ≤ DyadicCube'.boolean_algebra d n := by sorry
+
+def IsPartition.relabels {I J X:Type*} {parts_I: I → Set X} (_: IsPartition parts_I) {parts_J : J → Set X} (_: IsPartition parts_J) : Prop := ∃ e : I ≃ J, ∀ i:I, parts_I i = parts_J (e i)
+
+/-- Exercise 1.4.3 (Non-empty atoms of an atomic algebra determined up to relabeling) -/
+def IsPartition.boolean_algebra_eq_iff {I J X:Type*} {parts_I: I → Set X} {parts_J: J → Set X}
+  (hI: IsPartition parts_I) (hJ: IsPartition parts_J) : hI.to_ConcreteBooleanAlgebra = hJ.to_ConcreteBooleanAlgebra ↔ hI.remove_empty.relabels hJ.remove_empty := by sorry
+
+def IsPartition.no_empty {I X:Type*} {parts: I → Set X} (_: IsPartition parts) : Prop := ∀ i:I, parts i ≠ ∅
+
+def IsPartition.boolean_algebra_eq_iff' {I J X:Type*} {parts_I: I → Set X} {parts_J: J → Set X}
+  (hI: IsPartition parts_I) (hJ: IsPartition parts_J) (hIn: hI.no_empty) (hJn: hJ.no_empty) : hI.to_ConcreteBooleanAlgebra = hJ.to_ConcreteBooleanAlgebra ↔ hI.relabels hJ := by sorry
+
+def ConcreteBooleanAlgebra.isAtomic {X:Type*} (B: ConcreteBooleanAlgebra X) : Prop :=
+  ∃ (I:Type*) (parts: I → Set X) (hI:IsPartition parts), B = hI.to_ConcreteBooleanAlgebra
+
+/-- Exercise 1.4.4 (Finite boolean algebras are atomic) -/
+def ConcreteBooleanAlgebra.atomic_of_finite {X:Type*} (B: ConcreteBooleanAlgebra X) (h_fin: (B.measurableSets).Finite) : B.isAtomic :=
+  by sorry
+
+def ConcreteBooleanAlgebra.card_of_finite {X:Type*} (B: ConcreteBooleanAlgebra X) (h_fin: (B.measurableSets).Finite) : ∃ n:ℕ, (B.measurableSets).ncard = 2^n := by sorry
+
+/-- Exercise 1.4.5 (elementary algebra not atomic) -/
+def EuclideanSpace'.elementary_boolean_algebra_not_atomic (d:ℕ) (hd: d ≥ 1) : ¬ (EuclideanSpace'.elementary_boolean_algebra d).isAtomic :=
+  by sorry
+
+/-- Exercise 1.4.5 (Jordan algebra not atomic) -/
+def JordanMeasurable.boolean_algebra_not_atomic (d:ℕ) (hd: d ≥ 1) : ¬ (JordanMeasurable.boolean_algebra d).isAtomic :=
+  by sorry
+
+/-- Exercise 1.4.5 (Lebesgue algebra not atomic) -/
+def LebesgueMeasurable.boolean_algebra_not_atomic (d:ℕ) (hd: d ≥ 1) : ¬ (LebesgueMeasurable.boolean_algebra d).isAtomic :=
+  by sorry
+
+/-- Exercise 1.4.6 (Null algebra not atomic) -/
+def IsNull.boolean_algebra_not_atomic (d:ℕ) (hd: d ≥ 1) : ¬ (IsNull.boolean_algebra d).isAtomic :=
+  by sorry
+
+/-- Exercise 1.4.6 (Intersection of algebras) -/
+instance ConcreteBooleanAlgebra.instInfSet {X:Type*} : InfSet (ConcreteBooleanAlgebra X) :=
+  {
+      sInf S :=
+        {
+          measurable := fun E => ∀ B ∈ S, B.measurable E
+          empty_mem := by sorry
+          compl_mem := by sorry
+          union_mem := by sorry
+        }
+  }
+
+def ConcreteBooleanAlgebra.generated_by {X:Type*} (F: Set (Set X)) : ConcreteBooleanAlgebra X :=
+  sInf { B | ∀ E ∈ F, B.measurable E }
+
+/-- Definition 1.4.10 (Generation of algebras) -/
+instance ConcreteBooleanAlgebra.instSupSet {X:Type*} : SupSet (ConcreteBooleanAlgebra X) :=
+  {
+      sSup S := ConcreteBooleanAlgebra.generated_by (⋃ B ∈ S, B.measurableSets)
+  }
+
+instance ConcreteBooleanAlgebra.instCompleteLattice {X:Type*} : CompleteLattice (ConcreteBooleanAlgebra X) :=
+  {
+    sup := sorry
+    le_sup_left := sorry
+    le_sup_right := sorry
+    sup_le := sorry
+    inf := sorry
+    inf_le_left := sorry
+    inf_le_right := sorry
+    le_inf := sorry
+    le_top := sorry
+    bot_le := sorry
+    le_sSup := sorry
+    sSup_le := sorry
+    sInf_le := sorry
+    le_sInf := sorry
+  }
+
+/-- Example 1.4.11 -/
+instance ConcreteBooleanAlgebra.eq_generated_by_iff {X:Type*} (F: Set (Set X)) : ∃ (B : ConcreteBooleanAlgebra X), B.measurableSets = F ↔ (ConcreteBooleanAlgebra.generated_by F).measurableSets = F := by sorry
+
+/-- Exercise 1.4.7 (Generation by boxes) -/
+instance EuclideanSpace'.elementary_boolean_algebra_generated_by_boxes (d:ℕ) : EuclideanSpace'.elementary_boolean_algebra d =
+  ConcreteBooleanAlgebra.generated_by (Box.toSet '' Set.univ) := by sorry
+
+/-- Exercise 1.4.9 (Recursive definition of generated Boolean algebra)-/
+def ConcreteBooleanAlgebra.generated_by_eq {X:Type*} (F: Set (Set X)) :
+  (ConcreteBooleanAlgebra.generated_by F).measurableSets =
+  ⋃ n, Nat.rec (motive := fun _ ↦ Set (Set X)) F (fun n G ↦ { E: Set X | (∃ S: Finset G, E = ⋃ (H:S), H) ∨ (∃ S: Finset G, E = (⋃ (H:S), H))ᶜ }) n := by sorry
+
+

analysis/Analysis/MeasureTheory/Section_1_4_2.lean

@@ -0,0 +1,7 @@
+import Analysis.MeasureTheory.Section_1_4_1
+/-!
+# Introduction to Measure Theory, Section 1.4.2: $\sigma$-algebras and measurable spaces
+
+A companion to (the introduction to) Section 1.4.2 of the book "An introduction to Measure Theory".
+
+-/

analysis/Analysis/MeasureTheory/Section_1_4_3.lean

@@ -0,0 +1,8 @@
+import Analysis.MeasureTheory.Section_1_4_2
+
+/-!
+# Introduction to Measure Theory, Section 1.4.3: Countably additive measures and measure spaces
+
+A companion to (the introduction to) Section 1.4.3 of the book "An introduction to Measure Theory".
+
+-/

analysis/Analysis/MeasureTheory/Section_1_4_4.lean

@@ -0,0 +1,8 @@
+import Analysis.MeasureTheory.Section_1_4_3
+
+/-!
+# Introduction to Measure Theory, Section 1.4.4: Measurable functions, and integration on a measure space
+
+A companion to (the introduction to) Section 1.4.4 of the book "An introduction to Measure Theory".
+
+-/

analysis/Analysis/MeasureTheory/Section_1_4_5.lean

@@ -0,0 +1,8 @@
+import Analysis.MeasureTheory.Section_1_4_4
+
+/-!
+# Introduction to Measure Theory, Section 1.4.5: The convergence theorems
+
+A companion to (the introduction to) Section 1.4.5 of the book "An introduction to Measure Theory".
+
+-/