mathlib documentation

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 #

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 ι] :
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
theorem measure_theory.measurable_set_of_filtration {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [preorder ι] {f : measure_theory.filtration ι 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 : measure_theory.filtration ι m) :
Prop

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.adapted {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} [preorder ι] [measurable_space β] (f : measure_theory.filtration ι 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 ι] [measurable_space β] [has_add β] [has_measurable_add₂ β] {u v : ι → α → β} {f : measure_theory.filtration ι m} (hu : measure_theory.adapted f u) (hv : measure_theory.adapted f v) :
theorem measure_theory.adapted.neg {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} [preorder ι] [measurable_space β] [has_neg β] [has_measurable_neg β] {u : ι → α → β} {f : measure_theory.filtration ι m} (hu : measure_theory.adapted f u) :
theorem measure_theory.adapted.smul {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} [preorder ι] [measurable_space β] [has_scalar β] [has_measurable_smul β] {u : ι → α → β} {f : measure_theory.filtration ι m} (c : ) (hu : measure_theory.adapted f u) :
theorem measure_theory.adapted_zero {α : Type u_1} (β : Type u_2) {ι : Type u_3} {m : measurable_space α} [preorder ι] [measurable_space β] [has_zero β] (f : measure_theory.filtration ι m) :
def measure_theory.filtration.natural {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} [preorder ι] [measurable_space β] (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
theorem measure_theory.filtration.adapted_natural {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} [preorder ι] [measurable_space β] {u : ι → α → β} (hum : ∀ (i : ι), measurable (u i)) :
def measure_theory.is_stopping_time {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [preorder ι] (f : measure_theory.filtration ι 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 : measure_theory.filtration m} {τ : α → } (hτ : measure_theory.is_stopping_time f τ) (i : ) :
measurable_set {x : α | τ x i}
theorem measure_theory.is_stopping_time.measurable_set_eq {α : Type u_1} {m : measurable_space α} {f : measure_theory.filtration m} {τ : α → } (hτ : measure_theory.is_stopping_time f τ) (i : ) :
measurable_set {x : α | τ x = i}
theorem measure_theory.is_stopping_time.measurable_set_ge {α : Type u_1} {m : measurable_space α} {f : measure_theory.filtration m} {τ : α → } (hτ : measure_theory.is_stopping_time f τ) (i : ) :
measurable_set {x : α | i τ x}
theorem measure_theory.is_stopping_time.measurable_set_eq_le {α : Type u_1} {m : measurable_space α} {f : measure_theory.filtration m} {τ : α → } (hτ : measure_theory.is_stopping_time f τ) {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 : measure_theory.filtration m} {τ : α → } (hτ : measure_theory.is_stopping_time f τ) (i : ) :
measurable_set {x : α | τ x < i}
theorem measure_theory.is_stopping_time.measurable_set_lt_le {α : Type u_1} {m : measurable_space α} {f : measure_theory.filtration m} {τ : α → } (hτ : measure_theory.is_stopping_time f τ) {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 : measure_theory.filtration 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 : measure_theory.filtration ι m} (i : ι) :
theorem measure_theory.is_stopping_time.max {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [linear_order ι] {f : measure_theory.filtration ι m} {τ π : α → ι} (hτ : measure_theory.is_stopping_time f τ) (hπ : measure_theory.is_stopping_time f π) :
measure_theory.is_stopping_time f (λ (x : α), max (τ x) (π x))
theorem measure_theory.is_stopping_time.min {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [linear_order ι] {f : measure_theory.filtration ι m} {τ π : α → ι} (hτ : measure_theory.is_stopping_time f τ) (hπ : measure_theory.is_stopping_time f π) :
measure_theory.is_stopping_time f (λ (x : α), min (τ x) (π x))
theorem measure_theory.is_stopping_time.add_const {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [add_group ι] [preorder ι] [covariant_class ι ι (function.swap has_add.add) has_le.le] [covariant_class ι ι has_add.add has_le.le] {f : measure_theory.filtration ι m} {τ : α → ι} (hτ : measure_theory.is_stopping_time f τ) {i : ι} (hi : 0 i) :
measure_theory.is_stopping_time f (λ (x : α), τ x + i)
@[protected]
def measure_theory.is_stopping_time.measurable_space {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [preorder ι] {f : measure_theory.filtration ι m} {τ : α → ι} (hτ : measure_theory.is_stopping_time f τ) :

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 : measure_theory.filtration ι m} {τ : α → ι} (hτ : measure_theory.is_stopping_time f τ) (s : set α) :
measurable_set s ∀ (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 : measure_theory.filtration ι m} {τ π : α → ι} (hτ : measure_theory.is_stopping_time f τ) (hπ : measure_theory.is_stopping_time f π) (hle : τ π) :
theorem measure_theory.is_stopping_time.measurable_space_le {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [preorder ι] {f : measure_theory.filtration ι m} [encodable ι] {τ : α → ι} (hτ : measure_theory.is_stopping_time f τ) :
theorem measure_theory.is_stopping_time.measurable_set_eq_const {α : Type u_1} {m : measurable_space α} {f : measure_theory.filtration m} {τ : α → } (hτ : measure_theory.is_stopping_time f τ) (i : ) :
measurable_set {x : α | τ x = i}
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
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
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) :
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) :
measure_theory.stopped_process u τ i x = u (τ x) x
theorem measure_theory.stopped_value_sub_eq_sum {α : Type u_1} {β : Type u_2} {u : α → β} {τ π : α → } [add_comm_group β] (hle : τ π) :
measure_theory.stopped_value u π - measure_theory.stopped_value u τ = λ (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 : α → β} {τ π : α → } [add_comm_group β] (hle : τ π) {N : } (hbdd : ∀ (x : α), π x N) :
measure_theory.stopped_value u π - measure_theory.stopped_value u τ = λ (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 : α → β} {τ : α → } [add_comm_monoid β] {N : } (hbdd : ∀ (x : α), τ x N) :
measure_theory.stopped_value u τ = λ (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 : α → β} {τ : α → } [add_comm_monoid β] (n : ) :
measure_theory.stopped_process u τ n = {a : α | n τ a}.indicator (u n) + ∑ (i : ) in finset.range n, {a : α | τ a = i}.indicator (u i)
theorem measure_theory.measurable_stopped_process {α : Type u_1} {β : Type u_2} {m : measurable_space α} {f : measure_theory.filtration m} {u : α → β} {τ : α → } [measurable_space β] [normed_group β] [has_measurable_add₂ β] (hτ : measure_theory.is_stopping_time f τ) (hu : measure_theory.adapted f u) (n : ) :
theorem measure_theory.mem_ℒp_stopped_process {α : Type u_1} {β : Type u_2} {m : measurable_space α} {f : measure_theory.filtration m} {u : α → β} {τ : α → } [measurable_space β] [normed_group β] [has_measurable_add₂ β] {p : ℝ≥0∞} [borel_space β] {μ : measure_theory.measure α} (hτ : measure_theory.is_stopping_time f τ) (hu : ∀ (n : ), measure_theory.mem_ℒp (u n) p μ) (n : ) :
theorem measure_theory.integrable_stopped_process {α : Type u_1} {β : Type u_2} {m : measurable_space α} {f : measure_theory.filtration m} {u : α → β} {τ : α → } [measurable_space β] [normed_group β] [has_measurable_add₂ β] [borel_space β] {μ : measure_theory.measure α} (hτ : measure_theory.is_stopping_time f τ) (hu : ∀ (n : ), measure_theory.integrable (u n) μ) (n : ) :
theorem measure_theory.mem_ℒp_stopped_value {α : Type u_1} {β : Type u_2} {m : measurable_space α} {f : measure_theory.filtration m} {u : α → β} {τ : α → } [measurable_space β] [normed_group β] [has_measurable_add₂ β] {p : ℝ≥0∞} [borel_space β] {μ : measure_theory.measure α} (hτ : measure_theory.is_stopping_time f τ) (hu : ∀ (n : ), measure_theory.mem_ℒp (u n) p μ) {N : } (hbdd : ∀ (x : α), τ x N) :
theorem measure_theory.integrable_stopped_value {α : Type u_1} {β : Type u_2} {m : measurable_space α} {f : measure_theory.filtration m} {u : α → β} {τ : α → } [measurable_space β] [normed_group β] [has_measurable_add₂ β] [borel_space β] {μ : measure_theory.measure α} (hτ : measure_theory.is_stopping_time f τ) (hu : ∀ (n : ), measure_theory.integrable (u n) μ) {N : } (hbdd : ∀ (x : α), τ x N) :