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Ω} {n : ℕ}
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.
example {Y : ℕ → Ω → ℝ} (hY : Submartingale Y 𝓕 P)
{R : ℝ≥0} (hbdd : ∀ n, eLpNorm (Y n) 1 P ≤ R) :
∀ᵐ ω ∂P, Tendsto (Y · ω) atTop (𝓝 (𝓕.limitProcess Y P ω)) := Ω✝:Type u_1mΩ✝:MeasurableSpace Ω✝P✝:Measure Ω✝inst✝⁴:IsProbabilityMeasure P✝Ω:Type u_2mΩ:MeasurableSpace ΩP:Measure Ωinst✝³:IsProbabilityMeasure PE:Type u_3inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace ℝ Einst✝:CompleteSpace EmE:MeasurableSpace EX:ℕ → Ω → E𝓕:Filtration ℕ mΩn:ℕ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
Ω✝:Type u_1mΩ✝:MeasurableSpace Ω✝P✝:Measure Ω✝inst✝⁴:IsProbabilityMeasure P✝Ω:Type u_2mΩ:MeasurableSpace ΩP:Measure Ωinst✝³:IsProbabilityMeasure PE:Type u_3inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace ℝ Einst✝:CompleteSpace EmE:MeasurableSpace EX:ℕ → Ω → E𝓕:Filtration ℕ mΩn:ℕY:ℕ → Ω → ℝhY:Submartingale Y 𝓕 PR:ℝ≥0hbdd:∀ (n : ℕ), eLpNorm (Y n) 1 P ≤ ↑R⊢ ∃ g, StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂P, Tendsto (fun x ↦ Y x ω) atTop (𝓝 (g ω))
Ω✝:Type u_1mΩ✝:MeasurableSpace Ω✝P✝:Measure Ω✝inst✝⁴:IsProbabilityMeasure P✝Ω:Type u_2mΩ:MeasurableSpace ΩP:Measure Ωinst✝³:IsProbabilityMeasure PE:Type u_3inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace ℝ Einst✝:CompleteSpace EmE:MeasurableSpace EX:ℕ → Ω → E𝓕:Filtration ℕ mΩn:ℕ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 ω))
Ω✝:Type u_1mΩ✝:MeasurableSpace Ω✝P✝:Measure Ω✝inst✝⁴:IsProbabilityMeasure P✝Ω:Type u_2mΩ:MeasurableSpace ΩP:Measure Ωinst✝³:IsProbabilityMeasure PE:Type u_3inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace ℝ Einst✝:CompleteSpace EmE:MeasurableSpace EX:ℕ → Ω → E𝓕:Filtration ℕ mΩn:ℕ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 ω))
Ω✝:Type u_1mΩ✝:MeasurableSpace Ω✝P✝:Measure Ω✝inst✝⁴:IsProbabilityMeasure P✝Ω:Type u_2mΩ:MeasurableSpace ΩP:Measure Ωinst✝³:IsProbabilityMeasure PE:Type u_3inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace ℝ Einst✝:CompleteSpace EmE:MeasurableSpace EX:ℕ → Ω → E𝓕:Filtration ℕ mΩn:ℕ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, StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂P, Tendsto (fun x ↦ Y x ω) atTop (𝓝 (g ω))
Ω✝:Type u_1mΩ✝:MeasurableSpace Ω✝P✝:Measure Ω✝inst✝⁴:IsProbabilityMeasure P✝Ω:Type u_2mΩ:MeasurableSpace ΩP:Measure Ωinst✝³:IsProbabilityMeasure PE:Type u_3inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace ℝ Einst✝:CompleteSpace EmE:MeasurableSpace EX:ℕ → Ω → E𝓕:Filtration ℕ mΩn:ℕ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 ω))
Ω✝:Type u_1mΩ✝:MeasurableSpace Ω✝P✝:Measure Ω✝inst✝⁴:IsProbabilityMeasure P✝Ω:Type u_2mΩ:MeasurableSpace ΩP:Measure Ωinst✝³:IsProbabilityMeasure PE:Type u_3inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace ℝ Einst✝:CompleteSpace EmE:MeasurableSpace EX:ℕ → Ω → E𝓕:Filtration ℕ mΩn:ℕ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' =ᵐ[P.trim hle] g⊢ ∃ g, StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂P, Tendsto (fun x ↦ Y x ω) atTop (𝓝 (g ω))
Ω✝:Type u_1mΩ✝:MeasurableSpace Ω✝P✝:Measure Ω✝inst✝⁴:IsProbabilityMeasure P✝Ω:Type u_2mΩ:MeasurableSpace ΩP:Measure Ωinst✝³:IsProbabilityMeasure PE:Type u_3inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace ℝ Einst✝:CompleteSpace EmE:MeasurableSpace EX:ℕ → Ω → E𝓕:Filtration ℕ mΩn:ℕ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' =ᵐ[P.trim hle] ghg:∀ᵐ (ω : Ω) ∂P.trim hle, Tendsto (fun x ↦ Y x ω) atTop (𝓝 (g ω))⊢ ∃ g, StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂P, Tendsto (fun x ↦ Y x ω) atTop (𝓝 (g ω))
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 π.
example {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⟩