Introduction to Measure Theory, Section 1.2: Lebesgue measure

A companion to (the introduction to) Section 1.2 of the book "An introduction to Measure Theory".

theorem exercise_1_2_1_union : ∃ (E : ℕ → Set ℝ), (∀ (n : ℕ), Bornology.IsBounded (E n)) ∧ (∀ (n : ℕ), JordanMeasurable (⇑Real.equiv_EuclideanSpace' '' E n)) ∧ (∀ (n : ℕ), E n ⊆ Set.Icc 0 1) ∧ ¬JordanMeasurable (⋃ (n : ℕ), ⇑Real.equiv_EuclideanSpace' '' E n)

Exercise 1.2.1 (countable union)

def Ex_1_2_2b : Decidable (∀ (f : ℕ → ℝ → ℝ) (F : ℝ → ℝ), (∃ (M : ℝ), ∀ (n : ℕ), ∀ x ∈ Set.Icc 0 1, |f n x| ≤ M) → (∀ x ∈ Set.Icc 0 1, TendstoUniformly f F Filter.atTop) → (∀ (n : ℕ), RiemannIntegrableOn (f n) (BoundedInterval.Icc 0 1)) → RiemannIntegrableOn F (BoundedInterval.Icc 0 1))

Exercise 1.2.2

Equations

• Ex_1_2_2b = sorry

theorem Jordan_outer_eq {d : ℕ} {E : Set (EuclideanSpace' d)} (hE : Bornology.IsBounded E) : Jordan_outer_measure E = sInf ((fun (S : Finset (Box d)) => ∑ B ∈ S, B.volume) '' {S : Finset (Box d) | E ⊆ ⋃ B ∈ S, ↑B})

noncomputable def Lebesgue_outer_measure {d : ℕ} (E : Set (EuclideanSpace' d)) : EReal

This definition deviates from the text by working with countable families of boxes rather than boxes indexed by the natural numbers. This becomes important in dimension zero, when all boxes are non-empty.

Equations

• Lebesgue_outer_measure E = sInf {V : EReal | ∃ (X : Set ℕ) (S : ↑X → Box d), E ⊆ ⋃ (n : ↑X), ↑(S n) ∧ V = ∑' (n : ↑X), ↑(S n).volume}

theorem Lebesgue_outer_measure_eq_nat_indexed {d : ℕ} (hd : 0 < d) (E : Set (EuclideanSpace' d)) : Lebesgue_outer_measure E = sInf ((fun (S : ℕ → Box d) => ∑' (n : ℕ), ↑(S n).volume) '' {S : ℕ → Box d | E ⊆ ⋃ (n : ℕ), ↑(S n)})

When d > 0, the Lebesgue outer measure can be computed using ℕ-indexed box sequences, which is equivalent to the definition using countable families. This is because we can pad any countable family with zero-volume boxes (which exist when d > 0).

theorem hasSum_indicator_top_of_infinite (X : Set ℕ) (hX : ¬X.Finite) : HasSum (fun (n : ℕ) => if n ∈ X then 1 else 0) ⊤

Helper lemma: If X is an infinite subset of ℕ, then the sum of its indicator function (mapping elements of X to 1 and others to 0) diverges to ⊤ in EReal.

theorem Lebesgue_outer_measure_of_dim_zero {E : Set (EuclideanSpace' 0)} : Lebesgue_outer_measure E = if E.Nonempty then 1 else 0

In dimension 0, the Lebesgue outer measure is 1 for non-empty sets and 0 for the empty set. This is because all boxes in dimension 0 are singletons with volume 1 (empty product).

theorem EReal.sInf_image_coe {s : Set ℝ} (hs : s.Nonempty) (h_bdd : BddBelow s) : sInf ((fun (x : ℝ) => ↑x) '' s) = ↑(sInf s)

Coercion ℝ → EReal preserves infimums for nonempty bounded-below sets

theorem tsum_volume_finset_eq {d : ℕ} (hd : 0 < d) (S : Finset (Box d)) : have S_list := S.toList; have zero_box := { side := fun (i : Fin d) => if ↑i = 0 then ∅ else BoundedInterval.Icc 0 0 }; have S_seq := fun (n : ℕ) => if h : n < S_list.length then S_list.get ⟨n, h⟩ else zero_box; ∑' (n : ℕ), ↑(S_seq n).volume = ↑(∑ B ∈ S, B.volume)

When enumerating a finset to a sequence padded with empty boxes, the infinite sum of volumes equals the finite sum

theorem Lebesgue_outer_measure_le_Jordan {d : ℕ} {E : Set (EuclideanSpace' d)} (hE : Bornology.IsBounded E) : Lebesgue_outer_measure E ≤ ↑(Jordan_outer_measure E)

theorem Countable.Lebesgue_measure {d : ℕ} (hd : 0 < d) {E : Set (EuclideanSpace' d)} (hE : E.Countable) : Lebesgue_outer_measure E = 0

def LebesgueMeasurable {d : ℕ} (E : Set (EuclideanSpace' d)) : Prop

Equations

• LebesgueMeasurable E = ∀ ε > 0, ∃ (U : Set (EuclideanSpace' d)), IsOpen U ∧ E ⊆ U ∧ Lebesgue_outer_measure (U \ E) ≤ ε

noncomputable def Lebesgue_measure {d : ℕ} (E : Set (EuclideanSpace' d)) : EReal

Equations

• Lebesgue_measure E = Lebesgue_outer_measure E