setIntegral_le — Mathlib

English

If f is a Submartingale, then its positive part f⁺ is also a Submartingale.

Русский

Если f — субмартингал, то его положительная часть f⁺ тоже субмартингал.

LaTeX

$$$\mathrm{Submartingale}(f,\mathcal{F},\mu) \Rightarrow \mathrm{Submartingale}(f^{+},\mathcal{F},\mu)$$$

Lean4

/-- The converse of this lemma is `MeasureTheory.submartingale_of_setIntegral_le`. -/
theorem setIntegral_le [SigmaFiniteFiltration μ ℱ] {f : ι → Ω → ℝ} (hf : Submartingale f ℱ μ) {i j : ι} (hij : i ≤ j)
    {s : Set Ω} (hs : MeasurableSet[ℱ i] s) : ∫ ω in s, f i ω ∂μ ≤ ∫ ω in s, f j ω ∂μ :=
  by
  rw [← neg_le_neg_iff, ← integral_neg, ← integral_neg]
  exact Supermartingale.setIntegral_le hf.neg hij hs

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