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.IsPredictable: A process is predictable if it is measurable with respect to the predictable σ-algebra.
Main results #
IsPredictable.progMeasurable: A predictable process is progressively measurable.isPredictable_iff_measurable_add_one:uis a discrete predictable process iffu (n + 1)is𝓕 n-measurable andu 0is𝓕 0-measurable.
Tags #
predictable, previsible
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
Instances For
def
MeasureTheory.IsPredictable
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
{E : Type u_3}
[TopologicalSpace E]
[Preorder ι]
[OrderBot ι]
(𝓕 : Filtration ι m)
(u : ι → Ω → E)
:
A process is said to be predictable if it is measurable with respect to the predictable σ-algebra.
Equations
Instances For
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.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))
:
theorem
MeasureTheory.IsPredictable.progMeasurable
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
{E : Type u_3}
[TopologicalSpace E]
[LinearOrder ι]
[OrderBot ι]
[MeasurableSpace ι]
[TopologicalSpace ι]
[OpensMeasurableSpace ι]
[OrderClosedTopology ι]
[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 ι]
[TopologicalSpace.MetrizableSpace E]
[MeasurableSpace E]
[BorelSpace E]
[SecondCountableTopology E]
{𝓕 : Filtration ι m}
{u : ι → Ω → E}
(h𝓕 : IsPredictable 𝓕 u)
:
StronglyAdapted 𝓕 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 : ℕ)
:
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}
:
A discrete process u is predictable iff u (n + 1) is 𝓕 n-measurable for all n and
u 0 is 𝓕 0-measurable.