Progressively Measurable σ-algebra

This file defines the progressively measurable σ-algebra associated to a filtration, as well as the notion of predictable processes. We prove that predictable processes are progressively measurable and adapted. We also give an equivalent characterization of predictability for discrete processes.

Main definitions

• Filtration.rightCont: The right continuation of a filtration.
• Filtration.Predictable: The predictable σ-algebra associated to a filtration.
• Filtration.IsPredictable: A process is predictable if it is measurable with respect to the predictable σ-algebra.

Main results

• Filtration.IsPredictable.progMeasurable: A predictable process is progressively measurable.
• Filtration.IsPredictable.measurable_succ: u is a discrete predictable process iff u (n + 1) is 𝓕 n-measurable and u 0 is 𝓕 0-measurable.
• MeasureTheory.StronglyAdapted.isPredictable_of_leftContinuous: A left-continuous adapted process is predictable if the index set is DenselyOrdered.

Implementation note

To avoid requiring a TopologicalSpace instance on ι in the definition of rightCont, we endow ι with the order topology Preorder.topology inside the definition. Say you write a statement about 𝓕₊ which does not require a TopologicalSpace structure on ι, but you wish to use a statement which requires a topology (such as rightCont_def). Then you can endow ι with the order topology by writing

  letI := Preorder.topology ι
  haveI : OrderTopology ι := ⟨rfl⟩

Notation

• Given a filtration 𝓕, its right continuation is denoted 𝓕₊ (type ₊ with ;_+).

theorem MeasureTheory.measurableSet_predictable_univ_prod {ι : Type u_1} [LinearOrder ι] [OrderBot ι] {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {s : Set Ω} (hs : MeasurableSet s) : MeasurableSet (Set.univ ×ˢ s)

theorem MeasureTheory.measurableSet_predictable_Iic_prod {ι : Type u_1} [LinearOrder ι] [OrderBot ι] {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {s : Set Ω} (hs : MeasurableSet s) {i : ι} : MeasurableSet (Set.Iic i ×ˢ s)

theorem MeasureTheory.StronglyAdapted.isStronglyPredictable_of_leftContinuous {ι : Type u_1} [LinearOrder ι] [OrderBot ι] {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {β : Type u_3} [TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] {X : ι → Ω → β} [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] [DenselyOrdered ι] (h_adap : StronglyAdapted 𝓕 X) (h_cont : ∀ (ω : Ω) (a : ι), ContinuousWithinAt (fun (x : ι) => X x ω) (Set.Iio a) a) : IsStronglyPredictable 𝓕 X

class MeasureTheory.Filtration.IsComplete {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [PartialOrder ι] (𝓕 : Filtration ι m) (μ : Measure Ω := by volume_tac) : Prop

A filtration 𝓕 is complete with respect to a measure μ if for all i, 𝓕 i contains all the μ-null sets.

• measurableSet_of_null ⦃s : Set Ω⦄ (hs : μ s = 0) (t : ι) : MeasurableSet s

  𝓕 ⊥ contains all the null sets.

instance MeasureTheory.Filtration.instIsCompleteTrimOfIsComplete {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [PartialOrder ι] {𝓕 : Filtration ι m} {μ : Measure Ω} [u : 𝓕.IsComplete μ] {i : ι} : (μ.trim ⋯).IsComplete