# Doob-Meyer decomposition theorem #

source
theorem ProbabilityTheory.IsLocalSubmartingale.doob_meyer {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} [MeasurableSpace ι] (hX : IsLocalSubmartingale X 𝓕 P) (hX_cadlag : ∀ (ω : Ω), IsCadlag fun (x : ι) => X x ω) :
∃ (M : ι → Ω → ℝ) (A : ι → Ω → ℝ), X = M + A ∧ IsLocalMartingale M 𝓕 P ∧ (∀ (ω : Ω), IsCadlag fun (x : ι) => M x ω) ∧ MeasureTheory.IsPredictable 𝓕 A ∧ (∀ (ω : Ω), IsCadlag fun (x : ι) => A x ω) ∧ HasLocallyIntegrableSup A 𝓕 P ∧ ∀ (ω : Ω), Monotone fun (x : ι) => A x ω
source
noncomputable def ProbabilityTheory.IsLocalSubmartingale.martingalePart {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} [MeasurableSpace ι] (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

source
noncomputable def ProbabilityTheory.IsLocalSubmartingale.predictablePart {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} [MeasurableSpace ι] (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

source
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Ω} [MeasurableSpace ι] (hX : IsLocalSubmartingale X 𝓕 P) (hX_cadlag : ∀ (ω : Ω), IsCadlag fun (x : ι) => X x ω) :
X = martingalePart X hX hX_cadlag + predictablePart X hX hX_cadlag
source
theorem ProbabilityTheory.IsLocalSubmartingale.isLocalMartingale_martingalePart {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} [MeasurableSpace ι] (hX : IsLocalSubmartingale X 𝓕 P) (hX_cadlag : ∀ (ω : Ω), IsCadlag fun (x : ι) => X x ω) :
IsLocalMartingale (martingalePart X hX hX_cadlag) 𝓕 P
source
theorem ProbabilityTheory.IsLocalSubmartingale.cadlag_martingalePart {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} [MeasurableSpace ι] (hX : IsLocalSubmartingale X 𝓕 P) (hX_cadlag : ∀ (ω : Ω), IsCadlag fun (x : ι) => X x ω) (ω : Ω) :
IsCadlag fun (x : ι) => martingalePart X hX hX_cadlag x ω
source
theorem ProbabilityTheory.IsLocalSubmartingale.isPredictable_predictablePart {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} [MeasurableSpace ι] (hX : IsLocalSubmartingale X 𝓕 P) (hX_cadlag : ∀ (ω : Ω), IsCadlag fun (x : ι) => X x ω) :
MeasureTheory.IsPredictable 𝓕 (predictablePart X hX hX_cadlag)
source
theorem ProbabilityTheory.IsLocalSubmartingale.cadlag_predictablePart {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} [MeasurableSpace ι] (hX : IsLocalSubmartingale X 𝓕 P) (hX_cadlag : ∀ (ω : Ω), IsCadlag fun (x : ι) => X x ω) (ω : Ω) :
IsCadlag fun (x : ι) => predictablePart X hX hX_cadlag x ω
source
theorem ProbabilityTheory.IsLocalSubmartingale.hasLocallyIntegrableSup_predictablePart {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} [MeasurableSpace ι] (hX : IsLocalSubmartingale X 𝓕 P) (hX_cadlag : ∀ (ω : Ω), IsCadlag fun (x : ι) => X x ω) :
HasLocallyIntegrableSup (predictablePart X hX hX_cadlag) 𝓕 P
source
theorem ProbabilityTheory.IsLocalSubmartingale.monotone_predictablePart {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} [MeasurableSpace ι] (hX : IsLocalSubmartingale X 𝓕 P) (hX_cadlag : ∀ (ω : Ω), IsCadlag fun (x : ι) => X x ω) (ω : Ω) :
Monotone fun (x : ι) => predictablePart X hX hX_cadlag x ω