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 spacemeasure_theory.adapted: a sequence of functionsuis said to be adapted to a filtrationfif at each point in timei,u iisf i-measurablemeasure_theory.filtration.natural: the natural filtration with respect to a sequence of measurable functions is the smallest filtration to which it is adapted tomeasure_theory.is_stopping_time: a stopping time with respect to some filtrationfis a functionτsuch that for alli, the preimage of{j | j ≤ i}alongτisf i-measurablemeasure_theory.is_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)
- seq : ι → measurable_space α
- mono : monotone self.seq
- le : ∀ (i : ι), self.seq i ≤ m
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 ι] :
has_coe_to_fun (measure_theory.filtration ι m) (λ (_x : measure_theory.filtration ι m), ι → measurable_space α)
Equations
- measure_theory.filtration.has_coe_to_fun = {coe := λ (f : measure_theory.filtration ι m), f.seq}
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 : ι.
@[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 : 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
- sigma_finite : ∀ (i : ι), measure_theory.sigma_finite (μ.trim _)
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 : measure_theory.filtration ι m)
[hf : measure_theory.sigma_finite_filtration μ f]
(i : ι) :
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
- measure_theory.adapted f u = ∀ (i : ι), measurable (u i)
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) :
measure_theory.adapted f (u + 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) :
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) :
measure_theory.adapted f (c • 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
- measure_theory.filtration.natural u hum = {seq := λ (i : ι), ⨆ (j : ι) (H : j ≤ i), measurable_space.comap (u j) infer_instance, mono := _, le := _}
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
- measure_theory.is_stopping_time f τ = ∀ (i : ι), measurable_set {x : α | τ x ≤ i}
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 : ι) :
measure_theory.is_stopping_time f (λ (x : α), 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
- hτ.measurable_space = {measurable_set' := λ (s : set α), ∀ (i : ι), measurable_set (s ∩ {x : α | τ x ≤ i}), measurable_set_empty := _, measurable_set_compl := _, measurable_set_Union := _}
@[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 τ) :
hτ.measurable_space ≤ m
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}
theorem
measure_theory.is_stopping_time.measurable
{α : Type u_1}
{ι : Type u_3}
{m : measurable_space α}
[linear_order ι]
[topological_space ι]
[measurable_space ι]
[borel_space ι]
[order_topology ι]
[topological_space.second_countable_topology ι]
{f : measure_theory.filtration ι m}
{τ : α → ι}
(hτ : measure_theory.is_stopping_time f τ) :
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
- measure_theory.stopped_value u τ = λ (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
- measure_theory.stopped_process u τ = λ (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) :
measure_theory.stopped_process u τ 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) :
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.adapted.stopped_process
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{f : measure_theory.filtration ℕ m}
{u : ℕ → α → β}
{τ : α → ℕ}
[add_comm_monoid β]
[measurable_space β]
[has_measurable_add₂ β]
(hu : measure_theory.adapted f u)
(hτ : measure_theory.is_stopping_time f τ) :
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 : ℕ) :
measure_theory.mem_ℒp (measure_theory.stopped_process u τ n) p μ
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) :