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.

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 ;_+).

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

A filtration 𝓕 is said to satisfy the usual conditions if it is right continuous and 𝓕 0 and consequently 𝓕 t is complete (i.e. contains all null sets) for all t.

• RC : 𝓕.rightCont ≤ 𝓕
• IsComplete ⦃s : Set Ω⦄ (hs : μ s = 0) : MeasurableSet s

  𝓕 ⊥ contains all the null sets.

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

theorem MeasureTheory.Filtration.HasUsualConditions.measurableSet_of_null {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [PartialOrder ι] [OrderBot ι] (𝓕 : Filtration ι m) {μ : Measure Ω} [u : 𝓕.HasUsualConditions μ] (s : Set Ω) (hs : μ s = 0) : MeasurableSet s