def isLebesgueMeasurable (n : ℕ) (E : Set (EuclideanSpace ℝ (Fin n))) : Prop

Definition 7.5 (Lebesgue measurability): a set E ⊆ ℝ^n is Lebesgue measurable iff for every set A ⊆ ℝ^n, one has m*(A) = m*(A ∩ E) + m*(A \ E), where m* is Lebesgue outer measure.

Equations

• isLebesgueMeasurable n E = MeasureTheory.volume.IsCaratheodory E

noncomputable def lebesgueMeasureOfSet (n : ℕ) : { E : Set (EuclideanSpace ℝ (Fin n)) // isLebesgueMeasurable n E } → ENNReal

The Lebesgue measure m(E) as a function defined on Lebesgue measurable sets.

Equations

• lebesgueMeasureOfSet n E = MeasureTheory.volume.toOuterMeasure ↑E

theorem lastCoordinateIndex_lt (n : ℕ) (hn : 1 ≤ n) : n - 1 < n

The index of the last coordinate in Fin n when n ≥ 1.

def lastCoordinateIndex (n : ℕ) (hn : 1 ≤ n) : Fin n

The Fin n index corresponding to the last coordinate when n ≥ 1.

Equations

• lastCoordinateIndex n hn = ⟨n - 1, ⋯⟩

theorem helperForLemma_7_2_lastCoordinateProjectionContinuous (n : ℕ) (hn : 1 ≤ n) : Continuous fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp (lastCoordinateIndex n hn)

Helper for Lemma 7.2: continuity of the last-coordinate projection on ℝ^n.

theorem helperForLemma_7_2_halfSpaceIsOpen (n : ℕ) (hn : 1 ≤ n) : IsOpen {x : EuclideanSpace ℝ (Fin n) | 0 < x.ofLp (lastCoordinateIndex n hn)}

Helper for Lemma 7.2: the positivity half-space is open in ℝ^n.

theorem helperForLemma_7_2_isLebesgueMeasurable_of_isOpen (n : ℕ) {E : Set (EuclideanSpace ℝ (Fin n))} (hE : IsOpen E) : isLebesgueMeasurable n E

Helper for Lemma 7.2: every open subset of ℝ^n is Lebesgue measurable.

theorem halfSpace_isLebesgueMeasurable (n : ℕ) (hn : 1 ≤ n) : isLebesgueMeasurable n {x : EuclideanSpace ℝ (Fin n) | 0 < x.ofLp (lastCoordinateIndex n hn)}

Lemma 7.2 (Half-spaces are measurable): in ℝ^n with n ≥ 1, the open half-space {(x_1, …, x_n) : x_n > 0} (encoded via the last coordinate index) is Lebesgue measurable.

theorem helperForLemma_7_3_preimage_add_image (n : ℕ) (x : EuclideanSpace ℝ (Fin n)) (E : Set (EuclideanSpace ℝ (Fin n))) : (fun (y : EuclideanSpace ℝ (Fin n)) => x + y) ⁻¹' ((fun (y : EuclideanSpace ℝ (Fin n)) => x + y) '' E) = E

Helper for Lemma 7.3: preimage of a translated image under the same translation.

theorem helperForLemma_7_3_preimage_add_inter (n : ℕ) (x : EuclideanSpace ℝ (Fin n)) (E t : Set (EuclideanSpace ℝ (Fin n))) : (fun (y : EuclideanSpace ℝ (Fin n)) => x + y) ⁻¹' (t ∩ (fun (y : EuclideanSpace ℝ (Fin n)) => x + y) '' E) = (fun (y : EuclideanSpace ℝ (Fin n)) => x + y) ⁻¹' t ∩ E

Helper for Lemma 7.3: preimage of an intersection with a translated image.

theorem helperForLemma_7_3_preimage_add_diff (n : ℕ) (x : EuclideanSpace ℝ (Fin n)) (E t : Set (EuclideanSpace ℝ (Fin n))) : (fun (y : EuclideanSpace ℝ (Fin n)) => x + y) ⁻¹' (t \ (fun (y : EuclideanSpace ℝ (Fin n)) => x + y) '' E) = (fun (y : EuclideanSpace ℝ (Fin n)) => x + y) ⁻¹' t \ E

Helper for Lemma 7.3: preimage of a set difference with a translated image.

theorem helperForLemma_7_3_translation_preserves_measurability_and_volume (n : ℕ) (E : Set (EuclideanSpace ℝ (Fin n))) (x : EuclideanSpace ℝ (Fin n)) (hE : isLebesgueMeasurable n E) : isLebesgueMeasurable n ((fun (y : EuclideanSpace ℝ (Fin n)) => x + y) '' E) ∧ MeasureTheory.volume ((fun (y : EuclideanSpace ℝ (Fin n)) => x + y) '' E) = MeasureTheory.volume E

Helper for Lemma 7.3: translation preserves Lebesgue measurability and volume.

theorem helperForLemma_7_3_finite_union_and_intersection (n N : ℕ) (E : Fin N → Set (EuclideanSpace ℝ (Fin n))) (hE : ∀ (j : Fin N), isLebesgueMeasurable n (E j)) : isLebesgueMeasurable n (⋃ (j : Fin N), E j) ∧ isLebesgueMeasurable n (⋂ (j : Fin N), E j)

Helper for Lemma 7.3: finite unions and finite intersections of measurable sets are measurable.

theorem helperForLemma_7_3_coordinateProjectionContinuous (n : ℕ) (i : Fin n) : Continuous fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp i

Helper for Lemma 7.3: continuity of each coordinate projection on ℝ^n.

theorem helperForLemma_7_3_coordinate_open_closed_boxes_measurable (n : ℕ) (a b : EuclideanSpace ℝ (Fin n)) : isLebesgueMeasurable n {x : EuclideanSpace ℝ (Fin n) | ∀ (i : Fin n), a.ofLp i < x.ofLp i ∧ x.ofLp i < b.ofLp i} ∧ isLebesgueMeasurable n {x : EuclideanSpace ℝ (Fin n) | ∀ (i : Fin n), a.ofLp i ≤ x.ofLp i ∧ x.ofLp i ≤ b.ofLp i}

Helper for Lemma 7.3: coordinate open boxes and coordinate closed boxes are measurable.

theorem helperForLemma_7_3_outerMeasure_zero_implies_measurable (n : ℕ) (E : Set (EuclideanSpace ℝ (Fin n))) (hE0 : MeasureTheory.volume.toOuterMeasure E = 0) : isLebesgueMeasurable n E

Helper for Lemma 7.3: a set of outer measure zero is Carathéodory-measurable.

theorem measurableSet_properties (n : ℕ) : (∀ (E : Set (EuclideanSpace ℝ (Fin n))), isLebesgueMeasurable n E → isLebesgueMeasurable n Eᶜ) ∧ (∀ (E : Set (EuclideanSpace ℝ (Fin n))) (x : EuclideanSpace ℝ (Fin n)), isLebesgueMeasurable n E → isLebesgueMeasurable n ((fun (y : EuclideanSpace ℝ (Fin n)) => x + y) '' E) ∧ MeasureTheory.volume ((fun (y : EuclideanSpace ℝ (Fin n)) => x + y) '' E) = MeasureTheory.volume E) ∧ (∀ (E₁ E₂ : Set (EuclideanSpace ℝ (Fin n))), isLebesgueMeasurable n E₁ → isLebesgueMeasurable n E₂ → isLebesgueMeasurable n (E₁ ∩ E₂) ∧ isLebesgueMeasurable n (E₁ ∪ E₂)) ∧ (∀ (N : ℕ) (E : Fin N → Set (EuclideanSpace ℝ (Fin n))), (∀ (j : Fin N), isLebesgueMeasurable n (E j)) → isLebesgueMeasurable n (⋃ (j : Fin N), E j) ∧ isLebesgueMeasurable n (⋂ (j : Fin N), E j)) ∧ (∀ (a b : EuclideanSpace ℝ (Fin n)), isLebesgueMeasurable n {x : EuclideanSpace ℝ (Fin n) | ∀ (i : Fin n), a.ofLp i < x.ofLp i ∧ x.ofLp i < b.ofLp i} ∧ isLebesgueMeasurable n {x : EuclideanSpace ℝ (Fin n) | ∀ (i : Fin n), a.ofLp i ≤ x.ofLp i ∧ x.ofLp i ≤ b.ofLp i}) ∧ ∀ (E : Set (EuclideanSpace ℝ (Fin n))), MeasureTheory.volume.toOuterMeasure E = 0 → isLebesgueMeasurable n E

Lemma 7.3 (Properties of measurable sets): (a) complements of measurable sets are measurable; (b) translation preserves measurability and volume; (c) measurable sets are closed under finite unions and intersections of two sets; (d) measurable sets are closed under finite unions and intersections over Fin N; (e) every coordinate open box and coordinate closed box in ℝ^n is measurable; (f) sets of outer measure zero are measurable.

noncomputable def outerMeasureRestrictedMeasure {α : Type u_1} (mStar : MeasureTheory.OuterMeasure α) : MeasureTheory.Measure α

The measure induced by an outer measure on its Carathéodory measurable sets.

Equations

• outerMeasureRestrictedMeasure mStar = mStar.toMeasure ⋯

theorem helperForLemma_7_4_disjoint_with_biUnion_of_finset {α : Type u_1} {J : Type u_2} (E : J → Set α) (hDisj : Pairwise fun (i j : J) => Disjoint (E i) (E j)) (s : Finset J) (i : J) (hi : i ∉ s) : Disjoint (E i) (⋃ j ∈ ↑s, E j)

Helper for Lemma 7.4: one member of a pairwise disjoint family is disjoint from the finite union of all other members indexed by a Finset that does not contain it.

theorem helperForLemma_7_4_outerMeasure_inter_biUnion_finset_eq_sum {α : Type u_1} {J : Type u_2} (mStar : MeasureTheory.OuterMeasure α) (E : J → Set α) (hMeas : ∀ (j : J), mStar.IsCaratheodory (E j)) (hDisj : Pairwise fun (i j : J) => Disjoint (E i) (E j)) (A : Set α) (s : Finset J) : mStar (A ∩ ⋃ j ∈ ↑s, E j) = ∑ j ∈ s, mStar (A ∩ E j)

Helper for Lemma 7.4: finite additivity of an outer measure on intersections with a finite pairwise disjoint family of Carathéodory measurable sets.

theorem helperForLemma_7_4_restricted_measure_biUnion_univ_eq_sum {α : Type u_1} {J : Type u_2} [Fintype J] (mStar : MeasureTheory.OuterMeasure α) (E : J → Set α) (hMeas : ∀ (j : J), mStar.IsCaratheodory (E j)) (hDisj : Pairwise fun (i j : J) => Disjoint (E i) (E j)) : (outerMeasureRestrictedMeasure mStar) (⋃ (j : J), E j) = ∑ j : J, (outerMeasureRestrictedMeasure mStar) (E j)

Helper for Lemma 7.4: finite additivity for the measure induced from an outer measure on its Carathéodory measurable sets.

theorem outerMeasure_finite_additivity {α : Type u_1} {J : Type u_2} [Fintype J] (mStar : MeasureTheory.OuterMeasure α) (E : J → Set α) (hMeas : ∀ (j : J), mStar.IsCaratheodory (E j)) (hDisj : Pairwise fun (i j : J) => Disjoint (E i) (E j)) (A : Set α) : mStar (A ∩ ⋃ (j : J), E j) = ∑ j : J, mStar (A ∩ E j) ∧ (outerMeasureRestrictedMeasure mStar) (⋃ (j : J), E j) = ∑ j : J, (outerMeasureRestrictedMeasure mStar) (E j)

Lemma 7.4 (Finite additivity): for a finite pairwise disjoint family (E_j)_{j ∈ J} of m*-Carathéodory measurable sets, one has m*(A ∩ ⋃ j, E_j) = ∑ j, m*(A ∩ E_j) for every A (equation (7.u101)); in particular, for the restricted measure m induced by m* on m*-measurable sets, m(⋃ j, E_j) = ∑ j, m(E_j) (equation (7.u102)).

theorem measurableSet_diff_and_measure_add_eq_of_subset {α : Type u_1} [MeasurableSpace α] (m : MeasureTheory.Measure α) (A B : Set α) (hA : MeasurableSet A) (hB : MeasurableSet B) (hAB : A ⊆ B) : MeasurableSet (B \ A) ∧ m (B \ A) + m A = m B

Proposition 7.14: in a measure space (X, 𝓜, m), if A, B ∈ 𝓜 and A ⊆ B, then B \ A ∈ 𝓜 and m(B \ A) + m(A) = m(B) (equation (7.u109)).

theorem helperForLemma_7_5_iUnion_isCaratheodory {α : Type u_1} {J : Type u_2} [Countable J] (mStar : MeasureTheory.OuterMeasure α) (E : J → Set α) (hMeas : ∀ (j : J), mStar.IsCaratheodory (E j)) : mStar.IsCaratheodory (⋃ (j : J), E j)

Helper for Lemma 7.5: a countable union of Carathéodory-measurable sets is Carathéodory measurable.

theorem helperForLemma_7_5_pairwise_disjoint_on {α : Type u_1} {J : Type u_2} (E : J → Set α) (hDisj : Pairwise fun (i j : J) => Disjoint (E i) (E j)) : Pairwise (Function.onFun Disjoint E)

Helper for Lemma 7.5: convert pairwise disjointness into the Disjoint on form used by measure_iUnion.

theorem helperForLemma_7_5_restrictedMeasure_iUnion_eq_tsum {α : Type u_1} {J : Type u_2} [Countable J] (mStar : MeasureTheory.OuterMeasure α) (E : J → Set α) (hMeas : ∀ (j : J), mStar.IsCaratheodory (E j)) (hDisj : Pairwise fun (i j : J) => Disjoint (E i) (E j)) : (outerMeasureRestrictedMeasure mStar) (⋃ (j : J), E j) = ∑' (j : J), (outerMeasureRestrictedMeasure mStar) (E j)

Helper for Lemma 7.5: the restricted measure of a countable pairwise disjoint union is the sum of the restricted measures.

theorem outerMeasure_countable_additivity {α : Type u_1} {J : Type u_2} [Countable J] (mStar : MeasureTheory.OuterMeasure α) (E : J → Set α) (hMeas : ∀ (j : J), mStar.IsCaratheodory (E j)) (hDisj : Pairwise fun (i j : J) => Disjoint (E i) (E j)) : mStar.IsCaratheodory (⋃ (j : J), E j) ∧ (outerMeasureRestrictedMeasure mStar) (⋃ (j : J), E j) = ∑' (j : J), (outerMeasureRestrictedMeasure mStar) (E j)

Lemma 7.5 (Countable additivity): for the measure obtained by restricting an outer measure m* to its Carathéodory measurable sets, if (E_j)_{j ∈ J} is a countable pairwise disjoint family of measurable sets, then ⋃ j, E_j is measurable and m(⋃ j, E_j) = ∑' j, m(E_j) (equation (7.u112), independent of enumeration).

theorem outerMeasure_countable_disjoint_union_measurable {α : Type u_1} {J : Type u_2} [Countable J] (mStar : MeasureTheory.OuterMeasure α) (E : J → Set α) (hMeas : ∀ (j : J), mStar.IsCaratheodory (E j)) (hDisj : Pairwise fun (i j : J) => Disjoint (E i) (E j)) : mStar.IsCaratheodory (⋃ (j : J), E j) ∧ (outerMeasureRestrictedMeasure mStar) (⋃ (j : J), E j) = ∑' (j : J), (outerMeasureRestrictedMeasure mStar) (E j)

Lemma 7.6 (countable disjoint union measurable): if m* is an outer measure on X, m is its restriction to m*-measurable sets, and (E_j)_{j ∈ J} is a countable pairwise disjoint family of m*-measurable sets, then E := ⋃ j, E_j is m*-measurable and m(E) = ∑' j, m(E_j) (equation (7.u124)).

theorem measurableSet_iUnion_iInter_of_countable {α : Type u_1} {J : Type u_2} [MeasurableSpace α] [Countable J] (Ω : J → Set α) (hΩ : ∀ (j : J), MeasurableSet (Ω j)) : MeasurableSet (⋃ (j : J), Ω j) ∧ MeasurableSet (⋂ (j : J), Ω j)

Lemma 7.7 ($\sigma$-algebra property): in a measurable space (Ω, 𝓕), for a countable family (Ω_j)_{j ∈ J} with each Ω_j ∈ 𝓕, both ⋃ j, Ω_j and ⋂ j, Ω_j belong to 𝓕.

theorem helperForLemma_7_8_coordinateOpenBox_isOpen_fun (n : ℕ) (a b : Fin n → ℝ) : IsOpen {x : Fin n → ℝ | ∀ (i : Fin n), a i < x i ∧ x i < b i}

Helper for Lemma 7.8: coordinate open boxes in Fin n → ℝ are open.

theorem helperForLemma_7_8_exists_coordinateOpenBox_subset_of_mem_fun (n : ℕ) (E : Set (Fin n → ℝ)) (hE : IsOpen E) {x : Fin n → ℝ} (hx : x ∈ E) : ∃ (a : Fin n → ℝ) (b : Fin n → ℝ), x ∈ {y : Fin n → ℝ | ∀ (i : Fin n), a i < y i ∧ y i < b i} ∧ {y : Fin n → ℝ | ∀ (i : Fin n), a i < y i ∧ y i < b i} ⊆ E

Helper for Lemma 7.8: every point of an open subset of Fin n → ℝ lies in a coordinate open box contained in that open set.

theorem helperForLemma_7_8_eq_iUnion_all_boxes_subset_fun (n : ℕ) (E : Set (Fin n → ℝ)) (hE : IsOpen E) : have I0 := {ab : (Fin n → ℝ) × (Fin n → ℝ) | {x : Fin n → ℝ | ∀ (i : Fin n), ab.1 i < x i ∧ x i < ab.2 i} ⊆ E}; E = ⋃ (k : ↑I0), {x : Fin n → ℝ | ∀ (i : Fin n), (↑k).1 i < x i ∧ x i < (↑k).2 i}

Helper for Lemma 7.8: an open set in Fin n → ℝ is the union of all coordinate open boxes contained in it.

theorem helperForLemma_7_8_countable_subcover_of_all_boxes_fun (n : ℕ) (E : Set (Fin n → ℝ)) (hE : IsOpen E) : ∃ (T : Set ↑{ab : (Fin n → ℝ) × (Fin n → ℝ) | {x : Fin n → ℝ | ∀ (i : Fin n), ab.1 i < x i ∧ x i < ab.2 i} ⊆ E}), T.Countable ∧ E = ⋃ k ∈ T, {x : Fin n → ℝ | ∀ (i : Fin n), (↑k).1 i < x i ∧ x i < (↑k).2 i}

Helper for Lemma 7.8: from the full coordinate-box cover of an open set in Fin n → ℝ, extract a countable subcover.

theorem helperForLemma_7_8_isOpen_eq_iUnion_countable_coordinateOpenBoxes_fun (n : ℕ) (E : Set (Fin n → ℝ)) (hE : IsOpen E) : ∃ (I : Type) (_ : Countable I) (a : I → Fin n → ℝ) (b : I → Fin n → ℝ), E = ⋃ (k : I), {x : Fin n → ℝ | ∀ (i : Fin n), a k i < x i ∧ x i < b k i}

Helper for Lemma 7.8: every open subset of Fin n → ℝ is a union of countably many coordinate open boxes.

theorem isOpen_eq_iUnion_countable_coordinateOpenBoxes (n : ℕ) (E : Set (EuclideanSpace ℝ (Fin n))) (hE : IsOpen E) : ∃ (I : Type) (_ : Countable I) (a : I → Fin n → ℝ) (b : I → Fin n → ℝ), E = ⋃ (k : I), {x : EuclideanSpace ℝ (Fin n) | ∀ (i : Fin n), a k i < x.ofLp i ∧ x.ofLp i < b k i}

Lemma 7.8: if E ⊆ ℝ^n is open in the Euclidean topology, then E is the union of a finite or countable family of coordinate open boxes ∏_{i=1}^n (a_{k,i}, b_{k,i}) (encoded as a countable index type).

theorem isLebesgueMeasurable_of_isOpen_or_isClosed (n : ℕ) : (∀ (E : Set (EuclideanSpace ℝ (Fin n))), IsOpen E → isLebesgueMeasurable n E) ∧ ∀ (E : Set (EuclideanSpace ℝ (Fin n))), IsClosed E → isLebesgueMeasurable n E

Lemma 7.9 (Borel property): every open subset of ℝ^n and every closed subset of ℝ^n is Lebesgue measurable.

theorem isLebesgueMeasurable_and_volume_eq_zero_of_subset_of_volume_eq_zero (n : ℕ) (A B : Set (EuclideanSpace ℝ (Fin n))) (hAB : A ⊆ B) (hBzero : MeasureTheory.volume B = 0) : isLebesgueMeasurable n A ∧ MeasureTheory.volume A = 0

Proposition 7.15: if A ⊆ B ⊆ ℝ^n, B is Lebesgue measurable, and m(B) = 0, then A is Lebesgue measurable and m(A) = 0.

theorem helperForProposition_7_16_rationalFunctionSet_countable_dense : have Qfun := Set.univ.pi fun (x : Fin 2) => Set.range fun (q : ℚ) => ↑q; Qfun.Countable ∧ Dense Qfun

Helper for Proposition 7.16: the rational coordinate cube in Fin 2 → ℝ is countable and dense.

theorem helperForProposition_7_16_rationalGrid_countable_dense_zero_measurable : have Q := {x : EuclideanSpace ℝ (Fin 2) | ∀ (i : Fin 2), x.ofLp i ∈ Set.range fun (q : ℚ) => ↑q}; Q.Countable ∧ Dense Q ∧ MeasureTheory.volume Q = 0 ∧ isLebesgueMeasurable 2 Q

Helper for Proposition 7.16: the rational grid in ℝ^2 is countable, dense, null, and Lebesgue measurable.

theorem helperForProposition_7_16_unitSquare_measurable_volume_one : have U := {x : EuclideanSpace ℝ (Fin 2) | ∀ (i : Fin 2), x.ofLp i ∈ Set.Icc 0 1}; isLebesgueMeasurable 2 U ∧ MeasureTheory.volume U = 1

Helper for Proposition 7.16: the unit square in ℝ^2 is Lebesgue measurable and has volume 1.

theorem helperForProposition_7_16_emptyInterior_from_dense_complement (A Q : Set (EuclideanSpace ℝ (Fin 2))) (hQDense : Dense Q) (hQSubset : Q ⊆ Aᶜ) : interior A = ∅

Helper for Proposition 7.16: if a dense set is contained in Aᶜ, then A has empty interior.

theorem unitSquare_diff_rationalPoints_isLebesgueMeasurable_volume_one_interior_empty : have A := {x : EuclideanSpace ℝ (Fin 2) | ∀ (i : Fin 2), x.ofLp i ∈ Set.Icc 0 1} \ {x : EuclideanSpace ℝ (Fin 2) | ∀ (i : Fin 2), x.ofLp i ∈ Set.range fun (q : ℚ) => ↑q}; isLebesgueMeasurable 2 A ∧ MeasureTheory.volume A = 1 ∧ interior A = ∅

Proposition 7.16: for A := [0,1]^2 \ ℚ^2 = {x ∈ ℝ^2 : (∀ i, 0 ≤ x_i ≤ 1) ∧ (∃ i, x_i ∉ ℚ)}, the set A is Lebesgue measurable, has Lebesgue measure 1, and has empty interior.