source
theorem Set.indexedPartition_piecewise_preimage {ι : Type u_1} {Ω : Type u_2} {β : Type u_3} {s : ι → Set Ω} (hs : IndexedPartition s) (f : ι → Ω → β) (t : Set β) :
hs.piecewise f ⁻¹' t = ⋃ (i : ι), s i ∩ f i ⁻¹' t
source
theorem Set.range_indexedPartition_subset {ι : Type u_1} {Ω : Type u_2} {β : Type u_3} {s : ι → Set Ω} (hs : IndexedPartition s) (f : ι → Ω → β) :
range (hs.piecewise f) ⊆ ⋃ (i : ι), range (f i)
source
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)
source
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

source
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)
source
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