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.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.

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

A filtration 𝓕 is right continuous if 𝓕 t = ⨅ j > i, 𝓕 j = 𝓕 i for all t.

• RC (i : ι) : Prop

  The right continuity property.

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

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 (i : ι) : Prop
• IsComplete ⦃s : Set Ω⦄ (hs : μ s = 0) : MeasurableSet s

  𝓕 ⊥ contains all the null sets.

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

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

def MeasureTheory.Filtration.predictable {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] [OrderBot ι] (𝓕 : Filtration ι m) : MeasurableSpace (ι × Ω)

Given a filtration 𝓕, the predictable σ-algebra is the σ-algebra on ι × Ω generated by sets of the form (t, ∞) × A for t ∈ ι and A ∈ 𝓕 t and {⊥} × A for A ∈ 𝓕 ⊥.

Equations

• One or more equations did not get rendered due to their size.

def MeasureTheory.IsPredictable {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} {E : Type u_3} [TopologicalSpace E] [Preorder ι] [OrderBot ι] (𝓕 : Filtration ι m) (u : ι → Ω → E) : Prop

A process is said to be predictable if it is measurable with respect to the predictable σ-algebra.

Equations

• MeasureTheory.IsPredictable 𝓕 u = MeasureTheory.StronglyMeasurable (Function.uncurry u)

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

Sets of the form (i, j] × A for any A ∈ 𝓕 i are measurable with respect to the predictable σ-algebra.

theorem MeasureTheory.IsPredictable.progMeasurable {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} {E : Type u_3} [TopologicalSpace E] [LinearOrder ι] [OrderBot ι] [MeasurableSpace ι] [TopologicalSpace ι] [OpensMeasurableSpace ι] [OrderClosedTopology ι] [MeasurableSingletonClass ι] [TopologicalSpace.MetrizableSpace E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] {𝓕 : Filtration ι m} {u : ι → Ω → E} (h𝓕 : IsPredictable 𝓕 u) : ProgMeasurable 𝓕 u

A predictable process is progressively measurable.

theorem MeasureTheory.IsPredictable.adapted {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} {E : Type u_3} [TopologicalSpace E] [LinearOrder ι] [OrderBot ι] [MeasurableSpace ι] [TopologicalSpace ι] [OpensMeasurableSpace ι] [OrderClosedTopology ι] [MeasurableSingletonClass ι] [TopologicalSpace.MetrizableSpace E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] {𝓕 : Filtration ι m} {u : ι → Ω → E} (h𝓕 : IsPredictable 𝓕 u) : Adapted 𝓕 u

A predictable process is adapted.

theorem MeasureTheory.IsPredictable.measurableSet_prodMk_add_one_of_predictable {Ω : Type u_1} {m : MeasurableSpace Ω} {𝓕 : Filtration ℕ m} {s : Set (ℕ × Ω)} (hs : MeasurableSet s) (n : ℕ) : MeasurableSet {ω : Ω | (n + 1, ω) ∈ s}

theorem MeasureTheory.IsPredictable.measurable_add_one {Ω : Type u_1} {m : MeasurableSpace Ω} {E : Type u_3} [TopologicalSpace E] [TopologicalSpace.MetrizableSpace E] [MeasurableSpace E] [BorelSpace E] {𝓕 : Filtration ℕ m} {u : ℕ → Ω → E} (h𝓕 : IsPredictable 𝓕 u) (n : ℕ) : Measurable (u (n + 1))

If u is a discrete predictable process, then u (n + 1) is 𝓕 n-measurable.

theorem MeasureTheory.measurableSet_predictable_singleton_prod {Ω : Type u_1} {m : MeasurableSpace Ω} {𝓕 : Filtration ℕ m} {n : ℕ} {s : Set Ω} (hs : MeasurableSet s) : MeasurableSet ({n + 1} ×ˢ s)

theorem MeasureTheory.isPredictable_of_measurable_add_one {Ω : Type u_1} {m : MeasurableSpace Ω} {E : Type u_3} [TopologicalSpace E] [TopologicalSpace.MetrizableSpace E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] {𝓕 : Filtration ℕ m} {u : ℕ → Ω → E} (h₀ : Measurable (u 0)) (h : ∀ (n : ℕ), Measurable (u (n + 1))) : IsPredictable 𝓕 u

theorem MeasureTheory.isPredictable_iff_measurable_add_one {Ω : Type u_1} {m : MeasurableSpace Ω} {E : Type u_3} [TopologicalSpace E] [TopologicalSpace.MetrizableSpace E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] {𝓕 : Filtration ℕ m} {u : ℕ → Ω → E} : IsPredictable 𝓕 u ↔ Measurable (u 0) ∧ ∀ (n : ℕ), Measurable (u (n + 1))

A discrete process u is predictable iff u (n + 1) is 𝓕 n-measurable for all n and u 0 is 𝓕 0-measurable.