def Rat.addSubgroup : AddSubgroup ℝ

The additive subgroup of ℚ in ℝ

Equations

• Rat.addSubgroup = { carrier := Set.range Rat.cast, add_mem' := @Rat.addSubgroup._proof_1, zero_mem' := Rat.addSubgroup._proof_2, neg_mem' := @Rat.addSubgroup._proof_3 }

@[reducible, inline]

abbrev RealModRat : Type

The quotient group ℝ/ℚ (reals modulo rationals)

Equations

• RealModRat = (ℝ ⧸ Rat.addSubgroup)

theorem coset_intersects_unit_interval (c : RealModRat) : ∃ x ∈ Set.Icc 0 1, ↑x = c

ℚ is dense in ℝ, so every coset of ℝ/ℚ intersects [0,1]

noncomputable def VitaliSet : Set ℝ

The Vitali set: choose one representative from each coset that lies in [0,1]

Equations

• VitaliSet = Set.range fun (c : RealModRat) => ⋯.choose

theorem VitaliSet_subset_unit_interval : VitaliSet ⊆ Set.Icc 0 1

Each element of the Vitali set is in [0,1]

theorem unit_interval_covered_by_translates : Set.Icc 0 1 ⊆ ⋃ q ∈ Set.Icc (-1) 1, VitaliSet + {↑q}

Key lemma: [0,1] is covered by translates of E by rationals in [-1,1]

theorem rat_Icc_countable : {q : ℚ | q ∈ Set.Icc (-1) 1}.Countable

The rationals in [-1,1] are countable

theorem Lebesgue_measure.Icc_eq (a b : ℝ) (hab : a ≤ b) : Lebesgue_measure (⇑Real.equiv_EuclideanSpace' '' Set.Icc a b) = ↑(b - a)

The Lebesgue measure of a closed interval [a,b] in ℝ (embedded in EuclideanSpace' 1) equals b - a

theorem VitaliSet.nonmeasurable : ¬LebesgueMeasurable (⇑Real.equiv_EuclideanSpace' '' VitaliSet)

The Vitali set (lifted to EuclideanSpace' 1) is not Lebesgue measurable. This is the core of Proposition 1.2.18.

theorem LebesgueMeasurable.nonmeasurable : ∃ E ⊆ ⇑Real.equiv_EuclideanSpace' '' Set.Icc 0 1, ¬LebesgueMeasurable E

Proposition 1.2.18