feat(Counterexamples): the Vitali set is non-measurable by ctchou · Pull Request #20722 · leanprover-community/mathlib4

ctchou · 2025-01-14T00:35:46Z

github-actions · 2025-01-14T00:36:39Z

PR summary c0ec16697f

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.MeasureTheory.Measure.NullMeasurable	1343	1344	+1 (+0.07%)

Import changes for all files

Files	Import difference
`Mathlib.MeasureTheory.Measure.MeasureSpace` `Mathlib.MeasureTheory.Measure.NullMeasurable`	1

Declarations diff

+ Icc_subset_vitaliUnion
+ biUnion_volume
+ measure_union_null
+ not_measurableSet_vitaliSet
+ not_nullMeasurableSet_vitaliSet
+ nullMeasurableSet_image_of_measure_eq
+ nullmeasurable_measurable_null
+ shift_nullmeasurable
+ symmDiff
+ vI_infinite
+ vitaliSet
+ vitaliSet_subset_Icc
+ vitaliSetoid
+ vitaliShift
+ vitaliType
+ vitaliUnion
+ vitaliUnion_subset_Icc
+ vitali_pairwise_disjoint
+ volume_vitaliShift
+ volume_vitaliUnion
+ volume_vitaliUnion_mem

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

grunweg

Thanks for your pull request, and welcome to mathlib! I took a first look at your PR.
There are a number of places where your code can be written more compactly (i.e., doing the same thing, but being shorter). Such is completely normal for a first pull request. I have left some comments to get you started.

A number of comments occur several times: when addressing it once, please try to go over the file and fix all instances of it. If you're unsure, feel free to ask here (or on zulip)!

grunweg · 2025-01-14T13:37:39Z

Counterexamples/VitaliSetNotMeasurable.lean

+/-- We first derive the measure theoretic results that we need from
+the more general theorems in Mathlib. -/
+
+example {a b : ℝ} : volume (Icc a b) = ENNReal.ofReal (b - a) :=


Do you need this result in the final file? (It's fine if this was helpful during development, but we'd like to merge a polished version into mathlib.) In other words: I think it's better to simply delete this.

I prefer to enumerate explicitly all the measure theoretic results that are involved, because I want to make clear exactly which properties of measurability and the volume measure are used in the proof. I have updated the comment to make this point.

Maybe this characterization can be part of the module docs instead? Listing results like this is quite nonconventional.

grunweg · 2025-01-14T13:38:47Z

Counterexamples/VitaliSetNotMeasurable.lean

+example {a b : ℝ} : volume (Icc a b) = ENNReal.ofReal (b - a) :=
+  volume_Icc
+
+lemma volume_mono {s t : Set ℝ} (h : s ⊆ t) : volume s ≤ volume t := by


You can probably "inline" this lemma (i.e., replace every time you want to you volume_mono h by OuterMeasureclass.measure_mono volume h). Can you do so, please?

See my reply above.

grunweg · 2025-01-14T13:39:02Z

Counterexamples/VitaliSetNotMeasurable.lean

+lemma volume_mono {s t : Set ℝ} (h : s ⊆ t) : volume s ≤ volume t := by
+  exact OuterMeasureClass.measure_mono volume h
+
+lemma measurable_nullmeasurable {s : Set ℝ} (h : MeasurableSet s) : NullMeasurableSet s volume :=


A similar comment applies here. (Using dot notation, you can even write h.nullMeasurableSet.)

See my reply above. I did change to the dot-notation.

grunweg · 2025-01-14T13:39:08Z

Counterexamples/VitaliSetNotMeasurable.lean

+lemma measurable_nullmeasurable {s : Set ℝ} (h : MeasurableSet s) : NullMeasurableSet s volume :=
+  MeasurableSet.nullMeasurableSet h
+
+lemma measurable_null_nullmeasurable {s t : Set ℝ}


Also inline this one, please.

See my reply above.

Counterexamples/VitaliSetNotMeasurable.lean

ctchou · 2025-01-14T23:37:03Z

Question: as I update the PR, should I collapse my successive commits into a single commit, or keep them separate? I'm keeping them separate for now, but I can also collapse them if that's the convention.

grunweg · 2025-01-15T10:32:10Z

Indeed, different repositories have different conventions on this question. Adding separate comments is exactly right. When merging this pull request at the end, all commits are squashed into one (and the PR description is used to determine the final commit message).

ctchou · 2025-01-15T23:34:21Z

Thanks for replying. I've replied above why I don't want to make certain changes and asked for clarification on some other issues. What's the next step?

vihdzp · 2025-01-19T22:11:09Z

Counterexamples/VitaliSetNotMeasurable.lean

+/-- We first derive the measure theoretic results that we need from
+the more general theorems in Mathlib. -/
+
+example {a b : ℝ} : volume (Icc a b) = ENNReal.ofReal (b - a) :=


Maybe this characterization can be part of the module docs instead? Listing results like this is quite nonconventional.

vihdzp · 2025-01-19T22:13:53Z

Counterexamples/VitaliSetNotMeasurable.lean

+    (hm : NullMeasurableSet s) (hn : volume t = 0) : NullMeasurableSet (s ∪ t) :=
+  NullMeasurableSet.union_null hm hn
+
+lemma nullmeasurable_measurable_null {s : Set ℝ} (h : NullMeasurableSet s volume) :


I don't think this result is needed, since t is just the set given by exists_measurable_subset_ae_eq and the conclusions follow from the (I imagine more useful) t =ᵐ[μ] s predicate.

Sorry, does your comment apply to the lemma measurable_null_nullmeasurable or the lemma nullmeasurable_measurable_null?

It applies to the latter, though I do agree with the other reviewer that the former shouldn't be duplicated here.

vihdzp · 2025-01-19T22:16:34Z

Counterexamples/VitaliSetNotMeasurable.lean

+  · exact measure_congr t_eq_s
+  · exact ae_le_set.mp t_eq_s.symm.le
+
+lemma shift_volume (s : Set ℝ) (c : ℝ) : volume ((fun x ↦ x + c) '' s) = volume s := by


You can write this as

Suggested change

lemma shift_volume (s : Set ℝ) (c : ℝ) : volume ((fun x ↦ x + c) '' s) = volume s := by

lemma shift_volume (s : Set ℝ) (c : ℝ) : volume ((· + c) '' s) = volume s := by

Still, I don't think we need to have this theorem. It can just be inlined, or even replaced by a simp call.

Counterexamples/VitaliSetNotMeasurable.lean

vihdzp · 2025-01-19T22:39:43Z

Counterexamples/VitaliSetNotMeasurable.lean

+  rw [vitaliSet', shift_volume]
+
+/-- vI is an infinite set. -/
+lemma vI_infinite : vI.Infinite := by


This should follow more easily from Set.Icc_infinite.

Counterexamples/VitaliSetNotMeasurable.lean

vihdzp · 2025-01-19T22:41:52Z

Counterexamples/VitaliSetNotMeasurable.lean

+/-- The following theorems are the main results.
+
+vitaliSet is not null-measurable. -/
+theorem vitaliSet_not_nullmeasurable : ¬ (NullMeasurableSet vitaliSet volume) := by


I think you can prove (and add to Mathlib) an auxiliary theorem for this: a sum Σ i : I, x for an infinite type I is either 0 or ⊤.

Counterexamples/VitaliSetNotMeasurable.lean

vihdzp · 2025-01-20T07:35:56Z

I think it's going to be really hard to convince the reviewers to have 30-odd extra lines of code listing specific dependencies of your proof. First of all, you're not even making the formal guarantee that these are sufficient conditions for the theorem to hold (and if you did, you'd likely end up with a much uglier and unwieldy statement). And second, there's no guarantee someone else couldn't come to this file later on and add or switch out these dependencies.

The archive is meant as a showcase of good proofs, which doesn't always overlap with a good mathematical presentation. I really don't think we need to go over the basics of measure theory here.

grunweg

I left a few more comments about how this can be written more concisely.

Counterexamples/VitaliSetNotMeasurable.lean

grunweg · 2025-01-20T10:51:50Z

Counterexamples/VitaliSetNotMeasurable.lean

+    (hs : I.Countable) : volume (⋃ i ∈ I, f i) = 0 ↔ ∀ i ∈ I, volume (f i) = 0 :=
+  measure_biUnion_null_iff hs
+
+lemma biUnion_volume {ι : Type*} {I : Set ι} {s : ι → Set ℝ}


Every measure is countable additive - this result should be in mathlib, right? (If not, can you please add it there?)

I think the distinction here is that the sets are null-measurable rather than just measurable. I'm not a measure theory expert, but the (outer) measures on both the initial space and its completion coincide, right? If so, then this result should be an easy consequence of that.

I would be very interested if you can find a simpler proof. I was not able to.

But I suspect the intermediate result:
have h_st : ⋃ i ∈ I, s i = (⋃ i ∈ I, t i) ∪ (⋃ i ∈ I, (s i \ t i))
should have a simpler proof than the monstrosity I produced.

Counterexamples/VitaliSetNotMeasurable.lean

vihdzp · 2025-01-20T16:40:35Z

Counterexamples/VitaliSetNotMeasurable.lean

+    (hs : I.Countable) : volume (⋃ i ∈ I, f i) = 0 ↔ ∀ i ∈ I, volume (f i) = 0 :=
+  measure_biUnion_null_iff hs
+
+lemma biUnion_volume {ι : Type*} {I : Set ι} {s : ι → Set ℝ}


I think the distinction here is that the sets are null-measurable rather than just measurable. I'm not a measure theory expert, but the (outer) measures on both the initial space and its completion coincide, right? If so, then this result should be an easy consequence of that.

Counterexamples/VitaliSetNotMeasurable.lean

ctchou · 2025-01-22T21:40:38Z

I added the label "please-adopt" to this PR. Please feel free to make modifications needed for inclusion in mathlib. Thanks!

Zulip thread: https://leanprover.zulipchat.com/#narrow/channel/116395-maths/topic/The.20nonmeasurability.20of.20the.20Vitali.20set

…ments

ctchou · 2025-01-22T21:50:59Z

@vihdzp: In the first version of this proof, I proved only that ¬ (MeasurableSet vitaliSet). Then Floris van Doorn pointed out that. MeasurableSet means Borel measurability and I need to prove ¬ (NullMeasurableSet vitaliSet volume) for Lebesgue measurability, which is what I did in the version here.

https://leanprover.zulipchat.com/#narrow/channel/116395-maths/topic/The.20nonmeasurability.20of.20the.20Vitali.20set/near/489212000

ctchou · 2025-01-22T21:59:02Z

Practically speaking, a set is a NullMeasurableSet if it differs from a MeasurableSet by a set of measure zero, which is spelled out in the lemma nullmeasurable_measurable_null. (Of course, my lemma is not the only way to state this fact.) Most of the nontrivial measure theoretic lemmas in my proof basically use this fact to lift results about MeasurableSet to being about NullMeasurableSet.

vihdzp · 2025-01-23T01:42:48Z

I'll adopt this PR. I'll leave it as a draft until I've done all the changes I think are appropriate (hopefully in the next few days).

mathlib4-merge-conflict-bot · 2025-08-16T07:28:12Z

This pull request has conflicts, please merge master and resolve them.

vihdzp · 2025-08-16T11:36:19Z

Oh darn, I kind of forgot about this. I'm really busy with other Lean stuff, but I'll see if I can come back to this during the week.

github-actions bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Jan 14, 2025

grunweg changed the title ~~feat: Add Counterexamples/VitaliSetNotMeasurable.lean~~ feat(Counterexamples): the Vitali set is non-measurable Jan 14, 2025

grunweg added the t-measure-probability Measure theory / Probability theory label Jan 14, 2025

grunweg reviewed Jan 14, 2025

View reviewed changes

grunweg added the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 14, 2025

vihdzp reviewed Jan 19, 2025

View reviewed changes

grunweg reviewed Jan 20, 2025

View reviewed changes

vihdzp reviewed Jan 20, 2025

View reviewed changes

ctchou added the please-adopt Inactive PR (would be valuable to adopt) label Jan 22, 2025

ctchou added 2 commits January 22, 2025 22:50

feat: Add Counterexamples/VitaliSetNotMeasurable.lean

b49b094

Update Counterexamples/VitaliSetNotMeasurable.lean per @grunweg's com…

c6eeb1d

…ments

chore: update 1000.yaml

07fffd5

Some local golfs.

450a2be

grunweg force-pushed the ctchou/vitali-set branch from 4e77cfd to 450a2be Compare January 22, 2025 22:06

grunweg added 3 commits January 22, 2025 23:16

Generalise one lemma; inline two standard results.

6e44450

One more

99822dd

Some more review comments

798dbde

vihdzp self-assigned this Jan 23, 2025

vihdzp marked this pull request as draft January 23, 2025 01:42

vihdzp added 2 commits January 22, 2025 19:45

inline shift_volume

59d4942

golf + reprove

2fc80bb

vihdzp added 4 commits January 23, 2025 00:56

progress

db90cd6

Merge branch 'master' into ctchou/vitali-set

40f65ee

add lemma

3d15f17

oops

c0ec166

grunweg mentioned this pull request Apr 13, 2025

feat(Counterexamples): a non-negative function, not a.e. zero, with vanishing lowe… #24010

Open

1 task

mathlib4-merge-conflict-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Aug 16, 2025

	lemma shift_volume (s : Set ℝ) (c : ℝ) : volume ((fun x ↦ x + c) '' s) = volume s := by
	lemma shift_volume (s : Set ℝ) (c : ℝ) : volume ((· + c) '' s) = volume s := by

Conversation

ctchou commented Jan 14, 2025

Uh oh!

github-actions bot commented Jan 14, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary c0ec16697f

Import changes for modified files

Declarations diff

Uh oh!

grunweg left a comment

Choose a reason for hiding this comment

Uh oh!

grunweg Jan 14, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

ctchou commented Jan 14, 2025

Uh oh!

grunweg commented Jan 15, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

ctchou commented Jan 15, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

vihdzp commented Jan 20, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

grunweg left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

ctchou Jan 22, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

github-actions bot commented Jan 14, 2025 •

edited

Loading

grunweg Jan 14, 2025 •

edited

Loading

grunweg commented Jan 15, 2025 •

edited

Loading

ctchou commented Jan 15, 2025 •

edited

Loading

vihdzp commented Jan 20, 2025 •

edited

Loading

ctchou Jan 22, 2025 •

edited

Loading

ctchou commented Jan 22, 2025 •

edited

Loading

vihdzp commented Jan 23, 2025 •

edited

Loading