Backward martingale convergence theorem #

This file develops the backward (reverse) martingale convergence theorem: if f : ℕᵒᵈ → Ω → ℝ is a martingale with respect to an antitone filtration ℋ : Filtration ℕᵒᵈ m₀ (i.e. ℋ decreases as the ℕ-index grows), and f (toDual 0) is integrable, then f (toDual n) converges almost everywhere as n → ∞ to a ⨅ n, ℋ (toDual n)-measurable limit.

Structure #

• Martingale (ι := ℕᵒᵈ) API works out of the box because Mathlib's Martingale is Preorder ι-generic (Probability/Martingale/Basic.lean:53). We expose two convenience renames (backwardMartingale_condExp_ae_eq and BackwardMartingale.integrable) tailored to the ℕᵒᵈ shape.
• Backward upcrossing finiteness (BackwardMartingale.upcrossings_ae_lt_top), including the path-reversal combinatorial lemma upcrossingsBefore_le_revPath_succ (see Path-reversal section below).
• L¹ contraction eLpNorm (f n) 1 μ ≤ eLpNorm (f (toDual 0)) 1 μ: backward martingale means f n = 𝔼[f (toDual 0) | ℋ n] (since n ≤ toDual 0 in ℕᵒᵈ), then eLpNorm_one_condExp_le_eLpNorm.
• Main theorem BackwardMartingale.ae_tendsto, chaining off the upcrossing finiteness, the L¹ bound, and tendsto_of_uncrossing_lt_top, with the tail-σ-algebra measurability handled via Filter.limsup_nat_add tail invariance over ⨅ n, ℋ (toDual n).

Proxy machinery #

The upcrossing finiteness and main theorem proofs hinge on lifting a finite-window forward proxy to the global backward sequence. We introduce the proxy infrastructure here:

• reverseProxy N f k ω := f (toDual (N - k)) ω — a forward sequence indexed by k : ℕ whose values along [0, N] are the reverse of f (toDual ·) on [0, N].
• reverseFiltration N ℋ k := ℋ (toDual (N - k)) — the matching forward Filtration ℕ m₀. Since k ↦ N - k is antitone in ℕ and ℋ is monotone in ℕᵒᵈ, the composition is monotone in ℕ.
• reverseProxy_isMartingale — Mathlib forward Martingale for reverseProxy / reverseFiltration, derived from the ℕᵒᵈ martingale equation.

Path-reversal upcrossing inequality (private helper) #

The path-reversal inequality upcrossingsBefore_le_revPath_succ: for any path g : ℕ → Ω → ℝ and any a < b ∈ ℝ, N : ℕ, ω : Ω, upcrossingsBefore a b g N ω ≤ upcrossingsBefore a b (revPath g N) N ω + 1, where revPath g N k ω := g (N - k) ω.

Mathematically: each upcrossing of g corresponds to a "downcrossing" of the reversed path; downcrossings exceed upcrossings by at most 1 (interleaving). The formal proof avoids defining a separate downcrossingsBefore; instead it goes via a witness-chain characterization (upperCrossingTime_le_of_witness), extracts the n Mathlib upcrossing witnesses for g, reverses indices to obtain n - 1 upcrossing witnesses for revPath g N, and translates back via le_csSup. The boundary case τ_0 ≥ 1 is handled by upperCrossingTime_one_pos.

Main definitions / results #

• BackwardMartingale.integrable — Integrable (f n) μ for every n : ℕᵒᵈ.
• backwardMartingale_eq_condExp — f n =ᵐ[μ] 𝔼[f (toDual 0) | ℋ n].
• BackwardMartingale.eLpNorm_one_le — L¹ bound.
• reverseProxy, reverseFiltration, reverseProxy_isMartingale — forward-proxy machinery for the finite-window forward Doob argument.
• BackwardMartingale.upcrossings_ae_lt_top — backward upcrossing finiteness.
• BackwardMartingale.ae_tendsto — the convergence theorem.

Martingale (ι := ℕᵒᵈ) convenience wrappers #

Automatic L¹ boundedness #

Forward proxy for finite-window Doob arguments #

Given a backward martingale f : ℕᵒᵈ → Ω → ℝ w.r.t. ℋ : Filtration ℕᵒᵈ m₀ and a horizon N : ℕ, the reverse proxy is the forward ℕ-indexed sequence

reverseProxy N f k ω := f (toDual (N - k)) ω

with matching filtration reverseFiltration N ℋ k := ℋ (toDual (N - k)). Past k = N both stabilise (since N - k = 0 in ℕ), so the proxy is a genuine Filtration ℕ m₀ and a genuine Martingale (ι := ℕ). This lets us plug the proxy directly into Submartingale.mul_integral_upcrossingsBefore_le_integral_pos_part and other forward-time Doob estimates.

Path-reversal upcrossing inequality (private combinatorial helper) #

For any path g : ℕ → Ω' → ℝ and any a < b ∈ ℝ and N : ℕ, the number of upcrossings of g over [0, N] from a to b is at most one more than the number of upcrossings of the reversed path revPath g N k = g (N - k).

Mathematically: each upcrossing (σ, τ) of g (with g σ ≤ a, g τ ≥ b, σ < τ ≤ N) reverses to a pair (N - τ, N - σ) in revPath g N satisfying (revPath g N)(N - τ) ≥ b, (revPath g N)(N - σ) ≤ a — a downcrossing of the reversed path. Since downcrossings and upcrossings of any path interleave (between any two downcrossings there must be an upcrossing and vice versa), the count of downcrossings exceeds upcrossings by at most 1. Hence the number of upcrossings of g is at most one more than the number of upcrossings of revPath g N.

Mathlib does not provide this combinatorial identity. Our proof factors through two private helpers:

• upperCrossingTime_le_of_witness — from k strictly-alternating upcrossing witnesses (s_i, t_i) strictly inside [0, N), conclude upperCrossingTime a b g N k ω ≤ t_{k-1}. Induction on k using the recursive form of upperCrossingTime and hittingBtwn_le_of_mem.
• upperCrossingTime_one_pos — when 0 < upcrossings, the first upper crossing time upperCrossingTime _ _ g N 1 ω ≥ 1. (If it were 0, then g 0 ω ≥ b and also g 0 ω ≤ a, contradicting a < b.)

Combining them in upcrossingsBefore_revPath_ge: extract the n = k + 1 Mathlib upcrossing witnesses for g, reverse them via t' i := N - upperCrossingTime _ _ g N (k - i) ω, s' i := N - lowerCrossingTime _ _ g N (k - i) ω, apply upperCrossingTime_le_of_witness to revPath g N, then conclude via le_csSup and upperCrossingTime_lt_bddAbove. Total proof ~250 lines including helpers.

Backward upcrossing finiteness (via the path-reversal lemma) #

Backward martingale convergence theorem #