Lemmas about the Doob decomposition

theorem MeasureTheory.predictablePart_add_one {Ω : Type u_1} {E : Type u_2} {mΩ : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {X : ℕ → Ω → E} {𝓕 : Filtration ℕ mΩ} (n : ℕ) : predictablePart X 𝓕 μ (n + 1) = predictablePart X 𝓕 μ n + μ[X (n + 1) - X n|↑𝓕 n]

theorem MeasureTheory.isPredictable_predictablePart {Ω : Type u_1} {E : Type u_2} {mΩ : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {X : ℕ → Ω → E} {𝓕 : Filtration ℕ mΩ} [SecondCountableTopology E] [MeasurableSpace E] [BorelSpace E] : IsPredictable 𝓕 (predictablePart X 𝓕 μ)

theorem MeasureTheory.Submartingale.monotone_predictablePart {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : Measure Ω} {𝓕 : Filtration ℕ mΩ} {X : ℕ → Ω → ℝ} (hX : Submartingale X 𝓕 μ) : ∀ᵐ (ω : Ω) ∂μ, Monotone fun (x : ℕ) => predictablePart X 𝓕 μ x ω