def IsLebesgueMeasurableFunction (n m : ℕ) (Ω : Set (EuclideanSpace ℝ (Fin n))) (f : ↑Ω → EuclideanSpace ℝ (Fin m)) : Prop

Definition 7.6 (Measurable function): let n, m ∈ ℕ, let Ω ⊆ ℝ^n, and let f : Ω → ℝ^m. The function f is (Lebesgue) measurable if for every open set V ⊆ ℝ^m, there exists a Lebesgue measurable set E ⊆ ℝ^n such that the preimage {x ∈ Ω | f x ∈ V} equals Ω ∩ E as a subset of ℝ^n.

Equations

• One or more equations did not get rendered due to their size.

theorem continuous_preimage_borel_nullMeasurable {n m : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))} (hΩ : MeasureTheory.NullMeasurableSet Ω MeasureTheory.volume) {f : ↑Ω → EuclideanSpace ℝ (Fin m)} (hf : Continuous f) (B : Set (EuclideanSpace ℝ (Fin m))) : MeasurableSet B → MeasureTheory.NullMeasurableSet (Subtype.val '' (f ⁻¹' B)) MeasureTheory.volume

Lemma 7.10: if Ω ⊆ ℝ^n is Lebesgue measurable and f : Ω → ℝ^m is continuous for the subspace topology on Ω, then for every Borel set B ⊆ ℝ^m, the set {x ∈ Ω | f x ∈ B} is Lebesgue measurable in ℝ^n.

theorem helperForLemma_7_11_openBox_isOpen {m : ℕ} (a b : Fin m → ℝ) : IsOpen {x : EuclideanSpace ℝ (Fin m) | ∀ (i : Fin m), a i < x.ofLp i ∧ x.ofLp i < b i}

Helper for Lemma 7.11: every coordinate open box in ℝ^m is open.

theorem helperForLemma_7_11_preimageImage_subset {n m : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))} {f : ↑Ω → EuclideanSpace ℝ (Fin m)} (V : Set (EuclideanSpace ℝ (Fin m))) : Subtype.val '' (f ⁻¹' V) ⊆ Ω

Helper for Lemma 7.11: Subtype.val '' (f ⁻¹' V) is always contained in Ω.

theorem helperForLemma_7_11_preimageImage_compl {n m : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))} {f : ↑Ω → EuclideanSpace ℝ (Fin m)} (V : Set (EuclideanSpace ℝ (Fin m))) : Subtype.val '' (f ⁻¹' Vᶜ) = Ω \ Subtype.val '' (f ⁻¹' V)

Helper for Lemma 7.11: complement rule for V ↦ Subtype.val '' (f ⁻¹' V).

theorem helperForLemma_7_11_preimageImage_iUnion {n m : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))} {f : ↑Ω → EuclideanSpace ℝ (Fin m)} (V : ℕ → Set (EuclideanSpace ℝ (Fin m))) : Subtype.val '' (f ⁻¹' ⋃ (i : ℕ), V i) = ⋃ (i : ℕ), Subtype.val '' (f ⁻¹' V i)

Helper for Lemma 7.11: countable union rule for V ↦ Subtype.val '' (f ⁻¹' V).

def helperForLemma_7_11_openBoxFamily (m : ℕ) : Set (Set (EuclideanSpace ℝ (Fin m)))

Helper for Lemma 7.11: full-coordinate open boxes in ℝ^m as a generating family.

Equations

• One or more equations did not get rendered due to their size.

def helperForLemma_7_11_cylinderOpenFamily (m : ℕ) : Set (Set (EuclideanSpace ℝ (Fin m)))

Helper for Lemma 7.11: finite-coordinate open cylinders in ℝ^m form a basis family.

Equations

• One or more equations did not get rendered due to their size.

theorem helperForLemma_7_11_cylinderOpen_isTopologicalBasis {m : ℕ} : TopologicalSpace.IsTopologicalBasis (helperForLemma_7_11_cylinderOpenFamily m)

Helper for Lemma 7.11: finite-coordinate open cylinders are a topological basis on ℝ^m.

theorem helperForLemma_7_11_openBox_refines_cylinder {m : ℕ} {S : Set (EuclideanSpace ℝ (Fin m))} {x : EuclideanSpace ℝ (Fin m)} (hS : S ∈ helperForLemma_7_11_cylinderOpenFamily m) (hx : x ∈ S) : ∃ (a : Fin m → ℝ) (b : Fin m → ℝ), x ∈ {y : EuclideanSpace ℝ (Fin m) | ∀ (i : Fin m), a i < y.ofLp i ∧ y.ofLp i < b i} ∧ {y : EuclideanSpace ℝ (Fin m) | ∀ (i : Fin m), a i < y.ofLp i ∧ y.ofLp i < b i} ⊆ S

Helper for Lemma 7.11: every open cylinder neighborhood contains a full coordinate open box.

theorem helperForLemma_7_11_openBox_isTopologicalBasis {m : ℕ} : TopologicalSpace.IsTopologicalBasis (helperForLemma_7_11_openBoxFamily m)

Helper for Lemma 7.11: full-coordinate open boxes form a topological basis on ℝ^m.

theorem helperForLemma_7_11_isOpen_measurableSet_generateFrom_openBoxes {m : ℕ} {V : Set (EuclideanSpace ℝ (Fin m))} (hV : IsOpen V) : MeasurableSet V

Helper for Lemma 7.11: open sets are measurable for the σ-algebra generated by open boxes.

theorem helperForLemma_7_11_nullMeasurable_preimage_of_generateFrom {n m : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))} {f : ↑Ω → EuclideanSpace ℝ (Fin m)} (hΩ : MeasureTheory.NullMeasurableSet Ω MeasureTheory.volume) (hbox : ∀ (a b : Fin m → ℝ), MeasureTheory.NullMeasurableSet (Subtype.val '' (f ⁻¹' {x : EuclideanSpace ℝ (Fin m) | ∀ (i : Fin m), a i < x.ofLp i ∧ x.ofLp i < b i})) MeasureTheory.volume) (V : Set (EuclideanSpace ℝ (Fin m))) : MeasurableSet V → MeasureTheory.NullMeasurableSet (Subtype.val '' (f ⁻¹' V)) MeasureTheory.volume

Helper for Lemma 7.11: null measurability of preimages extends from open boxes to generated sets.

theorem isLebesgueMeasurableFunction_iff_preimage_openBox_nullMeasurable {n m : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))} {f : ↑Ω → EuclideanSpace ℝ (Fin m)} : MeasureTheory.NullMeasurableSet Ω MeasureTheory.volume → (IsLebesgueMeasurableFunction n m Ω f ↔ ∀ (a b : Fin m → ℝ), MeasureTheory.NullMeasurableSet (Subtype.val '' (f ⁻¹' {x : EuclideanSpace ℝ (Fin m) | ∀ (i : Fin m), a i < x.ofLp i ∧ x.ofLp i < b i})) MeasureTheory.volume)

Lemma 7.11: for Ω ⊆ ℝ^n and f : Ω → ℝ^m, if Ω is Lebesgue measurable, then f is (Lebesgue) measurable if and only if for every open box B = {x | ∀ i, a i < x i ∧ x i < b i} ⊆ ℝ^m, the set f⁻¹(B) is Lebesgue measurable (viewed in ℝ^n as Subtype.val '' (f ⁻¹' B)).