Measurability of piecewise functions

In this file, we prove some results about measurability of functions defined by using IndexedPartition.piecewise.

theorem IndexedPartition.measurable_piecewise {ι : Type u_1} {α : Type u_2} {β : Type u_3} [MeasurableSpace α] {s : ι → Set α} {f : ι → α → β} [MeasurableSpace β] [Countable ι] (hs : IndexedPartition s) (hm : ∀ (i : ι), MeasurableSet (s i)) (hf : ∀ (i : ι), Measurable (f i)) : Measurable (hs.piecewise f)

theorem IndexedPartition.aemeasurable_piecewise {ι : Type u_1} {α : Type u_2} {β : Type u_3} [MeasurableSpace α] {s : ι → Set α} {f : ι → α → β} {μ : MeasureTheory.Measure α} [MeasurableSpace β] [Countable ι] (hs : IndexedPartition s) (hm : ∀ (i : ι), MeasurableSet (s i)) (hf : ∀ (i : ι), AEMeasurable (f i) μ) : AEMeasurable (hs.piecewise f) μ

def IndexedPartition.simpleFunc_piecewise {ι : Type u_1} {α : Type u_2} {β : Type u_3} [MeasurableSpace α] {s : ι → Set α} [Finite ι] (hs : IndexedPartition s) (hm : ∀ (i : ι), MeasurableSet (s i)) (f : ι → MeasureTheory.SimpleFunc α β) : MeasureTheory.SimpleFunc α β

This is the analogue of SimpleFunc.piecewise for IndexedPartition.

Equations

• hs.simpleFunc_piecewise hm f = { toFun := hs.piecewise fun (i : ι) => ⇑(f i), measurableSet_fiber' := ⋯, finite_range' := ⋯ }

theorem IndexedPartition.stronglyMeasurable_piecewise {ι : Type u_1} {α : Type u_2} {β : Type u_3} [MeasurableSpace α] {s : ι → Set α} {f : ι → α → β} [Countable ι] (hs : IndexedPartition s) (hm : ∀ (i : ι), MeasurableSet (s i)) [TopologicalSpace β] (hf : ∀ (i : ι), MeasureTheory.StronglyMeasurable (f i)) : MeasureTheory.StronglyMeasurable (hs.piecewise f)

theorem IndexedPartition.aestronglyMeasurable_piecewise {ι : Type u_1} {α : Type u_2} {β : Type u_3} [MeasurableSpace α] {s : ι → Set α} {f : ι → α → β} {μ : MeasureTheory.Measure α} [Countable ι] (hs : IndexedPartition s) (hm : ∀ (i : ι), MeasurableSet (s i)) [TopologicalSpace β] (hf : ∀ (i : ι), MeasureTheory.AEStronglyMeasurable (f i) μ) : MeasureTheory.AEStronglyMeasurable (hs.piecewise f) μ