def MeasureTheory.Filtration.indexComap {ι : Type u_1} {ι' : Type u_2} {Ω : Type u_3} [Preorder ι] [Preorder ι'] {mΩ : MeasurableSpace Ω} (𝓕 : Filtration ι mΩ) {f : ι' → ι} (hf : Monotone f) : Filtration ι' mΩ

Given a filtration on ι and a monotone mapping ι' → ι, construct a filtration on ι'. This is most commonly used to restrict a filtration to a subset of the index set.

Equations

• 𝓕.indexComap hf = { seq := fun (k : ι') => ↑𝓕 (f k), mono' := ⋯, le' := ⋯ }

@[simp]

theorem MeasureTheory.Filtration.indexComap_seq {ι : Type u_1} {ι' : Type u_2} {Ω : Type u_3} [Preorder ι] [Preorder ι'] {mΩ : MeasurableSpace Ω} (𝓕 : Filtration ι mΩ) {f : ι' → ι} (hf : Monotone f) (k : ι') : ↑(𝓕.indexComap hf) k = ↑𝓕 (f k)

instance MeasureTheory.instSigmaFiniteFiltrationIndexComap {ι : Type u_1} {ι' : Type u_2} {Ω : Type u_3} [Preorder ι] [Preorder ι'] {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {f : ι' → ι} (hf : Monotone f) {μ : Measure Ω} [SigmaFiniteFiltration μ 𝓕] : SigmaFiniteFiltration μ (𝓕.indexComap hf)

theorem MeasureTheory.StronglyAdapted.indexComap {ι : Type u_1} {ι' : Type u_2} {Ω : Type u_3} [Preorder ι] [Preorder ι'] {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {f : ι' → ι} {E : Type u_4} [TopologicalSpace E] {X : ι → Ω → E} (hX : StronglyAdapted 𝓕 X) (hf : Monotone f) : StronglyAdapted (𝓕.indexComap hf) (X ∘ f)