condExp_sub_nonneg — Mathlib

English

For a submartingale, the a.e. nonnegativity of conditional expectations of increments holds: 0 ≤ μ[f_j − f_i | ℱ_i].

Русский

Для субмартингала верно неотрицательное условное ожидание приращений: 0 ≤ μ[f_j − f_i | ℱ_i].

LaTeX

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

Lean4

theorem condExp_sub_nonneg {f : ι → Ω → ℝ} (hf : Submartingale f ℱ μ) {i j : ι} (hij : i ≤ j) :
    0 ≤ᵐ[μ] μ[f j - f i|ℱ i] := by
  by_cases h : SigmaFinite (μ.trim (ℱ.le i))
  swap; · rw [condExp_of_not_sigmaFinite (ℱ.le i) h]
  refine EventuallyLE.trans ?_ (condExp_sub (hf.integrable _) (hf.integrable _) _).symm.le
  rw [eventually_sub_nonneg, condExp_of_stronglyMeasurable (ℱ.le _) (hf.adapted _) (hf.integrable _)]
  exact hf.2.1 i j hij

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