A nonnegative martingale starting at zero vanishes almost surely

Proved

AvramDividend.Classical.nonnegative_zero_initial_martingale_vanishes_ae

by WillR · Oct 25, 2026 · Mathlib 0df444a (Lean v4.33.1)

avram-dividendmartingaleoptional-stoppingverification-prerequisitezero-origin

A nonnegative real-valued martingale with identically zero initial reward must be zero almost surely at every fixed time. The proof uses the standard sigma-finite filtration martingale equality of integrals, nonnegative zero-integral criterion and integrability of martingales. This exposes why the un-killed discounted scale-function process cannot be used as a martingale at reserve zero for a process with positive increments, and directs the two-sided exit proof toward stopping at ruin.

Preamble

import Mathlib.Probability.Martingale.Basic
import Mathlib.MeasureTheory.Integral.Bochner.Basic

open MeasureTheory
open scoped NNReal

Formal statement

theorem AvramDividend.Classical.nonnegative_zero_initial_martingale_vanishes_ae
    {Ω : Type*} [mΩ : MeasurableSpace Ω]
    {P : Measure Ω} {𝓕 : Filtration ℝ≥0 mΩ}
    [SigmaFiniteFiltration P 𝓕]
    (M : ℝ≥0 → Ω → ℝ)
    (hM : Martingale M 𝓕 P)
    (hnonneg : ∀ t : ℝ≥0, 0 ≤ᵐ[P] M t)
    (hzero : M 0 =ᵐ[P] (fun _ => (0 : ℝ))) :
    ∀ t : ℝ≥0, M t =ᵐ[P] (fun _ => (0 : ℝ)) := by sorry

Source

Pinned Mathlib Martingale.setIntegral_eq and integral_eq_zero_iff_of_nonneg_ae.

View graph