submartingale_of_condExp_sub_nonneg

English

If f is a Submartingale, then for all i ≤ j, the almost everywhere limit of μ[f_j − f_i | ℱ_i] is nonnegative.

Русский

Если f — субмартингал, то для i ≤ j условное ожидание f_j − f_i по ℱ_i неотрицательно почти surely.

LaTeX

$$$\forall i,j, i \le j \Rightarrow 0 \le_{a.e.} \mu[f_j - f_i|\mathcal{F}_i]$$$

Lean4

theorem submartingale_of_condExp_sub_nonneg [SigmaFiniteFiltration μ ℱ] {f : ι → Ω → ℝ} (hadp : Adapted ℱ f)
    (hint : ∀ i, Integrable (f i) μ) (hf : ∀ i j, i ≤ j → 0 ≤ᵐ[μ] μ[f j - f i|ℱ i]) : Submartingale f ℱ μ :=
  by
  refine ⟨hadp, fun i j hij => ?_, hint⟩
  rw [← condExp_of_stronglyMeasurable (ℱ.le _) (hadp _) (hint _), ← eventually_sub_nonneg]
  exact EventuallyLE.trans (hf i j hij) (condExp_sub (hint _) (hint _) _).le

Похожие утверждения