theorem convex_comp_martingale_is_submartingale {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {ℱ : MeasureTheory.Filtration ℕ m0} {X : ℕ → Ω → ℝ} (hmart : MeasureTheory.Martingale X ℱ μ) {φ : ℝ → ℝ} (hφ_convex : ConvexOn ℝ Set.univ φ) (hφ_int : ∀ (n : ℕ), MeasureTheory.Integrable (fun (ω : Ω) => φ (X n ω)) μ) : MeasureTheory.Submartingale (fun (n : ℕ) (ω : Ω) => φ (X n ω)) ℱ μ

Convex function of a martingale is a submartingale (Lecture 26/27 claim).

If Xₙ is a martingale w.r.t. the filtration ℱ, and φ : ℝ → ℝ is convex with E|φ(Xₙ)| < ∞ for all n, then φ ∘ Xₙ is a submartingale. The proof uses conditional Jensen's inequality together with the martingale property E[Xⱼ | ℱᵢ] = Xᵢ.