English
Let μ be a finite measure and f: ℕ → Ω → ℝ adapted to a filtration 𝒢. If every f_i is integrable and for all i and all 𝒢_i-measurable sets s we have ∫_s f_i ≤ ∫_s f_{i+1}, then f is a submartingale with respect to 𝒢 and μ.
Русский
Пусть μ является конечной мерой, и f: ℕ → Ω → ℝ адаптирован к 𝒢. Если все f_i интегрируемы и для любых 𝒢_i-измеримых множеств s выполняется ∫_s f_i ≤ ∫_s f_{i+1}, тогда f является субмартингалом относительно 𝒢 и μ.
LaTeX
$$$[IsFiniteMeasure \\ μ] \\Rightarrow (\\text{Adapted } 𝒢 f) \\land (\\forall i, \\text{Integrable}(f_i)\\ μ) \\land (\\forall i,s,\\ MeasurableSet[𝒢 i] s \\to \\int_{s} f_i \\ dμ \\le \\int_{s} f_{i+1} \\ dμ) \\Rightarrow \\text{Submartingale}(f, 𝒢, μ).$$$
Lean4
theorem submartingale_of_setIntegral_le_succ [IsFiniteMeasure μ] {f : ℕ → Ω → ℝ} (hadp : Adapted 𝒢 f)
(hint : ∀ i, Integrable (f i) μ)
(hf : ∀ i, ∀ s : Set Ω, MeasurableSet[𝒢 i] s → ∫ ω in s, f i ω ∂μ ≤ ∫ ω in s, f (i + 1) ω ∂μ) :
Submartingale f 𝒢 μ :=
by
refine submartingale_of_setIntegral_le hadp hint fun i j hij s hs => ?_
induction hij with
| refl => rfl
| step hk₁ hk₂ => exact hk₂.trans (hf _ s (𝒢.mono hk₁ _ hs))
