Predictable σ-algebra

This file defines the predictable σ-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.
• IsStronglyPredictable : A process is predictable if it is measurable with respect to the predictable σ-algebra.

Main results

• IsStronglyPredictable.isStronglyProgressive : A predictable process is progressively measurable.
• IsStronglyPredictable.iff_measurable_add_one : u is a discrete predictable process iff u (n + 1) is 𝓕 n-measurable and u 0 is 𝓕 0-measurable.

Tags

predictable, previsible

@[implicit_reducible]

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.

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

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

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.measurableSet_predictable_singleton_prod {Ω : Type u_1} {m : MeasurableSpace Ω} {𝓕 : Filtration ℕ m} {n : ℕ} {s : Set Ω} (hs : MeasurableSet s) : MeasurableSet ({n + 1} ×ˢ s)

theorem MeasureTheory.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.measurableSpace_le_predictable_of_measurableSet {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] [OrderBot ι] {𝓕 : Filtration ι m} {m' : MeasurableSpace (ι × Ω)} (hm'bot : ∀ (A : Set Ω), MeasurableSet A → MeasurableSet ({⊥} ×ˢ A)) (hm' : ∀ (i : ι) (A : Set Ω), MeasurableSet A → MeasurableSet (Set.Ioi i ×ˢ A)) : 𝓕.predictable ≤ m'

theorem MeasureTheory.measurable_inclusion_predictable {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [LinearOrder ι] [OrderBot ι] [MeasurableSpace ι] [TopologicalSpace ι] [OpensMeasurableSpace ι] [OrderClosedTopology ι] {𝓕 : Filtration ι m} {i : ι} : Measurable fun (x : ↑(Set.Iic i) × Ω) => (↑x.1, x.2)

The inclusion map from [0,i] × Ω with the subtype × 𝓕 i σ-algebra) to ι × Ω with the predictable σ-algebra is measurable

def MeasureTheory.IsStronglyPredictable {Ω : 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.IsStronglyPredictable 𝓕 u = MeasureTheory.StronglyMeasurable (Function.uncurry u)

theorem MeasureTheory.IsStronglyPredictable.isStronglyProgressive {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} {E : Type u_3} [TopologicalSpace E] [LinearOrder ι] [OrderBot ι] [MeasurableSpace ι] [TopologicalSpace ι] [OpensMeasurableSpace ι] [OrderClosedTopology ι] {𝓕 : Filtration ι m} {u : ι → Ω → E} (h𝓕 : IsStronglyPredictable 𝓕 u) : IsStronglyProgressive 𝓕 u

A predictable process is progressively measurable.

theorem MeasureTheory.IsStronglyPredictable.stronglyAdapted {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} {E : Type u_3} [TopologicalSpace E] [LinearOrder ι] [OrderBot ι] [MeasurableSpace ι] [TopologicalSpace ι] [OpensMeasurableSpace ι] [OrderClosedTopology ι] {𝓕 : Filtration ι m} {u : ι → Ω → E} (h𝓕 : IsStronglyPredictable 𝓕 u) : StronglyAdapted 𝓕 u

A predictable process is adapted.

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

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

theorem MeasureTheory.IsStronglyPredictable.of_measurable_add_one {Ω : Type u_1} {m : MeasurableSpace Ω} {E : Type u_3} [TopologicalSpace E] {𝓕 : Filtration ℕ m} {u : ℕ → Ω → E} (h₀ : StronglyMeasurable (u 0)) (h : ∀ (n : ℕ), StronglyMeasurable (u (n + 1))) : IsStronglyPredictable 𝓕 u

theorem MeasureTheory.IsStronglyPredictable.iff_measurable_add_one {Ω : Type u_1} {m : MeasurableSpace Ω} {E : Type u_3} [TopologicalSpace E] {𝓕 : Filtration ℕ m} {u : ℕ → Ω → E} : IsStronglyPredictable 𝓕 u ↔ StronglyMeasurable (u 0) ∧ ∀ (n : ℕ), StronglyMeasurable (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.

@[deprecated MeasureTheory.IsStronglyPredictable.stronglyAdapted (since := "2026-01-05")]

theorem MeasureTheory.Predictable.stronglyAdapted {Ω : Type u_1} {m : MeasurableSpace Ω} {β : Type u_4} [TopologicalSpace β] {f : Filtration ℕ m} {u : ℕ → Ω → β} (hu : StronglyAdapted f fun (n : ℕ) => u (n + 1)) (hu0 : StronglyMeasurable (u 0)) : StronglyAdapted f u

@[deprecated MeasureTheory.IsStronglyPredictable (since := "2026-04-24")]

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

Alias of MeasureTheory.IsStronglyPredictable.

---

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

Equations

• @MeasureTheory.IsPredictable = @MeasureTheory.IsStronglyPredictable

@[deprecated MeasureTheory.IsStronglyPredictable.isStronglyProgressive (since := "2026-04-24")]

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

Alias of MeasureTheory.IsStronglyPredictable.isStronglyProgressive.

---

A predictable process is progressively measurable.

@[deprecated MeasureTheory.IsStronglyPredictable.stronglyAdapted (since := "2026-04-24")]

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

Alias of MeasureTheory.IsStronglyPredictable.stronglyAdapted.

---

A predictable process is adapted.

@[deprecated MeasureTheory.IsStronglyPredictable.measurable_add_one (since := "2026-04-24")]

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

Alias of MeasureTheory.IsStronglyPredictable.measurable_add_one.

---

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

@[deprecated MeasureTheory.IsStronglyPredictable.of_measurable_add_one (since := "2026-04-24")]

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

Alias of MeasureTheory.IsStronglyPredictable.of_measurable_add_one.

@[deprecated MeasureTheory.IsStronglyPredictable.iff_measurable_add_one (since := "2026-04-24")]

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

Alias of MeasureTheory.IsStronglyPredictable.iff_measurable_add_one.

---

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