setIntegral_eq — Mathlib

English

If f is a martingale and c is a real scalar, then c • f is a martingale.

Русский

Если f – мартингал и c – действительное число, то c·f – мартингал.

LaTeX

$$$\\text{Martingale}(c \\cdot f, \\mathcal{F}, \\mu)$$$

Lean4

theorem setIntegral_eq [SigmaFiniteFiltration μ ℱ] (hf : Martingale f ℱ μ) {i j : ι} (hij : i ≤ j) {s : Set Ω}
    (hs : MeasurableSet[ℱ i] s) : ∫ ω in s, f i ω ∂μ = ∫ ω in s, f j ω ∂μ :=
  by
  rw [← setIntegral_condExp (ℱ.le i) (hf.integrable j) hs]
  refine setIntegral_congr_ae (ℱ.le i s hs) ?_
  filter_upwards [hf.2 i j hij] with _ heq _ using heq.symm

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