mathlibdocumentation

probability_theory.stopping

Filtration and stopping time #

This file defines some standard definition from the theory of stochastic processes including filtrations and stopping times. These definitions are used to model the amount of information at a specific time and is the first step in formalizing stochastic processes.

Main definitions #

• measure_theory.filtration: a filtration on a measurable space
• measure_theory.adapted: a sequence of functions u is said to be adapted to a filtration f if at each point in time i, u i is f i-measurable
• measure_theory.filtration.natural: the natural filtration with respect to a sequence of measurable functions is the smallest filtration to which it is adapted to
• measure_theory.stopping_time: a stopping time with respect to some filtration f is a function τ such that for all i, the preimage of {j | j ≤ i} along τ is f i-measurable
• measure_theory.stopping_time.measurable_space: the σ-algebra associated with a stopping time

Tags #

filtration, stopping time, stochastic process

structure measure_theory.filtration {α : Type u_1} (ι : Type u_2) [preorder ι] (m : measurable_space α) :
Type (max u_1 u_2)

A filtration on measurable space α with σ-algebra m is a monotone sequence of of sub-σ-algebras of m.

@[protected, instance]
def measure_theory.filtration.has_coe_to_fun {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [preorder ι] :
(λ (_x : , ι →
Equations
def measure_theory.const_filtration {α : Type u_1} {ι : Type u_3} [preorder ι] (m : measurable_space α) :

The constant filtration which is equal to m for all i : ι.

Equations
@[protected, instance]
def measure_theory.filtration.inhabited {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [preorder ι] :
Equations
theorem measure_theory.measurable_set_of_filtration {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [preorder ι] {f : m} {s : set α} {i : ι} (hs : measurable_set s) :
@[class]
structure measure_theory.sigma_finite_filtration {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [preorder ι] (μ : measure_theory.measure α) (f : m) :
Prop
• sigma_finite : ∀ (i : ι),

A measure is σ-finite with respect to filtration if it is σ-finite with respect to all the sub-σ-algebra of the filtration.

@[protected, instance]
def measure_theory.sigma_finite_of_sigma_finite_filtration {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [preorder ι] (μ : measure_theory.measure α) (f : m) (i : ι) :
def measure_theory.adapted {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} [preorder ι] (f : m) (u : ι → α → β) :
Prop

A sequence of functions u is adapted to a filtration f if for all i, u i is f i-measurable.

Equations
theorem measure_theory.adapted.add {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} [preorder ι] [has_add β] {u v : ι → α → β} {f : m} (hu : u) (hv : v) :
(u + v)
theorem measure_theory.adapted.neg {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} [preorder ι] [has_neg β] {u : ι → α → β} {f : m} (hu : u) :
theorem measure_theory.adapted.smul {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} [preorder ι] [ β] {u : ι → α → β} {f : m} (c : ) (hu : u) :
(c u)
theorem measure_theory.adapted_zero {α : Type u_1} (β : Type u_2) {ι : Type u_3} {m : measurable_space α} [preorder ι] [has_zero β] (f : m) :
def measure_theory.filtration.natural {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} [preorder ι] (u : ι → α → β) (hum : ∀ (i : ι), measurable (u i)) :

Given a sequence of functions, the natural filtration is the smallest sequence of σ-algebras such that that sequence of functions is measurable with respect to the filtration.

Equations
• = {seq := λ (i : ι), ⨆ (j : ι) (H : j i), , mono := _, le := _}
theorem measure_theory.filtration.adapted_natural {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} [preorder ι] {u : ι → α → β} (hum : ∀ (i : ι), measurable (u i)) :
def measure_theory.is_stopping_time {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [preorder ι] (f : m) (τ : α → ι) :
Prop

A stopping time with respect to some filtration f is a function τ such that for all i, the preimage of {j | j ≤ i} along τ is measurable with respect to f i.

Intuitively, the stopping time τ describes some stopping rule such that at time i, we may determine it with the information we have at time i.

Equations
theorem measure_theory.is_stopping_time.measurable_set_le {α : Type u_1} {m : measurable_space α} {f : m} {τ : α → } (hτ : τ) (i : ) :
measurable_set {x : α | τ x i}
theorem measure_theory.is_stopping_time.measurable_set_eq {α : Type u_1} {m : measurable_space α} {f : m} {τ : α → } (hτ : τ) (i : ) :
measurable_set {x : α | τ x = i}
theorem measure_theory.is_stopping_time.measurable_set_ge {α : Type u_1} {m : measurable_space α} {f : m} {τ : α → } (hτ : τ) (i : ) :
measurable_set {x : α | i τ x}
theorem measure_theory.is_stopping_time.measurable_set_eq_le {α : Type u_1} {m : measurable_space α} {f : m} {τ : α → } (hτ : τ) {i j : } (hle : i j) :
measurable_set {x : α | τ x = i}
theorem measure_theory.is_stopping_time.measurable_set_lt {α : Type u_1} {m : measurable_space α} {f : m} {τ : α → } (hτ : τ) (i : ) :
measurable_set {x : α | τ x < i}
theorem measure_theory.is_stopping_time.measurable_set_lt_le {α : Type u_1} {m : measurable_space α} {f : m} {τ : α → } (hτ : τ) {i j : } (hle : i j) :
measurable_set {x : α | τ x < i}
theorem measure_theory.is_stopping_time_of_measurable_set_eq {α : Type u_1} {m : measurable_space α} {f : m} {τ : α → } (hτ : ∀ (i : ), measurable_set {x : α | τ x = i}) :
theorem measure_theory.is_stopping_time_const {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [preorder ι] {f : m} (i : ι) :
(λ (x : α), i)
theorem measure_theory.is_stopping_time.max {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [linear_order ι] {f : m} {τ π : α → ι} (hτ : τ) (hπ : π) :
(λ (x : α), max (τ x) (π x))
theorem measure_theory.is_stopping_time.min {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [linear_order ι] {f : m} {τ π : α → ι} (hτ : τ) (hπ : π) :
(λ (x : α), min (τ x) (π x))
theorem measure_theory.is_stopping_time.add_const {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [add_group ι] [preorder ι] {f : m} {τ : α → ι} (hτ : τ) {i : ι} (hi : 0 i) :
(λ (x : α), τ x + i)
@[protected]
def measure_theory.is_stopping_time.measurable_space {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [preorder ι] {f : m} {τ : α → ι} (hτ : τ) :

The associated σ-algebra with a stopping time.

Equations
@[protected]
theorem measure_theory.is_stopping_time.measurable_set {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [preorder ι] {f : m} {τ : α → ι} (hτ : τ) (s : set α) :
∀ (i : ι), measurable_set (s {x : α | τ x i})
theorem measure_theory.is_stopping_time.measurable_space_mono {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [preorder ι] {f : m} {τ π : α → ι} (hτ : τ) (hπ : π) (hle : τ π) :
theorem measure_theory.is_stopping_time.measurable_space_le {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [preorder ι] {f : m} [encodable ι] {τ : α → ι} (hτ : τ) :
theorem measure_theory.is_stopping_time.measurable_set_eq_const {α : Type u_1} {m : measurable_space α} {f : m} {τ : α → } (hτ : τ) (i : ) :
measurable_set {x : α | τ x = i}
theorem measure_theory.is_stopping_time.measurable {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [linear_order ι] [borel_space ι] {f : m} {τ : α → ι} (hτ : τ) :
def measure_theory.stopped_value {α : Type u_1} {β : Type u_2} {ι : Type u_3} (u : ι → α → β) (τ : α → ι) :
α → β

Given a map u : ι → α → E, its stopped value with respect to the stopping time τ is the map x ↦ u (τ x) x.

Equations
• = λ (x : α), u (τ x) x
def measure_theory.stopped_process {α : Type u_1} {β : Type u_2} {ι : Type u_3} [linear_order ι] (u : ι → α → β) (τ : α → ι) :
ι → α → β

Given a map u : ι → α → E, the stopped process with respect to τ is u i x if i ≤ τ x, and u (τ x) x otherwise.

Intuitively, the stopped process stops evolving once the stopping time has occured.

Equations
• = λ (i : ι) (x : α), u (min i (τ x)) x
theorem measure_theory.stopped_process_eq_of_le {α : Type u_1} {β : Type u_2} {ι : Type u_3} [linear_order ι] {u : ι → α → β} {τ : α → ι} {i : ι} {x : α} (h : i τ x) :
= u i x
theorem measure_theory.stopped_process_eq_of_ge {α : Type u_1} {β : Type u_2} {ι : Type u_3} [linear_order ι] {u : ι → α → β} {τ : α → ι} {i : ι} {x : α} (h : τ x i) :
= u (τ x) x
theorem measure_theory.stopped_value_sub_eq_sum {α : Type u_1} {β : Type u_2} {u : α → β} {τ π : α → } (hle : τ π) :
= λ (x : α), (∑ (i : ) in finset.Ico (τ x) (π x), (u (i + 1) - u i)) x
theorem measure_theory.stopped_value_sub_eq_sum' {α : Type u_1} {β : Type u_2} {u : α → β} {τ π : α → } (hle : τ π) {N : } (hbdd : ∀ (x : α), π x N) :
= λ (x : α), (∑ (i : ) in finset.range (N + 1), {x : α | τ x i i < π x}.indicator (u (i + 1) - u i)) x
theorem measure_theory.stopped_value_eq {α : Type u_1} {β : Type u_2} {u : α → β} {τ : α → } {N : } (hbdd : ∀ (x : α), τ x N) :
= λ (x : α), (∑ (i : ) in finset.range (N + 1), {x : α | τ x = i}.indicator (u i)) x
theorem measure_theory.stopped_process_eq {α : Type u_1} {β : Type u_2} {u : α → β} {τ : α → } (n : ) :
= {a : α | n τ a}.indicator (u n) + ∑ (i : ) in , {a : α | τ a = i}.indicator (u i)
theorem measure_theory.adapted.stopped_process {α : Type u_1} {β : Type u_2} {m : measurable_space α} {f : m} {u : α → β} {τ : α → } (hu : u) (hτ : τ) :
theorem measure_theory.measurable_stopped_process {α : Type u_1} {β : Type u_2} {m : measurable_space α} {f : m} {u : α → β} {τ : α → } [normed_group β] (hτ : τ) (hu : u) (n : ) :
theorem measure_theory.mem_ℒp_stopped_process {α : Type u_1} {β : Type u_2} {m : measurable_space α} {f : m} {u : α → β} {τ : α → } [normed_group β] {p : ℝ≥0∞} [borel_space β] {μ : measure_theory.measure α} (hτ : τ) (hu : ∀ (n : ), p μ) (n : ) :
theorem measure_theory.integrable_stopped_process {α : Type u_1} {β : Type u_2} {m : measurable_space α} {f : m} {u : α → β} {τ : α → } [normed_group β] [borel_space β] {μ : measure_theory.measure α} (hτ : τ) (hu : ∀ (n : ), μ) (n : ) :
theorem measure_theory.mem_ℒp_stopped_value {α : Type u_1} {β : Type u_2} {m : measurable_space α} {f : m} {u : α → β} {τ : α → } [normed_group β] {p : ℝ≥0∞} [borel_space β] {μ : measure_theory.measure α} (hτ : τ) (hu : ∀ (n : ), p μ) {N : } (hbdd : ∀ (x : α), τ x N) :
theorem measure_theory.integrable_stopped_value {α : Type u_1} {β : Type u_2} {m : measurable_space α} {f : m} {u : α → β} {τ : α → } [normed_group β] [borel_space β] {μ : measure_theory.measure α} (hτ : τ) (hu : ∀ (n : ), μ) {N : } (hbdd : ∀ (x : α), τ x N) :