From 4ab8697ea3a6ca2e62bb9b9ea68085437906d5ab Mon Sep 17 00:00:00 2001
From: Taksh <takshkothari09@gmail.com>
Date: Tue, 1 Sep 2026 22:33:41 +0530
Subject: [PATCH 1/3] fix: require boundedness for Lebesgue=Jordan-inner
 equalities
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Jordan_inner_measure is ℝ-valued via sSup, so unbounded sets get a junk
value; Lebesgue_outer_measure is EReal and can be ⊤.
---
 Analysis/MeasureTheory/Section_1_2_1.lean | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/Analysis/MeasureTheory/Section_1_2_1.lean b/Analysis/MeasureTheory/Section_1_2_1.lean
index 2ed00d71b..3c9e524f6 100644
--- a/Analysis/MeasureTheory/Section_1_2_1.lean
+++ b/Analysis/MeasureTheory/Section_1_2_1.lean
@@ -4340,7 +4340,8 @@ theorem Box.sum_volume_eq {d:ℕ} (B B': ℕ → Box d) (hdisj: Pairwise (Functi
 /-- Exercise 1.2.5: For any set that equals a countable union of almost disjoint boxes,
     the Lebesgue outer measure equals the Jordan inner measure. -/
 theorem Lebesgue_outer_measure.eq_Jordan_inner_of_boxes {d:ℕ} (E: Set (EuclideanSpace' d)) (B: ℕ → Box d)
-    (hE: E = ⋃ n, (B n).toSet) (hdisj: Pairwise (Function.onFun AlmostDisjoint B)) :
+    (hE: E = ⋃ n, (B n).toSet) (hdisj: Pairwise (Function.onFun AlmostDisjoint B))
+    (hbound : Bornology.IsBounded E) :
     Lebesgue_outer_measure E = Jordan_inner_measure E := by
   sorry
 
@@ -5121,7 +5122,8 @@ theorem IsOpen.eq_union_boxes {d:ℕ} (hd : 0 < d) (E: Set (EuclideanSpace' d))
         have h_scale_lt : (↑(B_idx j).1 : ℤ) < ↑(B_idx i).1 := by exact_mod_cast hij_gt
         exact dyadicCubeLargerNotInSmaller hd h_scale_lt h_ji
 
-theorem Lebesgue_outer_measure.of_open {d:ℕ} (E: Set (EuclideanSpace' d)) (hE: IsOpen E) : Lebesgue_outer_measure E = Jordan_inner_measure E := by
+theorem Lebesgue_outer_measure.of_open {d:ℕ} (E: Set (EuclideanSpace' d)) (hE: IsOpen E)
+    (hbound : Bornology.IsBounded E) : Lebesgue_outer_measure E = Jordan_inner_measure E := by
   by_cases hd : d = 0
   · -- Dimension 0: In dim 0, open sets are either ∅ or Set.univ
     subst hd
@@ -5255,7 +5257,7 @@ theorem Lebesgue_outer_measure.of_open {d:ℕ} (E: Set (EuclideanSpace' d)) (hE:
       -- Decompose E into almost-disjoint dyadic boxes
       obtain ⟨B, hE_eq, hB_dyadic, hB_disj⟩ := IsOpen.eq_union_boxes hd' E hE hE_nonempty
       -- Apply lemma eq_Jordan_inner_of_boxes (Exercise 1.2.5)
-      exact Lebesgue_outer_measure.eq_Jordan_inner_of_boxes E B hE_eq hB_disj
+      exact Lebesgue_outer_measure.eq_Jordan_inner_of_boxes E B hE_eq hB_disj hbound
 
 /-- Lemma 1.2.12 (Outer regularity). m\*(E) = inf\{m\*(U) : E ⊆ U, U open\}. -/
 theorem Lebesgue_outer_measure.eq {d:ℕ} (E: Set (EuclideanSpace' d)) : Lebesgue_outer_measure E = sInf { M | ∃ U, E ⊆ U ∧ IsOpen U ∧ M = Lebesgue_outer_measure U} := by

From 04817100a3a7e0896ea6a79e9d106be0e13a28cd Mon Sep 17 00:00:00 2001
From: Taksh <takshkothari09@gmail.com>
Date: Tue, 1 Sep 2026 22:36:46 +0530
Subject: [PATCH 2/3] Fill Exercise 3.5.5: product does not distribute over
 union or difference.

---
 Analysis/Section_3_5.lean | 66 ++++++++++++++++++++++++++++++++++++---
 1 file changed, 62 insertions(+), 4 deletions(-)

diff --git a/Analysis/Section_3_5.lean b/Analysis/Section_3_5.lean
index bbadf63aa..3d3c6182a 100644
--- a/Analysis/Section_3_5.lean
+++ b/Analysis/Section_3_5.lean
@@ -442,14 +442,72 @@ theorem SetTheory.Set.inter_of_prod (A B C D:Set) :
 /-- Exercise 3.5.5 (b) -/
 def SetTheory.Set.union_of_prod :
   Decidable (∀ (A B C D:Set), (A ×ˢ B) ∪ (C ×ˢ D) = (A ∪ C) ×ˢ (B ∪ D)) := by
-  -- the first line of this construction should be `apply isTrue` or `apply isFalse`.
-  sorry
+  -- Diagonal vs rectangle: LHS has 2 pairs, RHS has 4.
+  apply isFalse
+  intro h
+  let A : Set := {0}
+  let B : Set := {0}
+  let C : Set := {1}
+  let D : Set := {1}
+  have hf := h A B C D
+  let z : Object := (⟨(0:Object), (1:Object)⟩ : OrderedPair)
+  have hr : z ∈ (A ∪ C) ×ˢ (B ∪ D) := by
+    rw [mem_cartesian]
+    refine ⟨⟨(0:Object), ?_⟩, ⟨(1:Object), ?_⟩, rfl⟩
+    · simp [A, C, mem_union, mem_singleton]
+    · simp [B, D, mem_union, mem_singleton]
+  have hl : z ∉ (A ×ˢ B) ∪ (C ×ˢ D) := by
+    intro hin
+    have pair_eq {x y : Object} (hz : z = (⟨x, y⟩ : OrderedPair)) : x = 0 ∧ y = 1 := by
+      have := OrderedPair.toObject.injective (by
+        change OrderedPair.toObject ⟨0, 1⟩ = OrderedPair.toObject ⟨x, y⟩
+        simpa [z] using hz)
+      simpa [OrderedPair.eq] using this
+    cases (mem_union _ _ _).mp hin with
+    | inl hinAB =>
+      obtain ⟨x, y, hz⟩ := (mem_cartesian _ _ _).mp hinAB
+      have hy0 : y.val = (0:Object) := by simpa [B, mem_singleton] using y.property
+      have hy1 : y.val = (1:Object) := (pair_eq hz).2
+      exact Nat.zero_ne_one ((ofNat_inj' 0 1).mp (hy0.symm.trans hy1))
+    | inr hinCD =>
+      obtain ⟨x, y, hz⟩ := (mem_cartesian _ _ _).mp hinCD
+      have hx1 : x.val = (1:Object) := by simpa [C, mem_singleton] using x.property
+      have hx0 : x.val = (0:Object) := (pair_eq hz).1
+      exact Nat.zero_ne_one ((ofNat_inj' 0 1).mp (hx0.trans hx1))
+  exact hl (by rwa [← hf] at hr)
 
 /-- Exercise 3.5.5 (c) -/
 def SetTheory.Set.diff_of_prod :
   Decidable (∀ (A B C D:Set), (A ×ˢ B) \ (C ×ˢ D) = (A \ C) ×ˢ (B \ D)) := by
-  -- the first line of this construction should be `apply isTrue` or `apply isFalse`.
-  sorry
+  -- (0,0) survives on the left but the right-hand product is empty.
+  apply isFalse
+  intro h
+  let A : Set := {0}
+  let B : Set := {0}
+  let C : Set := {0}
+  let D : Set := {1}
+  have hf := h A B C D
+  let z : Object := (⟨(0:Object), (0:Object)⟩ : OrderedPair)
+  have hl : z ∈ (A ×ˢ B) \ (C ×ˢ D) := by
+    refine (mem_sdiff _ _ _).mpr ⟨?_, ?_⟩
+    · rw [mem_cartesian]
+      refine ⟨⟨(0:Object), by simp [A, mem_singleton]⟩,
+        ⟨(0:Object), by simp [B, mem_singleton]⟩, rfl⟩
+    · intro hin
+      obtain ⟨x, y, hz⟩ := (mem_cartesian _ _ _).mp hin
+      have hy : y.val = (1:Object) := by simpa [D, mem_singleton] using y.property
+      have hy0 : y.val = (0:Object) := by
+        have := OrderedPair.toObject.injective (by
+          change OrderedPair.toObject ⟨0, 0⟩ = OrderedPair.toObject ⟨x.val, y.val⟩
+          simpa [z] using hz)
+        exact ((OrderedPair.eq _ _ _ _).mp this).2
+      exact Nat.zero_ne_one ((ofNat_inj' 0 1).mp (hy0.symm.trans hy))
+  have hr : z ∉ (A \ C) ×ˢ (B \ D) := by
+    intro hin
+    obtain ⟨x, _y, _hz⟩ := (mem_cartesian _ _ _).mp hin
+    have hx := (mem_sdiff _ _ _).mp x.property
+    exact hx.2 ((mem_singleton _ _).mpr ((mem_singleton _ _).mp hx.1))
+  exact hr (hf ▸ hl)
 
 /--
   Exercise 3.5.6.

From cfab6d1a4f67c4bcb8ef65624d6208ff5209927f Mon Sep 17 00:00:00 2001
From: Taksh <takshkothari09@gmail.com>
Date: Tue, 1 Sep 2026 22:37:28 +0530
Subject: [PATCH 3/3] Revert "Fill Exercise 3.5.5: product does not distribute
 over union or difference."

This reverts commit 04817100a3a7e0896ea6a79e9d106be0e13a28cd.
---
 Analysis/Section_3_5.lean | 66 +++------------------------------------
 1 file changed, 4 insertions(+), 62 deletions(-)

diff --git a/Analysis/Section_3_5.lean b/Analysis/Section_3_5.lean
index 3d3c6182a..bbadf63aa 100644
--- a/Analysis/Section_3_5.lean
+++ b/Analysis/Section_3_5.lean
@@ -442,72 +442,14 @@ theorem SetTheory.Set.inter_of_prod (A B C D:Set) :
 /-- Exercise 3.5.5 (b) -/
 def SetTheory.Set.union_of_prod :
   Decidable (∀ (A B C D:Set), (A ×ˢ B) ∪ (C ×ˢ D) = (A ∪ C) ×ˢ (B ∪ D)) := by
-  -- Diagonal vs rectangle: LHS has 2 pairs, RHS has 4.
-  apply isFalse
-  intro h
-  let A : Set := {0}
-  let B : Set := {0}
-  let C : Set := {1}
-  let D : Set := {1}
-  have hf := h A B C D
-  let z : Object := (⟨(0:Object), (1:Object)⟩ : OrderedPair)
-  have hr : z ∈ (A ∪ C) ×ˢ (B ∪ D) := by
-    rw [mem_cartesian]
-    refine ⟨⟨(0:Object), ?_⟩, ⟨(1:Object), ?_⟩, rfl⟩
-    · simp [A, C, mem_union, mem_singleton]
-    · simp [B, D, mem_union, mem_singleton]
-  have hl : z ∉ (A ×ˢ B) ∪ (C ×ˢ D) := by
-    intro hin
-    have pair_eq {x y : Object} (hz : z = (⟨x, y⟩ : OrderedPair)) : x = 0 ∧ y = 1 := by
-      have := OrderedPair.toObject.injective (by
-        change OrderedPair.toObject ⟨0, 1⟩ = OrderedPair.toObject ⟨x, y⟩
-        simpa [z] using hz)
-      simpa [OrderedPair.eq] using this
-    cases (mem_union _ _ _).mp hin with
-    | inl hinAB =>
-      obtain ⟨x, y, hz⟩ := (mem_cartesian _ _ _).mp hinAB
-      have hy0 : y.val = (0:Object) := by simpa [B, mem_singleton] using y.property
-      have hy1 : y.val = (1:Object) := (pair_eq hz).2
-      exact Nat.zero_ne_one ((ofNat_inj' 0 1).mp (hy0.symm.trans hy1))
-    | inr hinCD =>
-      obtain ⟨x, y, hz⟩ := (mem_cartesian _ _ _).mp hinCD
-      have hx1 : x.val = (1:Object) := by simpa [C, mem_singleton] using x.property
-      have hx0 : x.val = (0:Object) := (pair_eq hz).1
-      exact Nat.zero_ne_one ((ofNat_inj' 0 1).mp (hx0.trans hx1))
-  exact hl (by rwa [← hf] at hr)
+  -- the first line of this construction should be `apply isTrue` or `apply isFalse`.
+  sorry
 
 /-- Exercise 3.5.5 (c) -/
 def SetTheory.Set.diff_of_prod :
   Decidable (∀ (A B C D:Set), (A ×ˢ B) \ (C ×ˢ D) = (A \ C) ×ˢ (B \ D)) := by
-  -- (0,0) survives on the left but the right-hand product is empty.
-  apply isFalse
-  intro h
-  let A : Set := {0}
-  let B : Set := {0}
-  let C : Set := {0}
-  let D : Set := {1}
-  have hf := h A B C D
-  let z : Object := (⟨(0:Object), (0:Object)⟩ : OrderedPair)
-  have hl : z ∈ (A ×ˢ B) \ (C ×ˢ D) := by
-    refine (mem_sdiff _ _ _).mpr ⟨?_, ?_⟩
-    · rw [mem_cartesian]
-      refine ⟨⟨(0:Object), by simp [A, mem_singleton]⟩,
-        ⟨(0:Object), by simp [B, mem_singleton]⟩, rfl⟩
-    · intro hin
-      obtain ⟨x, y, hz⟩ := (mem_cartesian _ _ _).mp hin
-      have hy : y.val = (1:Object) := by simpa [D, mem_singleton] using y.property
-      have hy0 : y.val = (0:Object) := by
-        have := OrderedPair.toObject.injective (by
-          change OrderedPair.toObject ⟨0, 0⟩ = OrderedPair.toObject ⟨x.val, y.val⟩
-          simpa [z] using hz)
-        exact ((OrderedPair.eq _ _ _ _).mp this).2
-      exact Nat.zero_ne_one ((ofNat_inj' 0 1).mp (hy0.symm.trans hy))
-  have hr : z ∉ (A \ C) ×ˢ (B \ D) := by
-    intro hin
-    obtain ⟨x, _y, _hz⟩ := (mem_cartesian _ _ _).mp hin
-    have hx := (mem_sdiff _ _ _).mp x.property
-    exact hx.2 ((mem_singleton _ _).mpr ((mem_singleton _ _).mp hx.1))
-  exact hr (hf ▸ hl)
+  -- the first line of this construction should be `apply isTrue` or `apply isFalse`.
+  sorry
 
 /--
   Exercise 3.5.6.