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 α β)
:
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' := ⋯ }
Instances For
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))
:
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) μ)
: