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

noncomputable def MeasureTheory.Filtration.rightCont {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [PartialOrder ι] (𝓕 : Filtration ι m) : Filtration ι m

Given a filtration 𝓕, its right continuation is the filtration 𝓕₊ defined as follows:

• If i is isolated on the right, then 𝓕₊ i := 𝓕 i;
• Otherwise, 𝓕₊ i := ⨅ j > i, 𝓕 j. It is sometimes simply defined as 𝓕₊ i := ⨅ j > i, 𝓕 j when the index type is ℝ. In the general case this is not ideal however. If i is maximal for instance, then 𝓕₊ i = ⊤, which is inconvenient because 𝓕₊ is not a Filtration ι m anymore. If the index type is discrete (such as ℕ), then we would have 𝓕 = 𝓕₊ (i.e. 𝓕 is right-continuous) only if 𝓕 is constant.

To avoid requiring a TopologicalSpace instance on ι in the definition, 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⟩

Equations

• 𝓕.rightCont = { seq := fun (i : ι) => if (nhdsWithin i (Set.Ioi i)).NeBot then ⨅ (j : ι), ⨅ (_ : j > i), ↑𝓕 j else ↑𝓕 i, mono' := ⋯, le' := ⋯ }

def MeasureTheory.Filtration.«term_₊» : Lean.TrailingParserDescr

Given a filtration 𝓕, its right continuation is the filtration 𝓕₊ defined as follows:

• If i is isolated on the right, then 𝓕₊ i := 𝓕 i;
• Otherwise, 𝓕₊ i := ⨅ j > i, 𝓕 j. It is sometimes simply defined as 𝓕₊ i := ⨅ j > i, 𝓕 j when the index type is ℝ. In the general case this is not ideal however. If i is maximal for instance, then 𝓕₊ i = ⊤, which is inconvenient because 𝓕₊ is not a Filtration ι m anymore. If the index type is discrete (such as ℕ), then we would have 𝓕 = 𝓕₊ (i.e. 𝓕 is right-continuous) only if 𝓕 is constant.

To avoid requiring a TopologicalSpace instance on ι in the definition, 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⟩

Equations

• MeasureTheory.Filtration.«term_₊» = Lean.ParserDescr.trailingNode `MeasureTheory.Filtration.«term_₊» 1024 1024 (Lean.ParserDescr.symbol "₊")

theorem MeasureTheory.Filtration.rightCont_def {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [PartialOrder ι] [TopologicalSpace ι] [OrderTopology ι] (𝓕 : Filtration ι m) (i : ι) : ↑𝓕.rightCont i = if (nhdsWithin i (Set.Ioi i)).NeBot then ⨅ (j : ι), ⨅ (_ : j > i), ↑𝓕 j else ↑𝓕 i

theorem MeasureTheory.Filtration.rightCont_eq_of_nhdsGT_eq_bot {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [PartialOrder ι] [TopologicalSpace ι] [OrderTopology ι] (𝓕 : Filtration ι m) {i : ι} (hi : nhdsWithin i (Set.Ioi i) = ⊥) : ↑𝓕.rightCont i = ↑𝓕 i

theorem MeasureTheory.Filtration.rightCont_eq_self {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [LinearOrder ι] [SuccOrder ι] (𝓕 : Filtration ι m) : 𝓕.rightCont = 𝓕

If the index type is a SuccOrder, then 𝓕₊ = 𝓕.

theorem MeasureTheory.Filtration.rightCont_eq_of_isMax {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [PartialOrder ι] (𝓕 : Filtration ι m) {i : ι} (hi : IsMax i) : ↑𝓕.rightCont i = ↑𝓕 i

theorem MeasureTheory.Filtration.rightCont_eq_of_exists_gt {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [LinearOrder ι] (𝓕 : Filtration ι m) {i : ι} (hi : ∃ j > i, Set.Ioo i j = ∅) : ↑𝓕.rightCont i = ↑𝓕 i

theorem MeasureTheory.Filtration.rightCont_eq_of_neBot_nhdsGT {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [PartialOrder ι] [TopologicalSpace ι] [OrderTopology ι] (𝓕 : Filtration ι m) (i : ι) [(nhdsWithin i (Set.Ioi i)).NeBot] : ↑𝓕.rightCont i = ⨅ (j : ι), ⨅ (_ : j > i), ↑𝓕 j

If i is not isolated on the right, then 𝓕₊ i = ⨅ j > i, 𝓕 j. This is for instance the case when ι is a densely ordered linear order with no maximal elements and equipped with the order topology, see rightCont_eq.

theorem MeasureTheory.Filtration.rightCont_eq_of_not_isMax {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [LinearOrder ι] [DenselyOrdered ι] (𝓕 : Filtration ι m) {i : ι} (hi : ¬IsMax i) : ↑𝓕.rightCont i = ⨅ (j : ι), ⨅ (_ : j > i), ↑𝓕 j

theorem MeasureTheory.Filtration.rightCont_eq {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [LinearOrder ι] [DenselyOrdered ι] [NoMaxOrder ι] (𝓕 : Filtration ι m) (i : ι) : ↑𝓕.rightCont i = ⨅ (j : ι), ⨅ (_ : j > i), ↑𝓕 j

If ι is a densely ordered linear order with no maximal elements, then no point is isolated on the right, so that 𝓕₊ i = ⨅ j > i, 𝓕 j holds for all i. This is in particular the case when ι := ℝ≥0.

theorem MeasureTheory.Filtration.le_rightCont {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [PartialOrder ι] (𝓕 : Filtration ι m) : 𝓕 ≤ 𝓕.rightCont

theorem MeasureTheory.Filtration.rightCont_self {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [PartialOrder ι] (𝓕 : Filtration ι m) : 𝓕.rightCont.rightCont = 𝓕.rightCont

class MeasureTheory.Filtration.IsRightContinuous {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [PartialOrder ι] (𝓕 : Filtration ι m) : Prop

A filtration 𝓕 is right continuous if it is equal to its right continuation 𝓕₊.

• RC : 𝓕.rightCont ≤ 𝓕

  The right continuity property.

theorem MeasureTheory.Filtration.IsRightContinuous.eq {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [PartialOrder ι] {𝓕 : Filtration ι m} [h : 𝓕.IsRightContinuous] : 𝓕 = 𝓕.rightCont

theorem MeasureTheory.Filtration.isRightContinuous_rightCont {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [PartialOrder ι] (𝓕 : Filtration ι m) : 𝓕.rightCont.IsRightContinuous

theorem MeasureTheory.Filtration.IsRightContinuous.measurableSet {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [PartialOrder ι] {𝓕 : Filtration ι m} [𝓕.IsRightContinuous] {i : ι} {s : Set Ω} (hs : MeasurableSet s) : MeasurableSet s

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