theorem
MeasureTheory.Measurable.IndexedPartition
{ι : Type u_1}
{Ω : Type u_2}
{β : Type u_3}
{s : ι → Set Ω}
(hs : _root_.IndexedPartition s)
{mΩ : MeasurableSpace Ω}
{mβ : MeasurableSpace β}
[Countable ι]
(hms : ∀ (i : ι), MeasurableSet (s i))
{f : ι → Ω → β}
(hmf : ∀ (i : ι), Measurable (f i))
:
Measurable (hs.piecewise f)
def
MeasureTheory.SimpleFunc.IndexedPartition
{ι : Type u_1}
{Ω : Type u_2}
{β : Type u_3}
{s : ι → Set Ω}
(hs : _root_.IndexedPartition s)
{mΩ : MeasurableSpace Ω}
[Finite ι]
(hms : ∀ (i : ι), MeasurableSet (s i))
(f : ι → SimpleFunc Ω β)
:
SimpleFunc Ω β
This is the analogue of SimpleFunc.piecewise for IndexedPartition.
Equations
- MeasureTheory.SimpleFunc.IndexedPartition hs hms f = { toFun := hs.piecewise fun (i : ι) => ⇑(f i), measurableSet_fiber' := ⋯, finite_range' := ⋯ }
Instances For
theorem
MeasureTheory.StronglyMeasurable.IndexedPartition
{ι : Type u_1}
{Ω : Type u_2}
{β : Type u_3}
{s : ι → Set Ω}
(hs : _root_.IndexedPartition s)
{mΩ : MeasurableSpace Ω}
[TopologicalSpace β]
[Finite ι]
(hm : ∀ (i : ι), MeasurableSet (s i))
{f : ι → Ω → β}
(hf : ∀ (i : ι), StronglyMeasurable (f i))
:
StronglyMeasurable (hs.piecewise f)
theorem
MeasureTheory.Adapted.progMeasurable_of_rightContinuous
{ι : Type u_1}
{Ω : Type u_2}
{β : Type u_3}
{mΩ : MeasurableSpace Ω}
[TopologicalSpace β]
[TopologicalSpace ι]
[LinearOrder ι]
[OrderTopology ι]
[SecondCountableTopology ι]
[MeasurableSpace ι]
[OpensMeasurableSpace ι]
[TopologicalSpace.PseudoMetrizableSpace β]
{X : ι → Ω → β}
{𝓕 : Filtration ι mΩ}
(h : Adapted 𝓕 X)
(hu_cont : ∀ (ω : Ω), Function.RightContinuous fun (x : ι) => X x ω)
:
ProgMeasurable 𝓕 X