theorem IsOpen.measurable {d : ℕ} {E : Set (EuclideanSpace' d)} (hE : IsOpen E) : LebesgueMeasurable E

Lemma 1.2.13(i) (Every open set is Lebesgue measurable).

theorem IsClosed.measurable {d : ℕ} {E : Set (EuclideanSpace' d)} (hE : IsClosed E) : LebesgueMeasurable E

Lemma 1.2.13(ii) (Every closed set is Lebesgue measurable).

@[reducible, inline]

abbrev IsNull {d : ℕ} (E : Set (EuclideanSpace' d)) : Prop

Equations

• IsNull E = (Lebesgue_outer_measure E = 0)

theorem IsNull.measurable {d : ℕ} {E : Set (EuclideanSpace' d)} (hE : IsNull E) : LebesgueMeasurable E

Lemma 1.2.13(iii) (Every null set is Lebesgue measurable).

theorem IsNull.subset {d : ℕ} {E F : Set (EuclideanSpace' d)} (hE : IsNull E) (hFE : F ⊆ E) : IsNull F

A subset of a null set is null.

theorem LebesgueMeasurable.empty {d : ℕ} : LebesgueMeasurable ∅

Lemma 1.2.13(iv) (Empty set is measurable).

theorem LebesgueMeasurable.empty' {d : ℕ} : LebesgueMeasurable ∅

theorem LebesgueMeasurable.countable_union {d : ℕ} {E : ℕ → Set (EuclideanSpace' d)} (hE : ∀ (n : ℕ), LebesgueMeasurable (E n)) : LebesgueMeasurable (⋃ (n : ℕ), E n)

Lemma 1.2.13(vi) (Countable union of measurable sets is measurable).

theorem LebesgueMeasurable.complement {d : ℕ} {E : Set (EuclideanSpace' d)} (hE : LebesgueMeasurable E) : LebesgueMeasurable Eᶜ

Lemma 1.2.13(v) (Complement of a measurable set is measurable).

theorem LebesgueMeasurable.finite_union {d n : ℕ} {E : Fin n → Set (EuclideanSpace' d)} (hE : ∀ (i : Fin n), LebesgueMeasurable (E i)) : LebesgueMeasurable (⋃ (i : Fin n), E i)

theorem LebesgueMeasurable.union {d : ℕ} {E F : Set (EuclideanSpace' d)} (hE : LebesgueMeasurable E) (hF : LebesgueMeasurable F) : LebesgueMeasurable (E ∪ F)

theorem LebesgueMeasurable.countable_inter {d : ℕ} {E : ℕ → Set (EuclideanSpace' d)} (hE : ∀ (n : ℕ), LebesgueMeasurable (E n)) : LebesgueMeasurable (⋂ (n : ℕ), E n)

Lemma 1.2.13(vii) (Countable intersection of measurable sets is measurable).

theorem LebesgueMeasurable.finite_inter {d n : ℕ} {E : Fin n → Set (EuclideanSpace' d)} (hE : ∀ (i : Fin n), LebesgueMeasurable (E i)) : LebesgueMeasurable (⋂ (i : Fin n), E i)

theorem LebesgueMeasurable.inter {d : ℕ} {E F : Set (EuclideanSpace' d)} (hE : LebesgueMeasurable E) (hF : LebesgueMeasurable F) : LebesgueMeasurable (E ∩ F)

theorem LebesgueMeasurable.finset_inter {d : ℕ} {α : Type u_1} [DecidableEq α] {E : α → Set (EuclideanSpace' d)} {S : Finset α} (hE : ∀ i ∈ S, LebesgueMeasurable (E i)) : LebesgueMeasurable (⋂ i ∈ S, E i)

Finite intersection indexed by a Finset is Lebesgue measurable.

theorem LebesgueMeasurable.finset_union {d : ℕ} {α : Type u_1} [DecidableEq α] {E : α → Set (EuclideanSpace' d)} {S : Finset α} (hE : ∀ i ∈ S, LebesgueMeasurable (E i)) : LebesgueMeasurable (⋃ i ∈ S, E i)

Finite union indexed by a Finset is Lebesgue measurable.

theorem LebesgueMeasurable.of_ae_eq {d : ℕ} {A B N : Set (EuclideanSpace' d)} (hB : LebesgueMeasurable B) (hN : IsNull N) (h_eq : A ∩ Nᶜ = B ∩ Nᶜ) : LebesgueMeasurable A

If A = B outside a null set N (i.e., A ∩ Nᶜ = B ∩ Nᶜ), then A is measurable if B is.

theorem LebesgueMeasurable.closedBall {d : ℕ} (c : EuclideanSpace' d) (r : ℝ) : LebesgueMeasurable (Metric.closedBall c r)

Closed balls are Lebesgue measurable.

theorem LebesgueMeasurable.TFAE {d : ℕ} (E : Set (EuclideanSpace' d)) : [LebesgueMeasurable E, ∀ ε > 0, ∃ (U : Set (EuclideanSpace' d)), IsOpen U ∧ E ⊆ U ∧ Lebesgue_outer_measure (U \ E) ≤ ε, ∀ ε > 0, ∃ (U : Set (EuclideanSpace' d)), IsOpen U ∧ Lebesgue_outer_measure (symmDiff U E) ≤ ε, ∀ ε > 0, ∃ (F : Set (EuclideanSpace' d)), IsClosed F ∧ F ⊆ E ∧ Lebesgue_outer_measure (E \ F) ≤ ε, ∀ ε > 0, ∃ (F : Set (EuclideanSpace' d)), IsClosed F ∧ Lebesgue_outer_measure (symmDiff F E) ≤ ε, ∀ ε > 0, ∃ (E' : Set (EuclideanSpace' d)), LebesgueMeasurable E' ∧ Lebesgue_outer_measure (symmDiff E' E) ≤ ε].TFAE

Exercise 1.2.7 (Criteria for measurability)

theorem Jordan_measurable.lebesgue {d : ℕ} {E : Set (EuclideanSpace' d)} (hE : JordanMeasurable E) : LebesgueMeasurable E

Exercise 1.2.8

@[reducible, inline]

abbrev CantorInterval (n : ℕ) : Set ℝ

Equations

• CantorInterval n = ⋃ (a : Fin n → ↑{0, 2}), ↑(BoundedInterval.Icc (∑ i : Fin n, ↑↑(a i) / 3 ^ (↑i + 1)) (∑ i : Fin n, ↑↑(a i) / 3 ^ (↑i + 1) + 1 / 3 ^ n))

@[reducible, inline]

abbrev CantorSet : Set ℝ

Equations

• CantorSet = ⋂ (n : ℕ), CantorInterval n

theorem CantorSet.compact : IsCompact CantorSet

Exercise 1.2.9 (Middle thirds Cantor set )

theorem CantorSet.uncountable : Uncountable ↑CantorSet

theorem CantorSet.null : IsNull (⇑Real.equiv_EuclideanSpace' '' CantorSet)

theorem Jordan_measurable.Lebesgue_measure {d : ℕ} {E : Set (EuclideanSpace' d)} (hE : JordanMeasurable E) : _root_.Lebesgue_measure E = ↑hE.measure

@[simp]

theorem Lebesgue_measure.empty {d : ℕ} : Lebesgue_measure ∅ = 0

Lemma 1.2.15(a) (Empty set has zero Lebesgue measure). The proof is missing.

theorem Lebesgue_measure.countable_union {d : ℕ} {E : ℕ → Set (EuclideanSpace' d)} (hmes : ∀ (n : ℕ), LebesgueMeasurable (E n)) (hdisj : Set.univ.PairwiseDisjoint E) : Lebesgue_measure (⋃ (n : ℕ), E n) = ∑' (n : ℕ), Lebesgue_measure (E n)

Lemma 1.2.15(b) (Countable additivity). Strategy: m(⋃ E_n) = ∑' m(E_n) for pairwise disjoint measurable sets.

• Direction ≤: Countable subadditivity (Lebesgue_outer_measure.union_le)

• Direction ≥: Decompose ℝᵈ into annuli Aₘ, express each E_n = ⋃_m (E_n ∩ Aₘ), apply bounded case to the doubly-indexed family $(E_n ∩ Aₘ)$.

theorem Lebesgue_measure.finite_union {d n : ℕ} {E : Fin n → Set (EuclideanSpace' d)} (hmes : ∀ (n : Fin n), LebesgueMeasurable (E n)) (hdisj : Set.univ.PairwiseDisjoint E) : Lebesgue_measure (⋃ (n : Fin n), E n) = ∑' (n : Fin n), Lebesgue_measure (E n)

theorem Lebesgue_measure.union {d : ℕ} {E F : Set (EuclideanSpace' d)} (hE : LebesgueMeasurable E) (hF : LebesgueMeasurable F) (hdisj : E ∩ F = ∅) : Lebesgue_measure (E ∪ F) = Lebesgue_measure E + Lebesgue_measure F

theorem Lebesgue_measure.upward_monotone_convergence {d : ℕ} {E : ℕ → Set (EuclideanSpace' d)} (hE : ∀ (n : ℕ), LebesgueMeasurable (E n)) (hmono : ∀ (n : ℕ), E n ⊆ E (n + 1)) : Filter.Tendsto (fun (n : ℕ) => Lebesgue_measure (E n)) Filter.atTop (nhds (Lebesgue_measure (⋃ (n : ℕ), E n)))

Exercise 1.2.11(a) (Upward monotone convergence)

theorem Lebesgue_measure.downward_monotone_convergence {d : ℕ} {E : ℕ → Set (EuclideanSpace' d)} (hE : ∀ (n : ℕ), LebesgueMeasurable (E n)) (hmono : ∀ (n : ℕ), E (n + 1) ⊆ E n) (hfin : ∃ (n : ℕ), Lebesgue_measure (E n) < ⊤) : Filter.Tendsto (fun (n : ℕ) => Lebesgue_measure (E n)) Filter.atTop (nhds (Lebesgue_measure (⋂ (n : ℕ), E n)))

Exercise 1.2.11(b) (Downward monotone convergence)

theorem Lebesgue_measure.eq {d : ℕ} {E : Set (EuclideanSpace' d)} (hE : LebesgueMeasurable E) : Lebesgue_measure E = sSup {M : EReal | ∃ K ⊆ E, IsCompact K ∧ M = Lebesgue_measure K}

Exercise 1.2.15 (Inner regularity)

theorem LebesgueMeasurable.finite_TFAE {d : ℕ} (E : Set (EuclideanSpace' d)) : [LebesgueMeasurable E ∧ Lebesgue_measure E < ⊤, ∀ ε > 0, ∃ (U : Set (EuclideanSpace' d)), IsOpen U ∧ E ⊆ U ∧ Lebesgue_measure U < ⊤ ∧ Lebesgue_outer_measure (U \ E) ≤ ε, ∀ ε > 0, ∃ (U : Set (EuclideanSpace' d)), IsOpen U ∧ Bornology.IsBounded U ∧ Lebesgue_outer_measure (symmDiff U E) ≤ ε, ∀ ε > 0, ∃ (F : Set (EuclideanSpace' d)), IsCompact F ∧ F ⊆ E ∧ Lebesgue_outer_measure (E \ F) ≤ ε, ∀ ε > 0, ∃ (F : Set (EuclideanSpace' d)), IsCompact F ∧ Lebesgue_outer_measure (symmDiff F E) ≤ ε, ∀ ε > 0, ∃ (E' : Set (EuclideanSpace' d)), LebesgueMeasurable E' ∧ Lebesgue_measure E' < ⊤ ∧ Lebesgue_outer_measure (symmDiff E' E) ≤ ε, ∀ ε > 0, ∃ (E' : Set (EuclideanSpace' d)), LebesgueMeasurable E' ∧ Bornology.IsBounded E' ∧ Lebesgue_outer_measure (symmDiff E' E) ≤ ε, ∀ ε > 0, ∃ (E' : Set (EuclideanSpace' d)), IsElementary E' ∧ Lebesgue_outer_measure (symmDiff E' E) ≤ ε, ∀ ε > 0, ∃ (n : ℤ) (F : Finset (Box d)), (∀ B ∈ F, B.IsDyadicAtScale n) ∧ Lebesgue_outer_measure (symmDiff (⋃ B ∈ F, ↑B) E) ≤ ε].TFAE

Exercise 1.2.16 (Criteria for measurability)

theorem LebesgueMeasurable.caratheodory {d : ℕ} (E : Set (EuclideanSpace' d)) : [LebesgueMeasurable E, ∀ (A : Set (EuclideanSpace' d)), IsElementary A → Lebesgue_outer_measure A = Lebesgue_outer_measure (A ∩ E) + Lebesgue_outer_measure (A \ E), ∀ (B : Box d), Lebesgue_outer_measure ↑B = Lebesgue_outer_measure (↑B ∩ E) + Lebesgue_outer_measure (↑B \ E)].TFAE

Exercise 1.2.17 (Caratheodory criterion one direction)

theorem Bornology.IsBounded.inElementary {d : ℕ} {E : Set (EuclideanSpace' d)} (hE : IsBounded E) : ∃ (A : Set (EuclideanSpace' d)), IsElementary A ∧ E ⊆ A

noncomputable def inner_measure {d : ℕ} {E : Set (EuclideanSpace' d)} (hE : Bornology.IsBounded E) : ℝ

Equations

• inner_measure hE = (Lebesgue_measure ⋯.choose).toReal - (Lebesgue_measure (⋯.choose \ E)).toReal

theorem inner_measure.eq {d : ℕ} {E A : Set (EuclideanSpace' d)} (hE : Bornology.IsBounded E) (hA : IsElementary A) (hsub : E ⊆ A) : ↑(inner_measure hE) = Lebesgue_measure A - Lebesgue_outer_measure (A \ E)

Exercise 1.2.18(i) (Inner measure)

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

Exercise 1.2.18(ii) (Inner measure)

theorem inner_measure.eq_iff {d : ℕ} {E : Set (EuclideanSpace' d)} (hE : Bornology.IsBounded E) : ↑(inner_measure hE) = Lebesgue_outer_measure E ↔ LebesgueMeasurable E

Exercise 1.2.18(ii) (Inner measure)

def IsFσ {X : Type u_1} [TopologicalSpace X] (s : Set X) : Prop

Equations

• IsFσ s = ∃ (T : Set (Set X)), (∀ t ∈ T, IsClosed t) ∧ T.Countable ∧ s = ⋃₀ T

theorem LebesgueMeasurable.TFAE' {d : ℕ} (E : Set (EuclideanSpace' d)) : [LebesgueMeasurable E, ∃ (F : Set (EuclideanSpace' d)) (N : Set (EuclideanSpace' d)), IsGδ F ∧ IsNull N ∧ E = F \ N, ∃ (F : Set (EuclideanSpace' d)) (N : Set (EuclideanSpace' d)), IsFσ F ∧ IsNull N ∧ E = F ∪ N].TFAE

Exercise 1.2.19

theorem LebesgueMeasurable.translate {d : ℕ} (E : Set (EuclideanSpace' d)) (x : EuclideanSpace' d) : LebesgueMeasurable E ↔ LebesgueMeasurable (E + {x})

Exercise 1.2.20 (Translation invariance)

theorem Lebesgue_measure.translate {d : ℕ} {E : Set (EuclideanSpace' d)} (x : EuclideanSpace' d) (hE : LebesgueMeasurable E) : Lebesgue_measure (E + {x}) = Lebesgue_measure E

theorem LebesgueMeasurable.linear {d : ℕ} (T : EuclideanSpace' d ≃ₗ[ℝ] EuclideanSpace' d) {E : Set (EuclideanSpace' d)} (hE : LebesgueMeasurable E) : LebesgueMeasurable (⇑T '' E)

Exercise 1.2.21 (Change of variables)

theorem Lebesgue_measure.linear {d : ℕ} (A : Matrix (Fin d) (Fin d) ℝ) [Invertible A] {E : Set (EuclideanSpace' d)} (hE : LebesgueMeasurable E) : Lebesgue_measure (⇑A.linear_equiv '' E) = ↑|A.det| * Lebesgue_measure E

Exercise 1.2.21 (Change of variables)

theorem Lebesgue_outer_measure.prod {d₁ d₂ : ℕ} {E₁ : Set (EuclideanSpace' d₁)} {E₂ : Set (EuclideanSpace' d₂)} : Lebesgue_outer_measure (EuclideanSpace'.prod E₁ E₂) ≤ Lebesgue_outer_measure E₁ * Lebesgue_outer_measure E₂

Exercise 1.2.22

theorem LebesgueMeasurable.prod {d₁ d₂ : ℕ} {E₁ : Set (EuclideanSpace' d₁)} {E₂ : Set (EuclideanSpace' d₂)} (hE₁ : LebesgueMeasurable E₁) (hE₂ : LebesgueMeasurable E₂) : LebesgueMeasurable (EuclideanSpace'.prod E₁ E₂)

Exercise 1.2.22

theorem Lebesgue_measure.prod {d₁ d₂ : ℕ} {E₁ : Set (EuclideanSpace' d₁)} {E₂ : Set (EuclideanSpace' d₂)} (hE₁ : LebesgueMeasurable E₁) (hE₂ : LebesgueMeasurable E₂) : Lebesgue_measure (EuclideanSpace'.prod E₁ E₂) = Lebesgue_measure E₁ * Lebesgue_measure E₂

Exercise 1.2.22

theorem Lebesgue_measure.unique {d : ℕ} (m : Set (EuclideanSpace' d) → EReal) (h_empty : m ∅ = 0) (h_pos : ∀ (E : Set (EuclideanSpace' d)), 0 ≤ m E) (h_add : ∀ (E : ℕ → Set (EuclideanSpace' d)), Set.univ.PairwiseDisjoint E → (∀ (n : ℕ), LebesgueMeasurable (E n)) → m (⋃ (n : ℕ), E n) = ∑' (n : ℕ), m (E n)) (hnorm : m ↑(Box.unit_cube d) = 1) (E : Set (EuclideanSpace' d)) : LebesgueMeasurable E → m E = Lebesgue_measure E

Exercise 1.2.23 (Uniqueness of Lebesgue measure)

@[implicit_reducible]

instance IsElementary.ae_equiv {d : ℕ} {A : Set (EuclideanSpace' d)} (hA : IsElementary A) : Setoid (Set ↑A)

Exercise 1.2.24(i) (Lebesgue measure as the completion of elementary measure)

Equations

• hA.ae_equiv = { r := fun (E F : Set ↑A) => IsNull (Subtype.val '' symmDiff E F), iseqv := ⋯ }

def IsElementary.ae_subsets {d : ℕ} {A : Set (EuclideanSpace' d)} (hA : IsElementary A) : Type

Equations

• hA.ae_subsets = Quotient hA.ae_equiv

def IsElementary.ae_quot {d : ℕ} {A : Set (EuclideanSpace' d)} (hA : IsElementary A) (E : Set ↑A) : hA.ae_subsets

Equations

• hA.ae_quot E = Quotient.mk' E

noncomputable def IsElementary.dist {d : ℕ} {A : Set (EuclideanSpace' d)} (hA : IsElementary A) : hA.ae_subsets → hA.ae_subsets → ℝ

Exercise 1.2.24(ii) (Lebesgue measure as the completion of elementary measure)

Equations

• hA.dist = Quotient.lift₂ (fun (E F : Set ↑A) => (Lebesgue_outer_measure (Subtype.val '' symmDiff E F)).toReal) ⋯

@[implicit_reducible]

noncomputable instance IsElementary.metric {d : ℕ} {A : Set (EuclideanSpace' d)} (hA : IsElementary A) : MetricSpace hA.ae_subsets

Exercise 1.2.24(ii) (Lebesgue measure as the completion of elementary measure)

Equations

• hA.metric = { dist := hA.dist, dist_self := ⋯, dist_comm := ⋯, dist_triangle := ⋯, edist_dist := ⋯, uniformity_dist := ⋯, cobounded_sets := ⋯, eq_of_dist_eq_zero := ⋯ }

instance IsElementary.complete {d : ℕ} {A : Set (EuclideanSpace' d)} (hA : IsElementary A) : CompleteSpace hA.ae_subsets

Exercise 1.2.24(ii) (Lebesgue measure as the completion of elementary measure)

noncomputable def IsElementary.ae_elem {d : ℕ} {A : Set (EuclideanSpace' d)} (hA : IsElementary A) : Set hA.ae_subsets

Equations

• hA.ae_elem = {E : hA.ae_subsets | ∃ (F : Set ↑A), IsElementary (Subtype.val '' F) ∧ hA.ae_quot F = E}

noncomputable def IsElementary.ae_measurable {d : ℕ} {A : Set (EuclideanSpace' d)} (hA : IsElementary A) : Set hA.ae_subsets

Equations

• hA.ae_measurable = {E : hA.ae_subsets | ∃ (F : Set ↑A), LebesgueMeasurable (Subtype.val '' F) ∧ hA.ae_quot F = E}

theorem IsElementary.measurable_eq_closure_elem {d : ℕ} {A : Set (EuclideanSpace' d)} (hA : IsElementary A) : closure hA.ae_elem = hA.ae_measurable

Exercise 1.2.24(iii) (Lebesgue measure as the completion of elementary measure)

theorem IsElementary.measurable_complete {d : ℕ} {A : Set (EuclideanSpace' d)} (hA : IsElementary A) : closure hA.ae_elem = hA.ae_measurable

Exercise 1.2.24(c) (Lebesgue measure as the completion of elementary measure)

noncomputable def IsElementary.ae_measure {d : ℕ} {A : Set (EuclideanSpace' d)} (hA : IsElementary A) (E : ↑hA.ae_measurable) : ℝ

Equations

• hA.ae_measure E = (Lebesgue_measure (Subtype.val '' Exists.choose ⋯)).toReal

noncomputable def IsElementary.ae_elem_measure {d : ℕ} {A : Set (EuclideanSpace' d)} (hA : IsElementary A) (E : ↑hA.ae_elem) : ℝ

Equations

• hA.ae_elem_measure E = ⋯.measure

theorem IsElementary.ae_measure_eq_completion {d : ℕ} {A : Set (EuclideanSpace' d)} (hA : IsElementary A) (m : hA.ae_subsets → ℝ) : (ContinuousOn m hA.ae_measurable ∧ ∀ (E : ↑hA.ae_elem), m ↑E = hA.ae_elem_measure E) ↔ ∀ (E : ↑hA.ae_measurable), m ↑E = hA.ae_measure E

Exercise 1.2.24(iv) (Lebesgue measure as the completion of elementary measure)

@[reducible, inline]

noncomputable abbrev IsCurve {d : ℕ} (C : Set (EuclideanSpace' d)) : Prop

Equations

• IsCurve C = ∃ (a : ℝ) (b : ℝ) (γ : ℝ → EuclideanSpace' d), C = γ '' Set.Icc a b ∧ ContDiffOn ℝ 1 γ (Set.Icc a b)

theorem IsCurve.null {d : ℕ} (hd : d ≥ 2) {C : Set (EuclideanSpace' d)} (hC : IsCurve C) : IsNull C

Exercise 1.2.25(i)