English
Let μ be a finite measure and f: ℕ → Ω → ℝ adapted to 𝒢. If for all i and all 𝒢_i-measurable s we have ∫_s f_{i+1} ≤ ∫_s f_i, then f is a supermartingale with respect to 𝒢 and μ.
Русский
Пусть μ — конечная мера, f: ℕ → Ω → ℝ адаптирован к 𝒢. Если для всех i и для всех 𝒢_i-измеримых множества s выполняется ∫_s f_{i+1} ≤ ∫_s f_i, то f — супермартингал относительно 𝒢 и μ.
LaTeX
$$$[IsFiniteMeasure \\ μ] \\Rightarrow (Adapted 𝒢 f) \\land (\\forall i, \\forall s, MeasurableSet[𝒢 i] s \\to \\int_{s} f_{i+1} \\ dμ \\le \\int_{s} f_i \\ dμ) \\Rightarrow \\text{Supermartingale}(f, 𝒢, μ).$$$
Lean4
theorem supermartingale_of_setIntegral_succ_le [IsFiniteMeasure μ] {f : ℕ → Ω → ℝ} (hadp : Adapted 𝒢 f)
(hint : ∀ i, Integrable (f i) μ)
(hf : ∀ i, ∀ s : Set Ω, MeasurableSet[𝒢 i] s → ∫ ω in s, f (i + 1) ω ∂μ ≤ ∫ ω in s, f i ω ∂μ) :
Supermartingale f 𝒢 μ := by
rw [← neg_neg f]
refine (submartingale_of_setIntegral_le_succ hadp.neg (fun i => (hint i).neg) ?_).neg
simpa only [integral_neg, Pi.neg_apply, neg_le_neg_iff]
