English
Let i ≤ j with a Sigma-finite filtration. For any set s measurable with respect to ℱ_i, the integral of f_j over s is not larger than the integral of f_i over s.
Русский
Пусть i ≤ j и имеется фильтрация с сигма-финитностью. Для любого множества s, измеримого относительно ℱ_i, интеграл f_j по s не больше интеграла f_i по s.
LaTeX
$$$[\Sigma FiniteFiltration \mu \mathcal{F}] \Rightarrow \forall i\le j, \forall s,\ MeasurableSet_{\mathcal{F}_i}(s) \Rightarrow \int_{s} f_j \;d\mu \le \int_{s} f_i \;d\mu$$$
Lean4
theorem setIntegral_le [SigmaFiniteFiltration μ ℱ] {f : ι → Ω → ℝ} (hf : Supermartingale f ℱ μ) {i j : ι} (hij : i ≤ j)
{s : Set Ω} (hs : MeasurableSet[ℱ i] s) : ∫ ω in s, f j ω ∂μ ≤ ∫ ω in s, f i ω ∂μ :=
by
rw [← setIntegral_condExp (ℱ.le i) (hf.integrable j) hs]
refine setIntegral_mono_ae integrable_condExp.integrableOn (hf.integrable i).integrableOn ?_
filter_upwards [hf.2.1 i j hij] with _ heq using heq
