Properties of martingales and submartingales #

This file contains auxiliary results about martingales and submartingales that are not yet in Mathlib.

Main statements #

Martingale.indicator: the product of a martingale with the indicator of a set that is measurable with respect to the first σ-algebra of the filtration is a martingale.
Martingale.indexComap, Submartingale.indexComap: reindexing a (sub)martingale along a monotone map gives a (sub)martingale with respect to the filtration Filtration.indexComap.
Martingale.submartingale_convex_comp: the composition of a martingale with a continuous convex function is a submartingale.
Martingale.submartingale_norm: the norm of a martingale is a submartingale.
Submartingale.monotone_convex_comp: the composition of a submartingale with a monotone continuous convex function is a submartingale.

theorem MeasureTheory.Martingale.stronglyMeasurable' {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [Preorder ι] [NormedAddCommGroup E] [NormedSpace ℝ E] {mΩ : MeasurableSpace Ω} {P : Measure Ω} {X : ι → Ω → E} {𝓕 : Filtration ι mΩ} (hX : Martingale X 𝓕 P) {t : ι} :

Each X t of a martingale X is strongly measurable with respect to the ambient σ-algebra.

theorem MeasureTheory.Martingale.indicator {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [Preorder ι] [NormedAddCommGroup E] [NormedSpace ℝ E] {mΩ : MeasurableSpace Ω} {P : Measure Ω} {X : ι → Ω → E} {𝓕 : Filtration ι mΩ} [CompleteSpace E] [OrderBot ι] {s : Set Ω} (hX : Martingale X 𝓕 P) (hs : MeasurableSet s) :

Martingale (fun (t : ι) => s.indicator (X t)) 𝓕 P

The indicator of a 𝓕 ⊥-measurable set times a martingale is a martingale.

theorem MeasureTheory.Martingale.indexComap {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [Preorder ι] [NormedAddCommGroup E] [NormedSpace ℝ E] {mΩ : MeasurableSpace Ω} {P : Measure Ω} {X : ι → Ω → E} {𝓕 : Filtration ι mΩ} {ι' : Type u_4} [Preorder ι'] {f : ι' → ι} (hX : Martingale X 𝓕 P) (hf : Monotone f) :

A martingale reindexed by a monotone map is a martingale for the reindexed filtration.

theorem MeasureTheory.Submartingale.indexComap {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [Preorder ι] [NormedAddCommGroup E] [NormedSpace ℝ E] {mΩ : MeasurableSpace Ω} {P : Measure Ω} {X : ι → Ω → E} {𝓕 : Filtration ι mΩ} {ι' : Type u_4} [Preorder ι'] {f : ι' → ι} [LE E] (hX : Submartingale X 𝓕 P) (hf : Monotone f) :

A submartingale reindexed by a monotone map is a submartingale for the reindexed filtration.

theorem MeasureTheory.Martingale.submartingale_convex_comp {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [Preorder ι] [NormedAddCommGroup E] [NormedSpace ℝ E] {mΩ : MeasurableSpace Ω} {P : Measure Ω} {X : ι → Ω → E} {𝓕 : Filtration ι mΩ} [CompleteSpace E] [SigmaFiniteFiltration P 𝓕] {φ : E → ℝ} (hX : Martingale X 𝓕 P) (hφ_cvx : ConvexOn ℝ Set.univ φ) (hφ_cont : Continuous φ) (hφ_int : ∀ (t : ι), Integrable (fun (ω : Ω) => φ (X t ω)) P) :

Submartingale (fun (t : ι) (ω : Ω) => φ (X t ω)) 𝓕 P

The composition of a martingale with a continuous convex function is a submartingale.

Submartingale (fun (t : ι) (ω : Ω) => ‖X t ω‖) 𝓕 P

The norm of a martingale is a submartingale.

theorem MeasureTheory.Submartingale.monotone_convex_comp {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [Preorder ι] [NormedAddCommGroup E] [NormedSpace ℝ E] {mΩ : MeasurableSpace Ω} {P : Measure Ω} {X : ι → Ω → E} {𝓕 : Filtration ι mΩ} [CompleteSpace E] [SigmaFiniteFiltration P 𝓕] {φ : E → ℝ} [Preorder E] (hX : Submartingale X 𝓕 P) (hφ_mono : Monotone φ) (hφ_cvx : ConvexOn ℝ Set.univ φ) (hφ_cont : Continuous φ) (hφ_int : ∀ (t : ι), Integrable (fun (ω : Ω) => φ (X t ω)) P) :

Submartingale (fun (t : ι) (ω : Ω) => φ (X t ω)) 𝓕 P

The composition of a submartingale with a monotone continuous convex function is a submartingale.