English
Let μ be a finite measure and f: ℕ → Ω → ℝ adapted to 𝒢. If for all i and all 𝒢_i-measurable s we have ∫_s f_i = ∫_s f_{i+1}, then f is a martingale with respect to 𝒢 and μ.
Русский
Пусть μ — конечная мера, f: ℕ → Ω → ℝ адаптирован к 𝒢. Если для всех i и всех 𝒢_i-измеримых множеств s выполняется ∫_s f_i = ∫_s f_{i+1}, то f является мартингалом относительно 𝒢 и μ.
LaTeX
$$$[IsFiniteMeasure \\ μ] \\Rightarrow (Adapted 𝒢 f) \\land (\\forall i, \\text{Integrable}(f_i)\\ μ) \\land (\\forall i,s, MeasurableSet[𝒢 i] s \\to \\int_{s} f_i \\ dμ = \\int_{s} f_{i+1} \\ dμ) \\Rightarrow \\text{Martingale}(f, 𝒢, μ).$$$
Lean4
theorem martingale_of_setIntegral_eq_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) ω ∂μ) : Martingale f 𝒢 μ :=
martingale_iff.2
⟨supermartingale_of_setIntegral_succ_le hadp hint fun i s hs => (hf i s hs).ge,
submartingale_of_setIntegral_le_succ hadp hint fun i s hs => (hf i s hs).le⟩
