English
If you multiply a process by a nonnegative scalar, the conditional expectations preserve the order, aiding nonnegativity arguments.
Русский
Умножение процесса на неотрицательную константу сохраняет порядок условных ожиданий.
LaTeX
$$$c \ge 0 \Rightarrow (\mu[f_j|\mathcal{F}_i] \le f_i) \Rightarrow (\mu[c f_j|\mathcal{F}_i] \le c f_i)$$$
Lean4
theorem submartingale_of_setIntegral_le [SigmaFiniteFiltration μ ℱ] {f : ι → Ω → ℝ} (hadp : Adapted ℱ f)
(hint : ∀ i, Integrable (f i) μ)
(hf : ∀ i j : ι, i ≤ j → ∀ s : Set Ω, MeasurableSet[ℱ i] s → ∫ ω in s, f i ω ∂μ ≤ ∫ ω in s, f j ω ∂μ) :
Submartingale f ℱ μ := by
refine ⟨hadp, fun i j hij => ?_, hint⟩
suffices f i ≤ᵐ[μ.trim (ℱ.le i)] μ[f j|ℱ i] by exact ae_le_of_ae_le_trim this
suffices 0 ≤ᵐ[μ.trim (ℱ.le i)] μ[f j|ℱ i] - f i
by
filter_upwards [this] with x hx
rwa [← sub_nonneg]
refine
ae_nonneg_of_forall_setIntegral_nonneg
((integrable_condExp.sub (hint i)).trim _ (stronglyMeasurable_condExp.sub <| hadp i)) fun s hs _ => ?_
specialize hf i j hij s hs
rwa [← setIntegral_trim _ (stronglyMeasurable_condExp.sub <| hadp i) hs,
integral_sub' integrable_condExp.integrableOn (hint i).integrableOn, sub_nonneg,
setIntegral_condExp (ℱ.le i) (hint j) hs]
