Prove: Vitali set in not measurable

Stream: new members

[Marvin Sigg]

I'm in a course about Lean 4, but had no previous experience. Up to now, I worked halfway through the Mathematics in Lean book from the Leanprover community.

My assignment is to formalise the proof that the Vitali set is not Lebesgue measurable, as can be found in https://en.wikipedia.org/wiki/Vitali_set#Construction_and_proof . I can use Mathlib up to a "reasonable extent", but I don't really know how to properly start. My idea is to construct the Vitali set via def using an instance of an equivalence relation, and then show that both assigning zero or a positive number to the set leads to a contradiction (by_contra). Currently I am at a loss as to how concretely formalise the equivalence relation, the set, and the Lebesgue measure. Can someone point me towards relevant Mathlib objects or references without giving the answer completely away?

[Kevin Buzzard]

Is your course lecturer ok about you asking this kind of question?

Concretely formalising the equivalence relation shouldn't be too hard. What did you try?

[Etienne Marion]

Just mentioning that this has already been done with Mathlib, there is an open PR about it.

[Marvin Sigg]

Thank you both for your quick responses. Yes, the lecturer pointed us specifically to this forum.

@Etienne Marion, I have found the version by Ching-Tsun Chou, thanks for pointing it out. My intention is of course to come up with my own version, and to need as little "inspiration" as possible. @Kevin Buzzard thank you for your willingness to help. I will try harder before asking a dozen trivial questions, but will probably soon return back to the board.

[Kevin Buzzard]

#new members is a fine place to ask trivial questions.

[Eric Paul]

(deleted)

[Marvin Sigg]

Kevin Buzzard schrieb:

#new members is a fine place to ask trivial questions.

In that case I'll happily take you up on your offer. At the moment, I'm struggling with the two notions

axiom sigma_additivity {A : ℕ → Set ℝ} : volume (⋃ n, A n) = ∑ n, volume (A n)

and

def equiv {x y : Icc 0 1} : Prop :=
  (x - y) ∈ ℚ

where I just cannot find the correct imports and syntax.
Specifically trouble bring me ∑ n, volume (A n) and (x - y) ∈ ℚ (as well as ℚ ∩ (Icc -1 1)).

Currently I've installed Mathlib.Tactic, Mathlib.Data.Real.Basic, Mathlib.Util.Delaborators, Mathlib.Data.Set.Function, and Mathlib.MeasureTheory.Measure.Lebesgue.Basic. Can someone help me out?

[Yaël Dillies]

Have you tried import Mathlib? (assuming your computer can withstand it)

[Marvin Sigg]

import Mathlibworks, but I think the problem lies more within my lack of knowledge for the correct syntax

[Yaël Dillies]

You will need to write open MeasureTheory at the start of your file most likely

[Yaël Dillies]

I would give you more detailed instructions, but you need to provide us with a #mwe (this is a link, please read)

[Jireh Loreaux]

sigma_additivity is not what you want, because your sets are not disjoint (nor measurable), and you certainly never want to write axiom.

In the definition of equiv, Lean probably interpretys 0 and 1 as terms of ℕ, not terms of ℝ, so the Icc 0 1 : Set ℕ and in that case Icc 0 1 = {0, 1} which is not what you want. You can tell Lean these should be real numbers by doing (Icc 0 1 : Set ℝ).

At the same time, ℚ is a type, not a set, so you can't write ∈ ℚ. You'll want x - y ∈ Set.range (Rat.cast : ℚ → ℝ).

[Jireh Loreaux]

But yes, please give a #mwe

[Marvin Sigg]

Right, apologies. Here is my MWE (I spare you the rest of the document for now)

import Mathlib

set_option warningAsError false


open Set Filter Real MeasureTheory Function

axiom monotony {A B : Set ℝ} (h : A ⊆ B) : volume A ≤ volume B

axiom translation_invariance {A : Set ℝ} {x : ℝ} : volume ({a + x|a ∈ A}) = volume A

axiom normalised {l : ℝ} : volume (Icc 0 l) = ENNReal.ofReal l

axiom sigma_additivity {A : ℕ → Set ℝ} : volume (⋃ n, A n) = ∑ n, volume (A n)

def equiv {x y : Icc 0 1} : Prop :=
  (x - y) ∈ ℚ
-- lemma : equiv really an equivalence relation

lemma test : (ℚ ∩ (Icc -1 1)) ⊆ ℚ

[Aaron Liu]

Why are you using axiom?

[Kevin Buzzard]

\Q is a type, not a set, so (x - y) \in \Q makes no sense. Lean uses type theory not set theory. You can make subsets of a type but \Q is not a subset of \R, it's a distinct type equipped with a function to \R.

[Marvin Sigg]

Aaron Liu schrieb:

Why are you using axiom?

So I don't have to write := by sorry

[Jireh Loreaux]

adding axioms is dangerous, because if you add them and they are inconsistent (as yours were), then you can easily prove false.

[Jireh Loreaux]

e.g., your normalised and sigma_additivity together are sufficient to prove False. (after you make the sigma additivity compile by using ∑' instead of ∑)

[Marvin Sigg]

Gotcha, I switched to lemmas and added (h : ∀ i j, i ≠ j → A i ∩ A j = ∅)

[Jireh Loreaux]

You can write that as Pairwise (Disjoint on A) and it will give you access to more API.

[Jireh Loreaux]

I know you probably already understand, but just to give you an example:

proof of false

import Mathlib

open Set Filter Real MeasureTheory Function

axiom normalised {l : ℝ} : volume (Icc 0 l) = ENNReal.ofReal l
axiom sigma_additivity {A : ℕ → Set ℝ} : volume (⋃ n, A n) = ∑' n, volume (A n)

example : False := by
  apply ENNReal.one_ne_top
  convert sigma_additivity (A := fun _ ↦ Icc 0 1)
  · simp [iUnion]
  · simp

[Marvin Sigg]

I'm sorry, but what does "access to more API" mean?

[Mario Carneiro]

if you use a hypothesis in "standard form", more lemmas will have that exact thing as a hypothesis so you don't have a complicated side condition every time you want to use lemmas

[Mario Carneiro]

it's very often the case that there is more than one way to say something, and the library tries to pick one variation in each case and use it canonically in all relevant lemmas

[Jireh Loreaux]

e.g., this is how it is phrased in docs#MeasureTheory.measure_iUnion

[Aaron Liu]

Marvin Sigg said:

Aaron Liu schrieb:

Why are you using axiom?

So I don't have to write := by sorry

If you do := by exact? and it finds a lemma, then now you know what it's called. If it doesn't find a lemma, there's a chance you stated it wrong.

[Kevin Buzzard]

And by "wrong" this might mean "mathematically incorrectly" or it might just mean "in an unidiomatic way".

[Marvin Sigg]

Hi folks, hope you're doing well. I wanted to ask if someone could give me a hint as how to implement the choice function, since the Vitali set relies on it. Here's what I got so far:

import Mathlib

set_option warningAsError false

open Set Filter Real MeasureTheory Function Rat

-- what we expect the measure to fulfill
lemma monotony {A B : Set ℝ} (h : A ⊆ B) : volume A ≤ volume B := by sorry
lemma translation_invariance {A : Set ℝ} {x : ℝ} : volume ({a + x|a ∈ A}) = volume A := by sorry
lemma normalised {l : ℝ} : volume (Icc 0 l) = ENNReal.ofReal l := by sorry
lemma sigma_additivity {A : ℕ → Set ℝ} (h : Pairwise (Disjoint on A)): volume (⋃ n, A n) = ∑' n, volume (A n) := by sorry

-- equivalence relation for Vitali set
def equiv {x y : ℝ} (hx : x ∈ Icc 0 1) (hy : y ∈ Icc 0 1) : Prop :=
  ∃ q : ℚ, x - y = q
-- lemma : need to show that equiv really an equivalence relation

-- define a bijection from the naturals to the rationals between -1 and 1
def η : Set ℝ := {x : ℝ | x ≥ -1 ∧ x ≤ 1 ∧ ∃ q : ℚ, x = q}
noncomputable def ξ : ℕ → η := sorry
lemma ξ_inj: Function.Injective ξ := by sorry
lemma ξ_surj : ∀ y ∈ η, ∃ x, ξ x = y := by sorry

-- one element from each equivalence class by axiom of choice. This is where I'm struggling.
noncomputable def M0 : Set ℝ (h : ∀ x ∈ M0, y ∈ M0 ∧ equiv x y → x = y) := sorry

[Aaron Liu]

Can you post a #mwe?

[Aaron Liu]

noncomputable def M0 doesn't work for me on the web editor.

[Marvin Sigg]

This is what I'm asking. I want to codify that there is exactly one element from each equivalence class in M0, so if for any xin M0 there exists a yin M0 such that they are equivalent, they must be equal.
Edit: I now realise that this only means that there exists at most one representative (as opposed to the required 'there exists exactly one representative'). It's quite tricky to think of a way to codify that for any equivalence class there is a representative in M0.

[Mario Carneiro]

I guess ∀ x ∈ Icc 0 1, ∃ y ∈ M0, equiv x y

[Mario Carneiro]

or ∀ x ∈ Icc 0 1, ∃! y ∈ M0, equiv x y to do existence and uniqueness in one go

[Mario Carneiro]

You should drop the hypotheses hx and hy from equiv, they will just get in the way

[Mario Carneiro]

this theorem statement is still not right, as you are using volume from the library rather than having it as a hypothesis. This means it's about lebesgue measure specifically, rather than any function which satisfies the four properties

[Mario Carneiro]

if you want it to be about lebesgue measure, then you can remove the lemmas since they are already proved

[Mario Carneiro]

here is maybe a simpler setup:

-- equivalence relation for Vitali set
def equiv (x y : Icc 0 1) : Prop :=
  ∃ q : ℚ, x - y = q
-- lemma : need to show that equiv really an equivalence relation

noncomputable def M0 : Set ℝ := range fun q : Quot equiv => q.out

[Mario Carneiro]

this is a bit more lean idiomatic in using quotients rather than equivalence classes

[Mario Carneiro]

We define equiv to be an equivalence relation directly on the set Icc 0 1 as a type, and then take the quotient wrt that equivalence relation to get the type Quot equiv. Quot.out uses the axiom of choice to reverse the quotient map and get an element of Icc 0 1 back out and this is coerced to a ℝ

[Mario Carneiro]

(we actually don't need to show it is really an equivalence relation to make this definition)

[Marvin Sigg]

Hello everyone, deadline is nearing but I've also made progress. My question is regarding the sum over all "siblings" of the Vitali set; I keep getting syntax errors, specifically

application type mismatch
  ∑' (_ : i ∈ shiftRange), μ.μ (vitaliSet' i)
argument
  fun h => μ.μ (vitaliSet' i)
has type
  i ∈ shiftRange → ENNReal : Type
but is expected to have type
  ?m.3495 i → ENNReal : Type (max ?u.2833 0)

My MWE is

import Mathlib

set_option warningAsError false


open Set Filter Real Function Rat
noncomputable section


structure naiveMeasure where
  μ : Set ℝ → ENNReal
  monotony {A B : Set ℝ} (h : A ⊆ B) : μ A ≤ μ B
  translation_invariance {A : Set ℝ} {x : ℝ} : μ ({a + x|a ∈ A}) = μ A
  normalised {l : ℝ} : μ (Icc 0 l) = ENNReal.ofReal l
  sigma_additivity {A : ℕ → Set ℝ} (h : Pairwise (Disjoint on A)): μ (⋃ n, A n) = ∑' n, μ (A n)

instance : CoeFun naiveMeasure (λ _ => Set ℝ → ENNReal) where
  coe := naiveMeasure.μ

def I : Set ℝ := Icc 0 1
def J : Set ℝ := Icc (-1) 2

instance equiv : Setoid I where
  r := fun x y ↦ (x.val - y.val) ∈ range ((↑) : ℚ → ℝ)
  iseqv := sorry


def vitaliSet : Set ℝ := { x : ℝ | ∃ y : I, Quot.mk equiv y = ⟦y⟧ ∧ x = y.val}

def shiftRange : Set ℝ := Icc (-1) 1 ∩ range ((↑) : ℚ → ℝ)

def vitaliSet' (j : ℝ) : Set ℝ := (fun x ↦ x + j)'' vitaliSet

def vitaliUnion : Set ℝ := ⋃ i ∈ shiftRange, vitaliSet' i

lemma sigma (μ : naiveMeasure) : μ vitaliUnion = ∑' i ∈ shiftRange, μ (vitaliSet' i) := by
  sorry

Can someone help me out here? My goal is to avoid the messy stuff with the bijection between the naturals and the rationals between -1 and 1, if at all possible.

[Aaron Liu]

tsum doesn't work on props

[Aaron Liu]

As a workaround, you can sum over an if then else

[Marvin Sigg]

Could you give me a basic example of summing over an if then else?

[Aaron Liu]

∑' i, if i ∈ shiftRange then μ (vitaliSet' i) else 0

[Marvin Sigg]

I see, thank you already. However, now the error message "failed to synthesize
Decidable (i ∈ shiftRange)" crops up, which I've never seen before.

[Aaron Liu]

That has to do with how if then else statements work, since everything is noncomputable anyways I think you should just open scoped Classical.

[Aaron Liu]

If you do somehow manage to obtain an instance of Decidable (i ∈ shiftRange) that's not just Classical.propDecidable you might run into some problems though.

[Marvin Sigg]

One last thing, how do I use the notion of infinity, which is an acceptable output of the measure function? Naively typing ∞ yields the error message expected token. What is the meaningful way of equating the measure of, say the whole real number line, to infinity?

[Aaron Liu]

Are you working with ENNReal or EReal?

[Aaron Liu]

If you are, then ⊤ will be infinity

[Aaron Liu]

I just noticed you have structure naiveMeasure in your example instead of using docs#MeasureTheory.Measure. Is there a reason for that?

[Marvin Sigg]

Thank you!
I wanted to have as naive an approach as possible, mirroring the time we learned about Vitali in lecture for the first time. But no, there's not a specific reason

[Jireh Loreaux]

If you open scoped ENNReal, then you can write ∞.