Doob-Meyer decomposition for submartingales of class DL

ProbabilityTheory.ClassD.doob_meyer gives the Doob-Meyer decomposition of a càdlàg submartingale of class D over an index set with a top element. If the index set has no top element (for example ℝ≥0), the right hypothesis is class DL. We deduce that case from the class D theorem.

For b : ι, the restriction of a class DL submartingale S to Set.Icc ⊥ b is of class D, hence has a Doob-Meyer decomposition S = M' + A' on Set.Icc ⊥ b. Composing with the maps t ↦ min t c for c ≤ b (seen as maps from ι to Set.Icc ⊥ b), we get a decomposition of the increment S (min t b) - S (min t a) on the whole of ι, for all a ≤ b. We then sum these decompositions along a monotone sequence of times tending to infinity: the sum is locally finite.

Main statements

• ProbabilityTheory.ClassDL.doob_meyer: Doob-Meyer decomposition of a càdlàg submartingale of class DL.

theorem ProbabilityTheory.ClassDL.exists_doob_meyer_increment {ι : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [ConditionallyCompleteLinearOrderBot ι] [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] [MeasurableSpace ι] [BorelSpace ι] [MeasureTheory.IsFiniteMeasure P] {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} [𝓕.IsRightContinuous] [𝓕.IsComplete P] (hd : ClassDL S 𝓕 P) (hs : MeasureTheory.Submartingale S 𝓕 P) (hc : ∀ (ω : Ω), IsCadlag fun (x : ι) => S x ω) {a b : ι} (hab : a ≤ b) : ∃ (N : ι → Ω → ℝ) (B : ι → Ω → ℝ), (∀ (t : ι), S (min t b) - S (min t a) = N t + B t) ∧ MeasureTheory.Martingale N 𝓕 P ∧ (∀ (ω : Ω), IsCadlag fun (x : ι) => N x ω) ∧ MeasureTheory.IsStronglyPredictable 𝓕 B ∧ (∀ (ω : Ω), IsCadlag fun (x : ι) => B x ω) ∧ (∀ (ω : Ω), Monotone fun (x : ι) => B x ω) ∧ ∀ t ≤ a, B t = 0

Doob-Meyer decomposition of the increment t ↦ S (min t b) - S (min t a) of a càdlàg submartingale of class DL.

theorem ProbabilityTheory.ClassDL.doob_meyer {ι : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [ConditionallyCompleteLinearOrderBot ι] [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] [MeasurableSpace ι] [BorelSpace ι] [MeasureTheory.IsFiniteMeasure P] {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} [𝓕.IsRightContinuous] [𝓕.IsComplete P] (hd : ClassDL S 𝓕 P) (hs : MeasureTheory.Submartingale S 𝓕 P) (hc : ∀ (ω : Ω), IsCadlag fun (x : ι) => S x ω) : ∃ (M : ι → Ω → ℝ) (A : ι → Ω → ℝ), S = M + A ∧ MeasureTheory.Martingale M 𝓕 P ∧ (∀ (ω : Ω), IsCadlag fun (x : ι) => M x ω) ∧ MeasureTheory.IsStronglyPredictable 𝓕 A ∧ (∀ (ω : Ω), IsCadlag fun (x : ι) => A x ω) ∧ (∀ (ω : Ω), Monotone fun (x : ι) => A x ω) ∧ A ⊥ = 0

Doob–Meyer decomposition of a càdlàg submartingale of class DL.