Skip to content

fix: require boundedness for Lebesgue=Jordan-inner equalities #679

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
Chessing234 wants to merge 3 commits into from
Closed

fix: require boundedness for Lebesgue=Jordan-inner equalities #679

Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
4ab8697
fix: require boundedness for Lebesgue=Jordan-inner equalities
Chessing234 Sep 1, 2026
0481710
Fill Exercise 3.5.5: product does not distribute over union or differ…
Chessing234 Sep 1, 2026
cfab6d1
Revert "Fill Exercise 3.5.5: product does not distribute over union o…
Chessing234 Sep 1, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 5 additions & 3 deletions Analysis/MeasureTheory/Section_1_2_1.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
Loading