theorem helperForLemma_7_12_isOpen_image_preimage_subtypeVal {m p : ℕ} {W : Set (EuclideanSpace ℝ (Fin m))} (hW : IsOpen W) {g : ↑W → EuclideanSpace ℝ (Fin p)} (hg : Continuous g) {V : Set (EuclideanSpace ℝ (Fin p))} (hV : IsOpen V) : IsOpen (Subtype.val '' (g ⁻¹' V))

Helper for Lemma 7.12: the image under Subtype.val of a continuous preimage of an open set in the subtype codomain is open in the ambient space.

theorem helperForLemma_7_12_comp_preimage_eq_coe_preimage_image {n m p : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))} {W : Set (EuclideanSpace ℝ (Fin m))} {f : ↑Ω → ↑W} {g : ↑W → EuclideanSpace ℝ (Fin p)} (V : Set (EuclideanSpace ℝ (Fin p))) : (fun (x : ↑Ω) => g (f x)) ⁻¹' V = (fun (x : ↑Ω) => ↑(f x)) ⁻¹' (Subtype.val '' (g ⁻¹' V))

Helper for Lemma 7.12: the composition preimage can be rewritten into the preimage form required by IsLebesgueMeasurableFunction.

theorem helperForLemma_7_12_image_preimage_inter_representation {n m p : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))} {W : Set (EuclideanSpace ℝ (Fin m))} {f : ↑Ω → ↑W} {g : ↑W → EuclideanSpace ℝ (Fin p)} {V : Set (EuclideanSpace ℝ (Fin p))} {E : Set (EuclideanSpace ℝ (Fin n))} (hEq : Subtype.val '' ((fun (x : ↑Ω) => ↑(f x)) ⁻¹' (Subtype.val '' (g ⁻¹' V))) = Ω ∩ E) : Subtype.val '' ((fun (x : ↑Ω) => g (f x)) ⁻¹' V) = Ω ∩ E

Helper for Lemma 7.12: once the preimage is rewritten, the representing set identity from hf transfers directly to the composition.

theorem isLebesgueMeasurableFunction_comp_continuous {n m p : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))} {W : Set (EuclideanSpace ℝ (Fin m))} (hW : IsOpen W) {f : ↑Ω → ↑W} (hf : IsLebesgueMeasurableFunction n m Ω fun (x : ↑Ω) => ↑(f x)) {g : ↑W → EuclideanSpace ℝ (Fin p)} (hg : Continuous g) : IsLebesgueMeasurableFunction n p Ω fun (x : ↑Ω) => g (f x)

Lemma 7.12: let Ω ⊆ ℝ^n be measurable, let W ⊆ ℝ^m be open, and let f : Ω → W be measurable. If g : W → ℝ^p is continuous, then the composition g ∘ f : Ω → ℝ^p is measurable.

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

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

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

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

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

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

theorem helperForLemma_7_13_nullMeasurable_preimage_of_measurableSet {n : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))} {f : ↑Ω → ℝ} (hΩ : MeasureTheory.NullMeasurableSet Ω MeasureTheory.volume) (hIoi : ∀ (a : ℝ), MeasureTheory.NullMeasurableSet (Subtype.val '' (f ⁻¹' Set.Ioi a)) MeasureTheory.volume) (V : Set ℝ) : MeasurableSet V → MeasureTheory.NullMeasurableSet (Subtype.val '' (f ⁻¹' V)) MeasureTheory.volume

Helper for Lemma 7.13: null measurability of all superlevel preimages implies null measurability of preimages of all Borel sets.

theorem isLebesgueMeasurableScalarFunction_iff_preimage_Ioi_nullMeasurable {n : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))} {f : ↑Ω → ℝ} : MeasureTheory.NullMeasurableSet Ω MeasureTheory.volume → (IsLebesgueMeasurableScalarFunction n Ω f ↔ ∀ (a : ℝ), MeasureTheory.NullMeasurableSet (Subtype.val '' (f ⁻¹' Set.Ioi a)) MeasureTheory.volume)

Lemma 7.13: let Ω ⊆ ℝ^n be Lebesgue measurable and f : Ω → ℝ. Then f is Lebesgue measurable if and only if for every a : ℝ, the superlevel preimage {x ∈ Ω | a < f x} is Lebesgue measurable in Ω (viewed in ℝ^n via Subtype.val '' (f ⁻¹' Set.Ioi a)).

def IsLebesgueMeasurableExtendedRealFunction (n : ℕ) (Ω : Set (EuclideanSpace ℝ (Fin n))) (f : ↑Ω → EReal) : Prop

Definition 7.7 (Measurable functions in the extended reals): let Ω ⊆ ℝ^n be Lebesgue measurable and let f : Ω → EReal (where EReal = ℝ ∪ {+∞, -∞}). Then f is measurable if for every a : ℝ, the superlevel preimage {x ∈ Ω | f x ∈ (a, +∞]} is Lebesgue measurable in ℝ^n.

Equations

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

theorem helperForLemma_7_14_preimageImage_iSup_Ioi {n : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))} {ι : Type u_1} [Countable ι] (u : ι → ↑Ω → EReal) (a : ℝ) : Subtype.val '' ((fun (x : ↑Ω) => ⨆ (i : ι), u i x) ⁻¹' Set.Ioi ↑a) = ⋃ (i : ι), Subtype.val '' (u i ⁻¹' Set.Ioi ↑a)

Helper for Lemma 7.14: the superlevel preimage of a pointwise iSup is the union of superlevel preimages.

theorem helperForLemma_7_14_preimageImage_iInf_Ioi_rat {n : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))} {ι : Type u_1} [Countable ι] (u : ι → ↑Ω → EReal) (a : ℝ) : Subtype.val '' ((fun (x : ↑Ω) => ⨅ (i : ι), u i x) ⁻¹' Set.Ioi ↑a) = ⋃ (q : { q : ℚ // ↑a < ↑↑q }), Ω ∩ ⋂ (i : ι), Subtype.val '' (u i ⁻¹' Set.Ioi ↑↑↑q)

Helper for Lemma 7.14: the superlevel preimage of a pointwise iInf can be written as a countable union over rational thresholds of countable intersections.

theorem helperForLemma_7_14_isLebesgueMeasurable_iSup_of_superlevel {n : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))} {ι : Type u_1} [Countable ι] (hΩ : MeasureTheory.NullMeasurableSet Ω MeasureTheory.volume) (u : ι → ↑Ω → EReal) (hIoi : ∀ (i : ι) (a : ℝ), MeasureTheory.NullMeasurableSet (Subtype.val '' (u i ⁻¹' Set.Ioi ↑a)) MeasureTheory.volume) : IsLebesgueMeasurableExtendedRealFunction n Ω fun (x : ↑Ω) => ⨆ (i : ι), u i x

Helper for Lemma 7.14: closure of extended-real measurability under countable pointwise iSup.

theorem helperForLemma_7_14_isLebesgueMeasurable_iInf_of_superlevel {n : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))} {ι : Type u_1} [Countable ι] (hΩ : MeasureTheory.NullMeasurableSet Ω MeasureTheory.volume) (u : ι → ↑Ω → EReal) (hIoi : ∀ (i : ι) (a : ℝ), MeasureTheory.NullMeasurableSet (Subtype.val '' (u i ⁻¹' Set.Ioi ↑a)) MeasureTheory.volume) : IsLebesgueMeasurableExtendedRealFunction n Ω fun (x : ↑Ω) => ⨅ (i : ι), u i x

Helper for Lemma 7.14: closure of extended-real measurability under countable pointwise iInf.

theorem helperForLemma_7_14_limsup_nat_rewrite {α : Type u_1} [CompleteLattice α] (u : ℕ → α) : Filter.limsup u Filter.atTop = ⨅ (N : ℕ), ⨆ (k : { m : ℕ // N ≤ m }), u ↑k

Helper for Lemma 7.14: rewrite limsup along ℕ as the tail iInf-iSup formula indexed by subtypes.

theorem helperForLemma_7_14_liminf_nat_rewrite {α : Type u_1} [CompleteLattice α] (u : ℕ → α) : Filter.liminf u Filter.atTop = ⨆ (N : ℕ), ⨅ (k : { m : ℕ // N ≤ m }), u ↑k

Helper for Lemma 7.14: rewrite liminf along ℕ as the tail iSup-iInf formula indexed by subtypes.

theorem isLebesgueMeasurableExtendedRealFunction_iSup_iInf_limsup_liminf {n : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))} {f : ℕ → ↑Ω → EReal} (hf : ∀ (k : ℕ), IsLebesgueMeasurableExtendedRealFunction n Ω (f k)) : (IsLebesgueMeasurableExtendedRealFunction n Ω fun (x : ↑Ω) => ⨆ (k : ℕ), f k x) ∧ (IsLebesgueMeasurableExtendedRealFunction n Ω fun (x : ↑Ω) => ⨅ (k : ℕ), f k x) ∧ (IsLebesgueMeasurableExtendedRealFunction n Ω fun (x : ↑Ω) => ⨅ (N : ℕ), ⨆ (k : { m : ℕ // N ≤ m }), f (↑k) x) ∧ (IsLebesgueMeasurableExtendedRealFunction n Ω fun (x : ↑Ω) => ⨆ (N : ℕ), ⨅ (k : { m : ℕ // N ≤ m }), f (↑k) x) ∧ ∀ (g : ↑Ω → EReal), (∀ (x : ↑Ω), Filter.Tendsto (fun (k : ℕ) => f k x) Filter.atTop (nhds (g x))) → IsLebesgueMeasurableExtendedRealFunction n Ω g

Lemma 7.14 (Limits of measurable functions are measurable): for a measurable set Ω ⊆ ℝ^n and measurable maps f_k : Ω → EReal, the pointwise functions x ↦ ⨆ k, f_k x, x ↦ ⨅ k, f_k x, x ↦ ⨅ N, ⨆ k≥N, f_k x, and x ↦ ⨆ N, ⨅ k≥N, f_k x (cf. (7.u161), (7.u162)) are measurable. In particular, any pointwise limit g of (f_k) is measurable.

theorem aemeasurable_of_eq_outside_nullSet {n : ℕ} {f g : EuclideanSpace ℝ (Fin n) → ℝ} (hf : AEMeasurable f MeasureTheory.volume) (hfg : ∃ (A : Set (EuclideanSpace ℝ (Fin n))), MeasureTheory.volume A = 0 ∧ ∀ x ∉ A, f x = g x) : AEMeasurable g MeasureTheory.volume

Proposition 7.17: let f : ℝ^n → ℝ be Lebesgue measurable, and let g : ℝ^n → ℝ. If there exists a Lebesgue null set A ⊆ ℝ^n such that f x = g x for all x ∈ ℝ^n \ A, then g is Lebesgue measurable.