Theorems · Theorem · probability

MeasureTheory.Submartingale.sum_smul_sub

∀ {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] {𝒢 : MeasureTheory.Filtration ℕ m0} [CompleteSpace E] [inst_3 : PartialOrder E]
  [IsOrderedModule ℝ E] [ClosedIciTopology E] [IsOrderedAddMonoid E] [MeasureTheory.IsFiniteMeasure μ] {R : ℝ}
  {f : ℕ → Ω → E} {ξ : ℕ → Ω → ℝ},
  MeasureTheory.Submartingale f 𝒢 μ →
    MeasureTheory.StronglyAdapted 𝒢 ξ →
      (∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R) →
        (∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω) →
          MeasureTheory.Submartingale (fun n => ∑ k ∈ Finset.range n, ξ k • (f (k + 1) - f k)) 𝒢 μ

Defined in

Mathlib.Probability.Martingale.Basic

Cited by

2 results in Mathlib

Foundations

Depth 306 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceCompleteSpacePartialOrderIsOrderedModuleClosedIciTopologyIsOrderedAddMonoidMeasureTheory.IsFiniteMeasure