The nonmeasurability of the Vitali set

Stream: maths

[Ching-Tsun Chou]

As as exercise in Lean, I formalized the definition of the Vitali set and proved that it is not (Lebesgue) measurable:

https://github.com/ctchou/my_lean/blob/main/MyLean/NonMeasurable.lean

I'd appreciate any comments on my code. The proof is basically the one in Wikipedia:

https://en.wikipedia.org/wiki/Vitali_set#Construction_and_proof

I am grateful to all who answered by questions; in particular:

#new members > A question about measure theory
#new members > A question about ENNReal

[Matt Diamond]

This is great! FYI the at clause can take multiple targets (including the goal) when rewriting / simplifying... so for example:

simp only [mem_Icc] at h_x1
simp only [mem_Icc] at h_y1
simp only [mem_Icc]

can be reduced to a single line:

simp only [mem_Icc] at h_x1 h_y1 ⊢

[Ching-Tsun Chou]

Thanks! I didn't know about that syntax. My file has been updated accordingly.

[Matt Diamond]

One other trivial comment: vS_vT_surj isn't strictly necessary, as you can use Quotient.out and Quotient.out_eq to define vRep and vRep_spec

def vRep : vT → { x : ℝ // x ∈ Icc 0 1 } := Quotient.out
lemma vRep_spec : ∀ t : vT, ⟦vRep t⟧ = t := Quotient.out_eq

[Ching-Tsun Chou]

Thanks! I didn't know about Quotient.out. I think I'll keep Classical.choose to make the use of the axiom of choice manifest.

[Floris van Doorn]

Your conclusion, ¬ MeasurableSet vitali_set only means that vitali_set is not Borel measurable, right? You would need ¬ NullMeasurableSet vitali_set to state that it's not Lebesgue measurable.

[Floris van Doorn]

Note: we would usually spell vitali_set as vitaliSet.

[Ching-Tsun Chou]

Thanks for pointing out this distinction which I was not aware of. I've modified the comment to reflect your comment. I've also changed vitali_{set, union} to Vitali{Set,Union} in the code.

I need to look into how to prove ¬ NullMeasurableSet vitaliSet. In principle, the proof depends only on the monotonicity, translation invariance, and countable additivity of the measure. So it should work for Lebesgue measure as well. But whether it is easy to do so given the results currently in Mathlib is of course a different question.

[Ching-Tsun Chou]

Question: The following page states:

https://leanprover-community.github.io/mathlib4_docs/Mathlib/MeasureTheory/Measure/NullMeasurable.html

A set s : Set α is called null measurable (MeasureTheory.NullMeasurableSet) if it satisfies any of the following equivalent conditions:
[...]
there exists a measurable subset t ⊆ s such that t =ᵐ[μ] s (in this case the latter equality means that μ (s \ t) = 0);

Is there a theorem in Mathlib corresponding to the above statement directly? I can't find one.

[Yaël Dillies]

You can get there using docs#MeasureTheory.NullMeasurableSet.exists_measurable_subset_ae_eq for the forward direction and docs#MeasureTheory.NullMeasurableSet.congr + docs#MeasurableSet.nullMeasurableSet for the backward direction

[Ching-Tsun Chou]

Thanks! I was able to prove it:

lemma nullmeasurable_measurable {s : Set ℝ} (h : NullMeasurableSet s volume) :
    ∃ t ⊆ s, MeasurableSet t ∧ volume (s \ t) = 0 := by
  have ⟨t, t_sub_s, t_m, t_eq_s⟩ := NullMeasurableSet.exists_measurable_subset_ae_eq h
  use t, t_sub_s, t_m
  refine ae_le_set.mp ?_
  exact EventuallyEq.le (id (Filter.EventuallyEq.symm t_eq_s))

Lean's apply? mechanism is really helpful.

[Alex Kontorovich]

Nice! This reminds me of the "Division Paradox" of Mycielski and Sierpiński, that if you lose the Axiom of Choice and assume that every set of reals is measurable, then the cardinality of the Vitali set exceeds (!?!) the cardinality of the Reals. There's a nice writeup of Taylor and Wagon in the Monthly from a few years ago: https://stanwagon.com/public/TheDivisionParadoxTaylorWagon.pdf... (Could be fun to formalize that too?)

[Ilmārs Cīrulis]

Hmm, is that id in the last code fragment by @Ching-Tsun Chou what I think it is?
If yes, then it can be removed. :sweat_smile: :sweat_smile: :sweat_smile:

Sometimes automatic hints contain unnecessary id, I believe.

[Ilmārs Cīrulis]

Apologies for interrupting / jumping in, probably unnecessary :sweat_smile:

[Ruben Van de Velde]

No, you're correct. Last line should probably be written as t_eq_s.symm.le

[Ching-Tsun Chou]

Thanks! t_eq_s.symm.le doesn't quite work, but exact t_eq_s.symm.le does.

[Ching-Tsun Chou]

BTW, I think I know how to prove ¬ (NullMeasurableSet vitaliSet volume), from which¬ (MeasurableSet vitaliSet) follows. I'm working on it.

[Ching-Tsun Chou]

I have enhanced the proof to prove ¬ (NullMeasurableSet vitaliSet volume):

https://github.com/ctchou/my_lean/blob/main/MyLean/NonMeasurable.lean

[Ching-Tsun Chou]

Regarding the comment by @Alex Kontorovich above: Is it even possible to reason meaningfully in Lean from an assumption that contradicts the axiom of choice (AC), which is an axiom in Lean? After all, ex falso quodlibet. It does not seem easy to keep track of whether a Lean proof ever uses AC.

[Ruben Van de Velde]

It is easy with #print axioms, but yeah, this doesn't seem like a well-supported path to go down

[Etienne Marion]

In particular because of the fact that the law of excluded middle is proved with AC

[Ching-Tsun Chou]

I just checked: Real.mk depends on Classical.choice. So, to do without AC, a lot of the theories will need to be redone even before one can start talking about measures.

[Kevin Buzzard]

I think that if you want to do mathematics without AC, but if you do want to assume LEM, then Lean+mathlib is a currently a poor choice for a foundational system to do this. We assume LEM everywhere, and LEM is proved via AC, so already AC is basically impossible to extract the moment you're thinking about the real numbers.

[Ching-Tsun Chou]

I updated my proof:

https://github.com/ctchou/my_lean/blob/main/MyLean/NonMeasurable.lean

The previous version was a bit clumsy and did not take full advantage of the results already in mathlib. The new version does a better job.

As far as I am concerned, this is the end of this exercise.

[Michael Rothgang]

I just saw that this in part of the 1000+ theorems list. Could/should this go into the Archive, for example? (Of course, it would have to be polished a bit to make it there.)

[Ching-Tsun Chou]

Sorry, I have not been following the 1000+ theorem discussion closely and I do not know what "Archive" is. Could you give me some pointers?

[Michael Rothgang]

Sorry for being unclear. The mathlib archive is a part of the mathlib repository (namely, the Archive directory). It is suitable for results which don't contribute to general theory, but are nicely polished (and are meant to show mathlib and its tools).

The 1000+ project is pretty new (and a bit experimental). See e.g. this webpage or this zulip thread.

[Ching-Tsun Chou]

Thanks for the explanation! Is there an example PR for Archive that I can follow?

[Seewoo Lee]

I don't have a clear distinction, but I also think that it can go under Counterexamples (prove negation of "all sets are measurable").

[Ching-Tsun Chou]

It seems to me that mathlib4/Counterexamples is more appropriate. I'll ask for write-access to non-master branches and start working on a PR.

[Ching-Tsun Chou]

PR: https://github.com/leanprover-community/mathlib4/pull/20722

[Violeta Hernández]

I've left a bunch of comments. I think there's lots of potential improvement in terms of both style and line count.

[Ching-Tsun Chou]

Thanks! I'll take a look and make the appropriate fixes.

[Ching-Tsun Chou]

I have a general comment: It seems that most of the comments I received stem from the fact that I enumerated the measure theoretic results needed in the proof at the beginning. As I explained in a comment in the code, I did so because I want to make it crystal-clear what measure theoretic results are actually used. The measure theory part of mathlib is huge and contains many advanced results. But the non-measurability of the Vitali set rely on only a small number of the properties of measurability and the volume measure. I think this deserves to be called out. This way even a reader who is not familiar with mathlib's measure theory can understand the proof. I think it is worth something to know exactly which properties of measurability and measure "cause" the Vitali set to be non-measurable.

[Damiano Testa]

It is very unusual to show non-dependencies the way you do in the PR. Can you maybe use assert_not_exists to ensure that certain declarations are not present? That would be more idiomatic.

[Michael Rothgang]

I agree with the other reviewers that re-stating just the results you use is brittle: you don't have a guarantee that only these are used, and somebody else might come and delete them again. However, I think there's a better way to accomplish the same.

I would prove a slightly more general result first: for any measure which is translation-invariant (and whatever particular properties of volume, i.e. the Lebesgue measure, you're using), there is a non-nullmeasurable set (namely the Vitali set). Then, you can apply this to the Lebesgue measure. What do you think?

[Michael Rothgang]

I think focusing on "does this use abstract results" is misleading. Asking "does this use any special properties of the Lebesgue measure" is reasonable to ask - proving a more general theorem is one way to make sure the answer is "only these ones".

[Michael Rothgang]

I checked: as far as I can see, your result should work for all translation-invariant measures on the circle, right?

[Kevin Buzzard]

@Ching-Tsun Chou the point of the Archive and Counterexamples folders is to demonstrate the power of mathlib (see #maths > The nonmeasurability of the Vitali set @ 💬 for example), not to show how few results we can get away with. If your vision of how to present this result is different then maybe the Counterexamples folder is not a good fit for your vision and you would be better off hosting the result in your own repository?

[Ching-Tsun Chou]

I started this proof to learn Lean and to have some fun. I did not originally intend to include my proof in mathlib. Someone suggested above that I add the proof to mathlib, which is why I created the PR. Now it looks like it will take more efforts to pass the PR review process than I want to spend. I think the best thing for me to do is to create a stand-alone repo containing my proof and add it to Reservoir. What do you think?

[Michael Rothgang]

You can also label your PR with the "help-wanted" or "please-adopt" labels, then somebody might come along and finish your PR. If that's something you are comfortable with!

[Michael Rothgang]

I could certainly imagine spending some time polishing it.

[Ching-Tsun Chou]

I added the label "please-adopt". Feel free to work on it. Personally I want to spend my "Lean time" on learning about Lean and formalization in Lean right now.

[Violeta Hernández]

I'll gladly take this over. I think there's a lot of improvements left on the table.

[Michael Rothgang]

@Violeta Hernández I picked some of the lower-hanging fruit - but I'm done for today, so feel free to continue!

[Violeta Hernández]

Question. A null-measurable set is just a measurable set in the completion of a measure space, right? Do the measures on both measure spaces coincide?

[Ching-Tsun Chou]

I'm no expert in measure theory, but I think so.

[Violeta Hernández]

Do we have this result? It should give a much simpler proof of biUnion_volume.

[Ching-Tsun Chou]

I'm not sure that is the source of the complexity of the proof of biUnion_volume. Note that the proof already uses the same measure volume throughout. The "meat" of the proof is to lift the mathlib theorem measure_biUnion from using MeasurableSet to using NullMeasurableSet in its antecedents.

[Violeta Hernández]

Let volume' be the measure in the null-measurable space. Then we already know that the volume' of the countable union of pairwise disjoint null-measurable sets is the sum of the volume's. If volume = volume' then we're immediately done.

[Ching-Tsun Chou]

I'm not sure the following statement is an existing theorem in mathlib:
"the volume' of the countable union of pairwise disjoint null-measurable sets is the sum of the volume'"

[Violeta Hernández]

Said statement is just measure_iUnion on the corresponding measure.

[Ching-Tsun Chou]

measure_iUnion uses MeasurableSet, not NullMeasurableSet, in its statement.

[Ching-Tsun Chou]

The whole point of the lemma biUnion_volume is to replace the former with the latter.

[Ching-Tsun Chou]

Otherwise you can't prove that vitaliSet is not a NullMeasurableSet. You can only prove that it is not a MeasurableSet.

[Violeta Hernández]

The point I'm making is that NullMeasurableSet is just a special case of MeasurableSet, namely, for the completion of the original measure space.

[Ching-Tsun Chou]

I understand that. All I can say is that I could not find in mathlib a version of measure_biUnion that uses NullMeasurableSet instead of MeasurableSet in its statement.

[Ching-Tsun Chou]

Without such a result, I can't prove anything about NullMeasurableSet.

[Etienne Marion]

There is https://leanprover-community.github.io/mathlib4_docs/Mathlib/MeasureTheory/Measure/NullMeasurable.html#MeasureTheory.measure_iUnion%E2%82%80

[Ching-Tsun Chou]

I missed that. It should make the proof of the lemma biUnion_volume much simpler.

[Ching-Tsun Chou]

One thing I struggled with is to choose between iUnion and biUnion in the definitions. I opted for the latter for reasons I can't remember now. That may or may not have been a mistake.

[Violeta Hernández]

I think biUnion is preferred when you're dealing with sets. I find iUnion more comfortable, but that's mostly up to preference as well.

[Violeta Hernández]

(particularly, biUnion is badly behaved if you don't have a complete lattice)

[Violeta Hernández]

Another math question. Do measurable embeddings preserve null-measurable sets?

[Violeta Hernández]

i.e. is there a null-measurable version of docs#MeasurableEmbedding.measurableSet_image ?

[Ching-Tsun Chou]

I don't know enough measure theory to know that. Time to consult a real expert.

[Damiano Testa]

This mathoverflow question seems relevant.

[Violeta Hernández]

I'm asking because I'm interested in seeing if there's a simpler way of proving that null-measurable sets are translation-invariant

[Etienne Marion]

If a measure is translation invariant then translation preserves the measure of any set

[Violeta Hernández]

I think MeasurableEquivs should map null-measurable sets to null-measurable sets. Any null-measurable set s can be bounded by two measurable sets t and u of the same measure. Which means f '' s is bounded by f '' t and f '' u, also with the same measure. So it's null-measurable.

[Violeta Hernández]

This should give a simpler proof of the fact the translation of a Lebesgue measurable set is Lebesgue measurable.

[Yaël Dillies]

Violeta Hernández said:

MeasurableEquivs should map null-measurable sets to null-measurable sets

How so? MeasurableEquiv preserves the σ-algebra, but says nothing about the measures.

[Ching-Tsun Chou]

I think there may be some miscommunication here. I don't think @Violeta Hernández was not asking whether the the volume measure is invariant under translation (it is, without any preconditions, as stated in the lemma shift_volume in my proof). I think Violeta was asking whether there is a simpler proof that a NullMeasurableSet is still a NullMeasurableSet after translation, which is lemma shift_nullmeasurable in my proof, whose proof is not long but not trivial either.

[Violeta Hernández]

Yeah, I'm basically trying to find the appropriate generalization instead, so that shift_volume can be made into a one-liner special case of it.

[Violeta Hernández]

Have some free time again. I'll try to prove the MeasurableEquiv result I mention and PR it (if it's even true as I expect!)

[Violeta Hernández]

Stuck on an auxiliary lemma I'm not sure is true. If f : α ≃ᵐ α and s =ᶠ[ae μ] t, does it follow that f '' s =ᶠ[ae μ] f '' t?

[Violeta Hernández]

Oh wait, a MeasurableEquiv doesn't actually have to preserve measures, does it? I'm pretty confused.

[Violeta Hernández]

For context this is what I'm trying to prove

import Mathlib

open MeasureTheory

example {α : Type*} [MeasurableSpace α] {μ : Measure α} (f : α ≃ᵐ α) {s : Set α}
    (hs : NullMeasurableSet s μ) : NullMeasurableSet (f '' s) μ := sorry

This is of course true when f is a translation in ℝⁿ, but I'm trying to generalize it to whatever the appropriate generality is.

[Ching-Tsun Chou]

What is α ≃ᵐ α?

[Etienne Marion]

Writing the image as the preimage of the inverse and using docs#MeasureTheory.NullMeasurable you should get there easily.

[Etienne Marion]

Ching-Tsun Chou said:

What is α ≃ᵐ α?

It is the type of measurable equivalences between α and itself, see docs#MeasurableEquiv

[Ching-Tsun Chou]

I see. Thanks!

[Yaël Dillies]

Etienne, I am pretty sure the theorem is false

[Yaël Dillies]

I don't have time to write a counterexample, but basically find a measure mu and a measurable automorphism f such that mu comp f isn't absolutely continuous wrt mu

[Yaël Dillies]

This has to exist

[Violeta Hernández]

What about the statement "functions that preserve measure preserve null-measurable sets". Is that true? Do we have some nice way of writing that down?

[Yaël Dillies]

Yes, definitely true

[Ching-Tsun Chou]

Even if the theorem is true, I'm not sure how it can be used in the proof. The fact that translation preserves the measure is critical in the proof, because the contradiction in the proof boils down to the fact that there is not an r ∈ ENNReal such that countably infinitely many r's can sum to a finite positive real. If your function f can change the measure, then you can't make this argument. (For example, your f may scale the measure so that the infinite sum converges to a positive real.)

[Violeta Hernández]

I'm just trying to generalize one of the auxiliary lemmas

[Violeta Hernández]

I thought it'd be a much more general result but it seems I was slightly wrong

[Etienne Marion]

Ah my bad I thought NullMeasurable meant preimages of null measurable was null measurable, but it is only for measurable sets.

[Violeta Hernández]

I managed to prove this

import Mathlib

open MeasureTheory Set
variable {α : Type*} [MeasurableSpace α] {μ : Measure α}

theorem nullMeasurableSet_image_of_measure_eq {f : α → α} {s : Set α}
    (hf : MeasurableEmbedding f) (H : ∀ s, μ s = 0 → μ (f '' s) = 0) (hs : NullMeasurableSet s μ) :
    NullMeasurableSet (f '' s) μ := by
  obtain ⟨t, hts, ht, hts'⟩ := hs.exists_measurable_subset_ae_eq
  rw [← union_diff_cancel hts, image_union]
  apply (hf.measurableSet_image' ht).nullMeasurableSet.union (.of_null <| H _ _)
  rwa [← union_ae_eq_right, union_eq_self_of_subset_right hts, ae_eq_comm]

[Violeta Hernández]

I imagine this proof can be golfed down a bit by someone more familiar with the API.

[Violeta Hernández]

I have a few questions:

• Is there some other "more canonical" way to write down condition H?
• Can this be made into an iff?
• Does this work with the preimage too? (I don't think so, but just checking)

[Violeta Hernández]

(Also, a better name for this theorem would be nice)

[Ching-Tsun Chou]

Nitpick: The variable s is not declared in the theorem.

[Violeta Hernández]

whoops, fixed my mwe