5. Stochastic Processes and Martingales🔗

5.1. Stochastic processes, filtrations, and martingales🔗

We define a measure space Ω, with a probability mesure P : Measure Ω.

variable {Ω : Type*} {mΩ : MeasurableSpace Ω}
  {P : Measure Ω} [IsProbabilityMeasure P]

Let then X be a stochastic process indexed by ℕ: a function ℕ → Ω → E. Here E is a Banach space, a complete normed space (that's what the martingale property needs). We will often need a measurability condition on X in lemmas, but we don't add it yet.

variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
  {mE : MeasurableSpace E} {X : ℕ → Ω → E}

A filtration is a monotone family of sub-σ-algebras indexed by ℕ.

variable {𝓕 : Filtration ℕ mΩ}

example : ∀ n, 𝓕 n ≤ mΩ := Filtration.le 𝓕

example {i j : ℕ} (hij : i ≤ j) : 𝓕 i ≤ 𝓕 j := Filtration.mono 𝓕 hij

If X is a martingale, then it is adapted to the filtration, which means that for all n, X n is (strongly) measurable with respect to 𝓕 n.

example (hX : Martingale X 𝓕 P) : StronglyAdapted 𝓕 X := hX.stronglyAdapted

example (hX : Martingale X 𝓕 P) (n : ℕ) : StronglyMeasurable[𝓕 n] (X n) := hX.stronglyAdapted n

example [BorelSpace E] (hX : Martingale X 𝓕 P) (n : ℕ) : Measurable[𝓕 n] (X n) :=
  (hX.stronglyAdapted n).measurable

/-- A martingale satisfies the following equality: for all `i ≤ j`, the conditional expectation of
`X j` with respect to `𝓕 i` is equal to `X i`. -/
example (hX : Martingale X 𝓕 P) {i j : ℕ} (hij : i ≤ j) : P[X j | 𝓕 i] =ᵐ[P] X i :=
  hX.condExp_ae_eq hij

/-- For a submartingale, the conditional expectation of `Y j` with respect to `𝓕 i` is greater than
or equal to `Y i`. -/
example {Y : ℕ → Ω → ℝ} (hX : Submartingale Y 𝓕 P) {i j : ℕ} (hij : i ≤ j) :
    Y i ≤ᵐ[P] P[Y j | 𝓕 i] :=
  hX.ae_le_condExp hij

Almost everywhere martingale convergence theorem: An L¹-bounded submartingale converges almost everywhere to a ⨆ n, ℱ n-measurable function.

theorem ae_tendsto_limitProcess {Y : ℕ → Ω → ℝ} (hY : Submartingale Y 𝓕 P)
    {R : ℝ≥0} (hbdd : ∀ n, eLpNorm (Y n) 1 P ≤ R) :
    ∀ᵐ ω ∂P, Tendsto (Y · ω) atTop (𝓝 (𝓕.limitProcess Y P ω)) := byΩ:Type u_1mΩ:MeasurableSpace ΩP:Measure Ωinst✝:IsProbabilityMeasure P𝓕:Filtration ℕ mΩY:ℕ → Ω → ℝhY:Submartingale Y 𝓕 PR:ℝ≥0hbdd:∀ (n : ℕ), eLpNorm (Y n) 1 P ≤ ↑R⊢ ∀ᵐ (ω : Ω) ∂P, Tendsto (fun x => Y x ω) atTop (𝓝 (Filtration.limitProcess Y 𝓕 P ω))
  classical
  suffices ∃ g, StronglyMeasurable[⨆ n, 𝓕 n] g ∧ ∀ᵐ ω ∂P, Tendsto (Y · ω) atTop (𝓝 (g ω)) byΩ:Type u_1mΩ:MeasurableSpace ΩP:Measure Ωinst✝:IsProbabilityMeasure P𝓕:Filtration ℕ mΩY:ℕ → Ω → ℝhY:Submartingale Y 𝓕 PR:ℝ≥0hbdd:∀ (n : ℕ), eLpNorm (Y n) 1 P ≤ ↑Rthis:∃ g, StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂P, Tendsto (fun x => Y x ω) atTop (𝓝 (g ω))⊢ ∀ᵐ (ω : Ω) ∂P, Tendsto (fun x => Y x ω) atTop (𝓝 (Filtration.limitProcess Y 𝓕 P ω))
    rw [Filtration.limitProcess, dif_pos this]Ω:Type u_1mΩ:MeasurableSpace ΩP:Measure Ωinst✝:IsProbabilityMeasure P𝓕:Filtration ℕ mΩY:ℕ → Ω → ℝhY:Submartingale Y 𝓕 PR:ℝ≥0hbdd:∀ (n : ℕ), eLpNorm (Y n) 1 P ≤ ↑Rthis:∃ g, StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂P, Tendsto (fun x => Y x ω) atTop (𝓝 (g ω))⊢ ∀ᵐ (ω : Ω) ∂P, Tendsto (fun x => Y x ω) atTop (𝓝 (Classical.choose this ω))
    exact (Classical.choose_spec this).2All goals completed! 🐙
  set g' : Ω → ℝ := fun ω ↦ if h : ∃ c, Tendsto (Y · ω) atTop (𝓝 c) then h.choose else 0Ω:Type u_1mΩ:MeasurableSpace ΩP:Measure Ωinst✝:IsProbabilityMeasure P𝓕:Filtration ℕ mΩY:ℕ → Ω → ℝhY:Submartingale Y 𝓕 PR:ℝ≥0hbdd:∀ (n : ℕ), eLpNorm (Y n) 1 P ≤ ↑Rg':Ω → ℝ := fun ω => if h : ∃ c, Tendsto (fun x => Y x ω) atTop (𝓝 c) then h.choose else 0⊢ ∃ g, StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂P, Tendsto (fun x => Y x ω) atTop (𝓝 (g ω))
  have hle : ⨆ n, 𝓕 n ≤ mΩ := sSup_le fun m ⟨n, hn⟩ ↦ hn ▸ 𝓕.le _Ω:Type u_1mΩ:MeasurableSpace ΩP:Measure Ωinst✝:IsProbabilityMeasure P𝓕:Filtration ℕ mΩY:ℕ → Ω → ℝhY:Submartingale Y 𝓕 PR:ℝ≥0hbdd:∀ (n : ℕ), eLpNorm (Y n) 1 P ≤ ↑Rg':Ω → ℝ := fun ω => if h : ∃ c, Tendsto (fun x => Y x ω) atTop (𝓝 c) then h.choose else 0hle:⨆ n, ↑𝓕 n ≤ mΩ⊢ ∃ g, StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂P, Tendsto (fun x => Y x ω) atTop (𝓝 (g ω))
  have hg' : ∀ᵐ ω ∂P.trim hle, Tendsto (Y · ω) atTop (𝓝 (g' ω)) := byΩ:Type u_1mΩ:MeasurableSpace ΩP:Measure Ωinst✝:IsProbabilityMeasure P𝓕:Filtration ℕ mΩY:ℕ → Ω → ℝhY:Submartingale Y 𝓕 PR:ℝ≥0hbdd:∀ (n : ℕ), eLpNorm (Y n) 1 P ≤ ↑R⊢ ∀ᵐ (ω : Ω) ∂P, Tendsto (fun x => Y x ω) atTop (𝓝 (Filtration.limitProcess Y 𝓕 P ω))
    filter_upwards [hY.exists_ae_trim_tendsto_of_bdd hbdd] with ω hωhΩ:Type u_1mΩ:MeasurableSpace ΩP:Measure Ωinst✝:IsProbabilityMeasure P𝓕:Filtration ℕ mΩY:ℕ → Ω → ℝhY:Submartingale Y 𝓕 PR:ℝ≥0hbdd:∀ (n : ℕ), eLpNorm (Y n) 1 P ≤ ↑Rg':Ω → ℝ := fun ω => if h : ∃ c, Tendsto (fun x => Y x ω) atTop (𝓝 c) then h.choose else 0hle:⨆ n, ↑𝓕 n ≤ mΩω:Ωhω:∃ c, Tendsto (fun n => Y n ω) atTop (𝓝 c)⊢ Tendsto (fun x => Y x ω) atTop (𝓝 (g' ω))
    simp_rw [hΩ:Type u_1mΩ:MeasurableSpace ΩP:Measure Ωinst✝:IsProbabilityMeasure P𝓕:Filtration ℕ mΩY:ℕ → Ω → ℝhY:Submartingale Y 𝓕 PR:ℝ≥0hbdd:∀ (n : ℕ), eLpNorm (Y n) 1 P ≤ ↑Rg':Ω → ℝ := fun ω => if h : ∃ c, Tendsto (fun x => Y x ω) atTop (𝓝 c) then h.choose else 0hle:⨆ n, ↑𝓕 n ≤ mΩω:Ωhω:∃ c, Tendsto (fun n => Y n ω) atTop (𝓝 c)⊢ Tendsto (fun x => Y x ω) atTop (𝓝 (g' ω))g', dif_pos hω]
    exact hω.choose_specAll goals completed! 🐙
  have hg'm : AEStronglyMeasurable[⨆ n, 𝓕 n] g' (P.trim hle) :=
    (@aemeasurable_of_tendsto_metrizable_ae' _ _ (⨆ n, 𝓕 n) _ _ _ _ _ _ _
      (fun n ↦ ((hY.stronglyMeasurable n).measurable.mono (le_sSup ⟨n, rfl⟩ : 𝓕 n ≤ ⨆ n, 𝓕 n)
        le_rfl).aemeasurable) hg').aestronglyMeasurableΩ:Type u_1mΩ:MeasurableSpace ΩP:Measure Ωinst✝:IsProbabilityMeasure P𝓕:Filtration ℕ mΩY:ℕ → Ω → ℝhY:Submartingale Y 𝓕 PR:ℝ≥0hbdd:∀ (n : ℕ), eLpNorm (Y n) 1 P ≤ ↑Rg':Ω → ℝ := fun ω => if h : ∃ c, Tendsto (fun x => Y x ω) atTop (𝓝 c) then h.choose else 0hle:⨆ n, ↑𝓕 n ≤ mΩhg':∀ᵐ (ω : Ω) ∂P.trim hle, Tendsto (fun x => Y x ω) atTop (𝓝 (g' ω))hg'm:AEStronglyMeasurable g' (P.trim hle)⊢ ∃ g, StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂P, Tendsto (fun x => Y x ω) atTop (𝓝 (g ω))
  obtain ⟨g, hgm, hae⟩ := hg'mΩ:Type u_1mΩ:MeasurableSpace ΩP:Measure Ωinst✝:IsProbabilityMeasure P𝓕:Filtration ℕ mΩY:ℕ → Ω → ℝhY:Submartingale Y 𝓕 PR:ℝ≥0hbdd:∀ (n : ℕ), eLpNorm (Y n) 1 P ≤ ↑Rg':Ω → ℝ := fun ω => if h : ∃ c, Tendsto (fun x => Y x ω) atTop (𝓝 c) then h.choose else 0hle:⨆ n, ↑𝓕 n ≤ mΩhg':∀ᵐ (ω : Ω) ∂P.trim hle, Tendsto (fun x => Y x ω) atTop (𝓝 (g' ω))g:Ω → ℝhgm:StronglyMeasurable ghae:g' =ᶠ[ae (P.trim hle)] g⊢ ∃ g, StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂P, Tendsto (fun x => Y x ω) atTop (𝓝 (g ω))
  have hg : ∀ᵐ ω ∂P.trim hle, Tendsto (Y · ω) atTop (𝓝 (g ω)) := byΩ:Type u_1mΩ:MeasurableSpace ΩP:Measure Ωinst✝:IsProbabilityMeasure P𝓕:Filtration ℕ mΩY:ℕ → Ω → ℝhY:Submartingale Y 𝓕 PR:ℝ≥0hbdd:∀ (n : ℕ), eLpNorm (Y n) 1 P ≤ ↑R⊢ ∀ᵐ (ω : Ω) ∂P, Tendsto (fun x => Y x ω) atTop (𝓝 (Filtration.limitProcess Y 𝓕 P ω))
    filter_upwards [hae, hg'] with ω hωhΩ:Type u_1mΩ:MeasurableSpace ΩP:Measure Ωinst✝:IsProbabilityMeasure P𝓕:Filtration ℕ mΩY:ℕ → Ω → ℝhY:Submartingale Y 𝓕 PR:ℝ≥0hbdd:∀ (n : ℕ), eLpNorm (Y n) 1 P ≤ ↑Rg':Ω → ℝ := fun ω => if h : ∃ c, Tendsto (fun x => Y x ω) atTop (𝓝 c) then h.choose else 0hle:⨆ n, ↑𝓕 n ≤ mΩhg':∀ᵐ (ω : Ω) ∂P.trim hle, Tendsto (fun x => Y x ω) atTop (𝓝 (g' ω))g:Ω → ℝhgm:StronglyMeasurable ghae:g' =ᶠ[ae (P.trim hle)] gω:Ωhω:g' ω = g ω⊢ Tendsto (fun x => Y x ω) atTop (𝓝 (g' ω)) → Tendsto (fun x => Y x ω) atTop (𝓝 (g ω)) hg'ωhΩ:Type u_1mΩ:MeasurableSpace ΩP:Measure Ωinst✝:IsProbabilityMeasure P𝓕:Filtration ℕ mΩY:ℕ → Ω → ℝhY:Submartingale Y 𝓕 PR:ℝ≥0hbdd:∀ (n : ℕ), eLpNorm (Y n) 1 P ≤ ↑Rg':Ω → ℝ := fun ω => if h : ∃ c, Tendsto (fun x => Y x ω) atTop (𝓝 c) then h.choose else 0hle:⨆ n, ↑𝓕 n ≤ mΩhg':∀ᵐ (ω : Ω) ∂P.trim hle, Tendsto (fun x => Y x ω) atTop (𝓝 (g' ω))g:Ω → ℝhgm:StronglyMeasurable ghae:g' =ᶠ[ae (P.trim hle)] gω:Ωhω:g' ω = g ωhg'ω:Tendsto (fun x => Y x ω) atTop (𝓝 (g' ω))⊢ Tendsto (fun x => Y x ω) atTop (𝓝 (g ω)) using hω ▸ hg'ω
  exact ⟨g, hgm, measure_eq_zero_of_trim_eq_zero hle hg⟩All goals completed! 🐙

5.2. Stopping times🔗

A stopping time with respect to a filtration indexed by ℕ is a random time τ : Ω → ℕ∞ such that for all n, the set {ω | τ ω ≤ n} is measurable with respect to 𝓕 n.

variable {τ : Ω → ℕ∞} (hτ : IsStoppingTime 𝓕 τ)

example (i : ℕ) : MeasurableSet[𝓕 i] {ω | τ ω ≤ i} := hτ.measurableSet_le i

The optional stopping theorem (fair game theorem): an adapted integrable process Y is a submartingale if and only if for all bounded stopping times τ and π such that τ ≤ π, the stopped value of Y at τ has expectation smaller than its stopped value at π.

theorem submartingale_iff_expected_stoppedValue_mono' {Y : ℕ → Ω → ℝ} (hadp : StronglyAdapted 𝓕 Y)
    (hint : ∀ i, Integrable (Y i) P) :
    Submartingale Y 𝓕 P ↔ ∀ τ π : Ω → ℕ∞, IsStoppingTime 𝓕 τ → IsStoppingTime 𝓕 π →
      τ ≤ π → (∃ N : ℕ, ∀ x, π x ≤ N) → P[stoppedValue Y τ] ≤ P[stoppedValue Y π] :=
  ⟨fun hf _ _ hτ hπ hle ⟨_, hN⟩ => hf.expected_stoppedValue_mono hτ hπ hle hN,
    submartingale_of_expected_stoppedValue_mono hadp hint⟩