Reverse martingale infrastructure (finite horizon)

Reversing time on a finite horizon N turns an antitone family of σ-algebras 𝔽, and its conditional-expectation process n ↦ μ[f | 𝔽 n], into a forward filtration revFiltration on which the conditional-expectation process is a genuine forward martingale (via Mathlib's martingale_condExp). This finite-horizon reversal is the base step of the reverse (Lévy-downward) martingale convergence argument.

Main definitions

• revFiltration: the time-reversed filtration on a finite horizon N (k ↦ 𝔽 (N - k)).
• revCEFinite: the time-reversed conditional-expectation process (n ↦ μ[f | 𝔽 (N - n)]), for a Banach-space-valued f.

Main results

• revCEFinite_martingale: the reversed conditional-expectation process is a forward martingale for revFiltration (the finite-horizon reversal adapter for Mathlib's martingale_condExp).

revFiltration_apply / revCEFinite_apply are the @[simp] defining equations.

Adapted from cameronfreer/exchangeability (Probability/Martingale/Reverse.lean, pin e0532e59ceff23edab44dda9ab0655debbc9cc22). Written Mathlib-shaped for eventual upstreaming.

def MeasureTheory.revFiltration {Ω : Type u_1} {m0 : MeasurableSpace Ω} (𝔽 : ℕ → MeasurableSpace Ω) (h_antitone : Antitone 𝔽) (h_le : ∀ (n : ℕ), 𝔽 n ≤ m0) (N : ℕ) : Filtration ℕ m0

Reverse filtration on a finite horizon N: its level n is 𝔽 (N - n). Used for finite-horizon time reversal of an antitone family 𝔽.

Equations

• MeasureTheory.revFiltration 𝔽 h_antitone h_le N = { seq := fun (n : ℕ) => 𝔽 (N - n), mono' := ⋯, le' := ⋯ }

noncomputable def MeasureTheory.revCEFinite {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : Measure Ω} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : Ω → E) (𝔽 : ℕ → MeasurableSpace Ω) (N n : ℕ) : Ω → E

Reverse conditional-expectation process at finite horizon N: for n ≤ N this is μ[f | 𝔽 (N - n)], for a Banach-space-valued f.

Equations

• MeasureTheory.revCEFinite f 𝔽 N n = μ[f | 𝔽 (N - n)]

@[simp]

theorem MeasureTheory.revCEFinite_apply {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : Measure Ω} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : Ω → E) (𝔽 : ℕ → MeasurableSpace Ω) (N n : ℕ) : revCEFinite f 𝔽 N n = μ[f | 𝔽 (N - n)]

Defining equation for revCEFinite (whose body is deliberately not @[expose]d).

@[simp]

theorem MeasureTheory.revFiltration_apply {Ω : Type u_1} {m0 : MeasurableSpace Ω} (𝔽 : ℕ → MeasurableSpace Ω) (h_antitone : Antitone 𝔽) (h_le : ∀ (n : ℕ), 𝔽 n ≤ m0) (N n : ℕ) : ↑(revFiltration 𝔽 h_antitone h_le N) n = 𝔽 (N - n)

Levels of the reverse filtration: revFiltration 𝔽 … N at n is 𝔽 (N - n).

theorem MeasureTheory.revCEFinite_martingale {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : Measure Ω} {𝔽 : ℕ → MeasurableSpace Ω} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (h_antitone : Antitone 𝔽) (h_le : ∀ (n : ℕ), 𝔽 n ≤ m0) (f : Ω → E) (N : ℕ) [SigmaFiniteFiltration μ (revFiltration 𝔽 h_antitone h_le N)] : Martingale (fun (n : ℕ) => revCEFinite f 𝔽 N n) (revFiltration 𝔽 h_antitone h_le N) μ

Finite-horizon reversal adapter for Mathlib's martingale_condExp: the reversed conditional-expectation process revCEFinite … N is a genuine (forward) martingale for the forward filtration revFiltration 𝔽 … N.