Doob-Meyer decomposition theorem #
theorem
ProbabilityTheory.IsLocalSubmartingale.doob_meyer
{ι : Type u_1}
{Ω : Type u_2}
[LinearOrder ι]
[OrderBot ι]
[TopologicalSpace ι]
[OrderTopology ι]
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X : ι → Ω → ℝ}
{𝓕 : MeasureTheory.Filtration ι mΩ}
(hX : IsLocalSubmartingale X 𝓕 P)
(hX_cadlag : ∀ (ω : Ω), IsCadlag fun (x : ι) => X x ω)
:
noncomputable def
ProbabilityTheory.IsLocalSubmartingale.martingalePart
{ι : Type u_1}
{Ω : Type u_2}
[LinearOrder ι]
[OrderBot ι]
[TopologicalSpace ι]
[OrderTopology ι]
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{𝓕 : MeasureTheory.Filtration ι mΩ}
(X : ι → Ω → ℝ)
(hX : IsLocalSubmartingale X 𝓕 P)
(hX_cadlag : ∀ (ω : Ω), IsCadlag fun (x : ι) => X x ω)
:
ι → Ω → ℝ
The local martingale part of the Doob-Meyer decomposition of the local submartingale.
Equations
- ProbabilityTheory.IsLocalSubmartingale.martingalePart X hX hX_cadlag = ⋯.choose
Instances For
noncomputable def
ProbabilityTheory.IsLocalSubmartingale.predictablePart
{ι : Type u_1}
{Ω : Type u_2}
[LinearOrder ι]
[OrderBot ι]
[TopologicalSpace ι]
[OrderTopology ι]
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{𝓕 : MeasureTheory.Filtration ι mΩ}
(X : ι → Ω → ℝ)
(hX : IsLocalSubmartingale X 𝓕 P)
(hX_cadlag : ∀ (ω : Ω), IsCadlag fun (x : ι) => X x ω)
:
ι → Ω → ℝ
The predictable part of the Doob-Meyer decomposition of the local submartingale.
Equations
- ProbabilityTheory.IsLocalSubmartingale.predictablePart X hX hX_cadlag = ⋯.choose
Instances For
theorem
ProbabilityTheory.IsLocalSubmartingale.martingalePart_add_predictablePart
{ι : Type u_1}
{Ω : Type u_2}
[LinearOrder ι]
[OrderBot ι]
[TopologicalSpace ι]
[OrderTopology ι]
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X : ι → Ω → ℝ}
{𝓕 : MeasureTheory.Filtration ι mΩ}
(hX : IsLocalSubmartingale X 𝓕 P)
(hX_cadlag : ∀ (ω : Ω), IsCadlag fun (x : ι) => X x ω)
:
theorem
ProbabilityTheory.IsLocalSubmartingale.isLocalMartingale_martingalePart
{ι : Type u_1}
{Ω : Type u_2}
[LinearOrder ι]
[OrderBot ι]
[TopologicalSpace ι]
[OrderTopology ι]
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X : ι → Ω → ℝ}
{𝓕 : MeasureTheory.Filtration ι mΩ}
(hX : IsLocalSubmartingale X 𝓕 P)
(hX_cadlag : ∀ (ω : Ω), IsCadlag fun (x : ι) => X x ω)
:
IsLocalMartingale (martingalePart X hX hX_cadlag) 𝓕 P
theorem
ProbabilityTheory.IsLocalSubmartingale.cadlag_martingalePart
{ι : Type u_1}
{Ω : Type u_2}
[LinearOrder ι]
[OrderBot ι]
[TopologicalSpace ι]
[OrderTopology ι]
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X : ι → Ω → ℝ}
{𝓕 : MeasureTheory.Filtration ι mΩ}
(hX : IsLocalSubmartingale X 𝓕 P)
(hX_cadlag : ∀ (ω : Ω), IsCadlag fun (x : ι) => X x ω)
(ω : Ω)
:
IsCadlag fun (x : ι) => martingalePart X hX hX_cadlag x ω
theorem
ProbabilityTheory.IsLocalSubmartingale.isPredictable_predictablePart
{ι : Type u_1}
{Ω : Type u_2}
[LinearOrder ι]
[OrderBot ι]
[TopologicalSpace ι]
[OrderTopology ι]
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X : ι → Ω → ℝ}
{𝓕 : MeasureTheory.Filtration ι mΩ}
(hX : IsLocalSubmartingale X 𝓕 P)
(hX_cadlag : ∀ (ω : Ω), IsCadlag fun (x : ι) => X x ω)
:
MeasureTheory.IsPredictable 𝓕 (predictablePart X hX hX_cadlag)
theorem
ProbabilityTheory.IsLocalSubmartingale.cadlag_predictablePart
{ι : Type u_1}
{Ω : Type u_2}
[LinearOrder ι]
[OrderBot ι]
[TopologicalSpace ι]
[OrderTopology ι]
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X : ι → Ω → ℝ}
{𝓕 : MeasureTheory.Filtration ι mΩ}
(hX : IsLocalSubmartingale X 𝓕 P)
(hX_cadlag : ∀ (ω : Ω), IsCadlag fun (x : ι) => X x ω)
(ω : Ω)
:
IsCadlag fun (x : ι) => predictablePart X hX hX_cadlag x ω
theorem
ProbabilityTheory.IsLocalSubmartingale.hasLocallyIntegrableSup_predictablePart
{ι : Type u_1}
{Ω : Type u_2}
[LinearOrder ι]
[OrderBot ι]
[TopologicalSpace ι]
[OrderTopology ι]
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X : ι → Ω → ℝ}
{𝓕 : MeasureTheory.Filtration ι mΩ}
(hX : IsLocalSubmartingale X 𝓕 P)
(hX_cadlag : ∀ (ω : Ω), IsCadlag fun (x : ι) => X x ω)
:
HasLocallyIntegrableSup (predictablePart X hX hX_cadlag) 𝓕 P
theorem
ProbabilityTheory.IsLocalSubmartingale.monotone_predictablePart
{ι : Type u_1}
{Ω : Type u_2}
[LinearOrder ι]
[OrderBot ι]
[TopologicalSpace ι]
[OrderTopology ι]
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X : ι → Ω → ℝ}
{𝓕 : MeasureTheory.Filtration ι mΩ}
(hX : IsLocalSubmartingale X 𝓕 P)
(hX_cadlag : ∀ (ω : Ω), IsCadlag fun (x : ι) => X x ω)
(ω : Ω)
:
Monotone fun (x : ι) => predictablePart X hX hX_cadlag x ω