mathlib3 documentation

probability.process.stopping

Stopping times, stopped processes and stopped values #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Definition and properties of stopping times.

Main definitions #

Main results #

Tags #

stopping time, stochastic process

Stopping times #

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_const {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] (f : measure_theory.filtration ι m) (i : ι) :
@[protected]
theorem measure_theory.is_stopping_time.measurable_set_le {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] {f : measure_theory.filtration ι m} {τ : Ω ι} (hτ : measure_theory.is_stopping_time f τ) (i : ι) :
measurable_set {ω : Ω | τ ω i}
theorem measure_theory.is_stopping_time.measurable_set_lt_of_pred {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] {f : measure_theory.filtration ι m} {τ : Ω ι} [pred_order ι] (hτ : measure_theory.is_stopping_time f τ) (i : ι) :
measurable_set {ω : Ω | τ ω < i}
@[protected]
theorem measure_theory.is_stopping_time.measurable_set_eq_of_countable_range {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [partial_order ι] {τ : Ω ι} {f : measure_theory.filtration ι m} (hτ : measure_theory.is_stopping_time f τ) (h_countable : (set.range τ).countable) (i : ι) :
measurable_set {ω : Ω | τ ω = i}
@[protected]
theorem measure_theory.is_stopping_time.measurable_set_eq_of_countable {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [partial_order ι] {τ : Ω ι} {f : measure_theory.filtration ι m} [countable ι] (hτ : measure_theory.is_stopping_time f τ) (i : ι) :
measurable_set {ω : Ω | τ ω = i}
@[protected]
theorem measure_theory.is_stopping_time.measurable_set_lt_of_countable_range {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [partial_order ι] {τ : Ω ι} {f : measure_theory.filtration ι m} (hτ : measure_theory.is_stopping_time f τ) (h_countable : (set.range τ).countable) (i : ι) :
measurable_set {ω : Ω | τ ω < i}
@[protected]
theorem measure_theory.is_stopping_time.measurable_set_lt_of_countable {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [partial_order ι] {τ : Ω ι} {f : measure_theory.filtration ι m} [countable ι] (hτ : measure_theory.is_stopping_time f τ) (i : ι) :
measurable_set {ω : Ω | τ ω < i}
@[protected]
theorem measure_theory.is_stopping_time.measurable_set_ge_of_countable_range {Ω : Type u_1} {m : measurable_space Ω} {ι : Type u_2} [linear_order ι] {τ : Ω ι} {f : measure_theory.filtration ι m} (hτ : measure_theory.is_stopping_time f τ) (h_countable : (set.range τ).countable) (i : ι) :
measurable_set {ω : Ω | i τ ω}
@[protected]
theorem measure_theory.is_stopping_time.measurable_set_ge_of_countable {Ω : Type u_1} {m : measurable_space Ω} {ι : Type u_2} [linear_order ι] {τ : Ω ι} {f : measure_theory.filtration ι m} [countable ι] (hτ : measure_theory.is_stopping_time f τ) (i : ι) :
measurable_set {ω : Ω | i τ ω}
theorem measure_theory.is_stopping_time.measurable_set_gt {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [linear_order ι] {f : measure_theory.filtration ι m} {τ : Ω ι} (hτ : measure_theory.is_stopping_time f τ) (i : ι) :
measurable_set {ω : Ω | i < τ ω}

Auxiliary lemma for is_stopping_time.measurable_set_lt.

theorem measure_theory.is_stopping_time_of_measurable_set_eq {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] [countable ι] {f : measure_theory.filtration ι m} {τ : Ω ι} (hτ : (i : ι), measurable_set {ω : Ω | τ ω = i}) :
@[protected]
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 (λ (ω : Ω), linear_order.max (τ ω) (π ω))
@[protected]
theorem measure_theory.is_stopping_time.max_const {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [linear_order ι] {f : measure_theory.filtration ι m} {τ : Ω ι} (hτ : measure_theory.is_stopping_time f τ) (i : ι) :
@[protected]
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 (λ (ω : Ω), linear_order.min (τ ω) (π ω))
@[protected]
theorem measure_theory.is_stopping_time.min_const {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [linear_order ι] {f : measure_theory.filtration ι m} {τ : Ω ι} (hτ : measure_theory.is_stopping_time f τ) (i : ι) :
@[protected]

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 {ω : Ω | τ ω i})
theorem measure_theory.is_stopping_time.measurable_set_inter_eq_iff {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] {f : measure_theory.filtration ι m} {τ : Ω ι} (hτ : measure_theory.is_stopping_time f τ) (s : set Ω) (i : ι) :
measurable_set (s {ω : Ω | τ ω = i}) measurable_set (s {ω : Ω | τ ω = i})
theorem measure_theory.is_stopping_time.measurable_space_le_of_le_const {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] {f : measure_theory.filtration ι m} {τ : Ω ι} (hτ : measure_theory.is_stopping_time f τ) {i : ι} (hτ_le : (ω : Ω), τ ω i) :
theorem measure_theory.is_stopping_time.measurable_space_le_of_le {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] {f : measure_theory.filtration ι m} {τ : Ω ι} (hτ : measure_theory.is_stopping_time f τ) {n : ι} (hτ_le : (ω : Ω), τ ω n) :
theorem measure_theory.is_stopping_time.le_measurable_space_of_const_le {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] {f : measure_theory.filtration ι m} {τ : Ω ι} (hτ : measure_theory.is_stopping_time f τ) {i : ι} (hτ_le : (ω : Ω), i τ ω) :
@[protected, instance]
@[protected]
theorem measure_theory.is_stopping_time.measurable_set_le' {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [linear_order ι] {f : measure_theory.filtration ι m} {τ : Ω ι} (hτ : measure_theory.is_stopping_time f τ) (i : ι) :
measurable_set {ω : Ω | τ ω i}
@[protected]
theorem measure_theory.is_stopping_time.measurable_set_gt' {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [linear_order ι] {f : measure_theory.filtration ι m} {τ : Ω ι} (hτ : measure_theory.is_stopping_time f τ) (i : ι) :
measurable_set {ω : Ω | i < τ ω}
@[protected]
theorem measure_theory.is_stopping_time.measurable_set_eq_of_countable_range' {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [linear_order ι] {f : measure_theory.filtration ι m} {τ : Ω ι} (hτ : measure_theory.is_stopping_time f τ) (h_countable : (set.range τ).countable) (i : ι) :
measurable_set {ω : Ω | τ ω = i}
@[protected]
theorem measure_theory.is_stopping_time.measurable_set_eq_of_countable' {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [linear_order ι] {f : measure_theory.filtration ι m} {τ : Ω ι} [countable ι] (hτ : measure_theory.is_stopping_time f τ) (i : ι) :
measurable_set {ω : Ω | τ ω = i}
@[protected]
theorem measure_theory.is_stopping_time.measurable_set_ge_of_countable_range' {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [linear_order ι] {f : measure_theory.filtration ι m} {τ : Ω ι} (hτ : measure_theory.is_stopping_time f τ) (h_countable : (set.range τ).countable) (i : ι) :
measurable_set {ω : Ω | i τ ω}
@[protected]
theorem measure_theory.is_stopping_time.measurable_set_ge_of_countable' {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [linear_order ι] {f : measure_theory.filtration ι m} {τ : Ω ι} [countable ι] (hτ : measure_theory.is_stopping_time f τ) (i : ι) :
measurable_set {ω : Ω | i τ ω}
@[protected]
theorem measure_theory.is_stopping_time.measurable_set_lt_of_countable_range' {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [linear_order ι] {f : measure_theory.filtration ι m} {τ : Ω ι} (hτ : measure_theory.is_stopping_time f τ) (h_countable : (set.range τ).countable) (i : ι) :
measurable_set {ω : Ω | τ ω < i}
@[protected]
theorem measure_theory.is_stopping_time.measurable_set_lt_of_countable' {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [linear_order ι] {f : measure_theory.filtration ι m} {τ : Ω ι} [countable ι] (hτ : measure_theory.is_stopping_time f τ) (i : ι) :
measurable_set {ω : Ω | τ ω < i}
@[protected]
theorem measure_theory.is_stopping_time.measurable_set_inter_le_const_iff {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [linear_order ι] {f : measure_theory.filtration ι m} {τ : Ω ι} (hτ : measure_theory.is_stopping_time f τ) (s : set Ω) (i : ι) :
measurable_set (s {ω : Ω | τ ω i}) measurable_set (s {ω : Ω | τ ω i})

Stopped value and stopped process #

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 (τ ω) ω.

Equations
theorem measure_theory.stopped_value_const {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} (u : ι Ω β) (i : ι) :
measure_theory.stopped_value u (λ (ω : Ω), i) = u i
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 ω if i ≤ τ ω, and u (τ ω) ω otherwise.

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

Equations
theorem measure_theory.stopped_process_eq_stopped_value {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [linear_order ι] {u : ι Ω β} {τ : Ω ι} :
theorem measure_theory.stopped_value_stopped_process {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [linear_order ι] {u : ι Ω β} {τ σ : Ω ι} :
theorem measure_theory.stopped_process_eq_of_le {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [linear_order ι] {u : ι Ω β} {τ : Ω ι} {i : ι} {ω : Ω} (h : i τ ω) :
theorem measure_theory.stopped_process_eq_of_ge {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [linear_order ι] {u : ι Ω β} {τ : Ω ι} {i : ι} {ω : Ω} (h : τ ω i) :
measure_theory.stopped_process u τ i ω = u (τ ω) ω
theorem measure_theory.stopped_value_eq_of_mem_finset {Ω : Type u_1} {ι : Type u_3} {τ : Ω ι} {E : Type u_4} {u : ι Ω E} [add_comm_monoid E] {s : finset ι} (hbdd : (ω : Ω), τ ω s) :
measure_theory.stopped_value u τ = s.sum (λ (i : ι), {ω : Ω | τ ω = i}.indicator (u i))
theorem measure_theory.stopped_value_eq' {Ω : Type u_1} {ι : Type u_3} {τ : Ω ι} {E : Type u_4} {u : ι Ω E} [preorder ι] [locally_finite_order_bot ι] [add_comm_monoid E] {N : ι} (hbdd : (ω : Ω), τ ω N) :
measure_theory.stopped_value u τ = (finset.Iic N).sum (λ (i : ι), {ω : Ω | τ ω = i}.indicator (u i))
theorem measure_theory.stopped_process_eq_of_mem_finset {Ω : Type u_1} {ι : Type u_3} {τ : Ω ι} {E : Type u_4} {u : ι Ω E} [linear_order ι] [add_comm_monoid E] {s : finset ι} (n : ι) (hbdd : (ω : Ω), τ ω < n τ ω s) :
measure_theory.stopped_process u τ n = {a : Ω | n τ a}.indicator (u n) + (finset.filter (λ (_x : ι), _x < n) s).sum (λ (i : ι), {ω : Ω | τ ω = i}.indicator (u i))
theorem measure_theory.stopped_process_eq'' {Ω : Type u_1} {ι : Type u_3} {τ : Ω ι} {E : Type u_4} {u : ι Ω E} [linear_order ι] [locally_finite_order_bot ι] [add_comm_monoid E] (n : ι) :
measure_theory.stopped_process u τ n = {a : Ω | n τ a}.indicator (u n) + (finset.Iio n).sum (λ (i : ι), {ω : Ω | τ ω = i}.indicator (u i))
theorem measure_theory.mem_ℒp_stopped_value_of_mem_finset {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} {μ : measure_theory.measure Ω} {τ : Ω ι} {E : Type u_4} {p : ennreal} {u : ι Ω E} [partial_order ι] {ℱ : measure_theory.filtration ι m} [normed_add_comm_group E] (hτ : measure_theory.is_stopping_time τ) (hu : (n : ι), measure_theory.mem_ℒp (u n) p μ) {s : finset ι} (hbdd : (ω : Ω), τ ω s) :
theorem measure_theory.mem_ℒp_stopped_value {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} {μ : measure_theory.measure Ω} {τ : Ω ι} {E : Type u_4} {p : ennreal} {u : ι Ω E} [partial_order ι] {ℱ : measure_theory.filtration ι m} [normed_add_comm_group E] [locally_finite_order_bot ι] (hτ : measure_theory.is_stopping_time τ) (hu : (n : ι), measure_theory.mem_ℒp (u n) p μ) {N : ι} (hbdd : (ω : Ω), τ ω N) :
theorem measure_theory.integrable_stopped_value_of_mem_finset {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} {μ : measure_theory.measure Ω} {τ : Ω ι} {E : Type u_4} {u : ι Ω E} [partial_order ι] {ℱ : measure_theory.filtration ι m} [normed_add_comm_group E] (hτ : measure_theory.is_stopping_time τ) (hu : (n : ι), measure_theory.integrable (u n) μ) {s : finset ι} (hbdd : (ω : Ω), τ ω s) :
theorem measure_theory.integrable_stopped_value {Ω : Type u_1} (ι : Type u_3) {m : measurable_space Ω} {μ : measure_theory.measure Ω} {τ : Ω ι} {E : Type u_4} {u : ι Ω E} [partial_order ι] {ℱ : measure_theory.filtration ι m} [normed_add_comm_group E] [locally_finite_order_bot ι] (hτ : measure_theory.is_stopping_time τ) (hu : (n : ι), measure_theory.integrable (u n) μ) {N : ι} (hbdd : (ω : Ω), τ ω N) :
theorem measure_theory.mem_ℒp_stopped_process_of_mem_finset {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} {μ : measure_theory.measure Ω} {τ : Ω ι} {E : Type u_4} {p : ennreal} {u : ι Ω E} [linear_order ι] [topological_space ι] [order_topology ι] [topological_space.first_countable_topology ι] {ℱ : measure_theory.filtration ι m} [normed_add_comm_group E] (hτ : measure_theory.is_stopping_time τ) (hu : (n : ι), measure_theory.mem_ℒp (u n) p μ) (n : ι) {s : finset ι} (hbdd : (ω : Ω), τ ω < n τ ω s) :
theorem measure_theory.integrable_stopped_process_of_mem_finset {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} {μ : measure_theory.measure Ω} {τ : Ω ι} {E : Type u_4} {u : ι Ω E} [linear_order ι] [topological_space ι] [order_topology ι] [topological_space.first_countable_topology ι] {ℱ : measure_theory.filtration ι m} [normed_add_comm_group E] (hτ : measure_theory.is_stopping_time τ) (hu : (n : ι), measure_theory.integrable (u n) μ) (n : ι) {s : finset ι} (hbdd : (ω : Ω), τ ω < n τ ω s) :

The stopped process of an adapted process with continuous paths is adapted.

If the indexing order has the discrete topology, then the stopped process of an adapted process is adapted.

Filtrations indexed by #

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 τ = λ (ω : Ω), (finset.Ico (τ ω) (π ω)).sum (λ (i : ), u (i + 1) - u i) ω
theorem measure_theory.stopped_value_sub_eq_sum' {Ω : Type u_1} {β : Type u_2} {u : Ω β} {τ π : Ω } [add_comm_group β] (hle : τ π) {N : } (hbdd : (ω : Ω), π ω N) :
measure_theory.stopped_value u π - measure_theory.stopped_value u τ = λ (ω : Ω), (finset.range (N + 1)).sum (λ (i : ), {ω : Ω | τ ω i i < π ω}.indicator (u (i + 1) - u i)) ω
theorem measure_theory.stopped_value_eq {Ω : Type u_1} {β : Type u_2} {u : Ω β} {τ : Ω } [add_comm_monoid β] {N : } (hbdd : (ω : Ω), τ ω N) :
measure_theory.stopped_value u τ = λ (x : Ω), (finset.range (N + 1)).sum (λ (i : ), {ω : Ω | τ ω = 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) + (finset.range n).sum (λ (i : ), {ω : Ω | τ ω = i}.indicator (u i))
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 + 1 τ a}.indicator (u n) + (finset.range (n + 1)).sum (λ (i : ), {a : Ω | τ a = i}.indicator (u i))
theorem measure_theory.is_stopping_time.piecewise_of_le {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] {𝒢 : measure_theory.filtration ι m} {τ η : Ω ι} {i : ι} {s : set Ω} [decidable_pred (λ (_x : Ω), _x s)] (hτ_st : measure_theory.is_stopping_time 𝒢 τ) (hη_st : measure_theory.is_stopping_time 𝒢 η) (hτ : (ω : Ω), i τ ω) (hη : (ω : Ω), i η ω) (hs : measurable_set s) :

Given stopping times τ and η which are bounded below, set.piecewise s τ η is also a stopping time with respect to the same filtration.

theorem measure_theory.is_stopping_time_piecewise_const {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] {𝒢 : measure_theory.filtration ι m} {i j : ι} {s : set Ω} [decidable_pred (λ (_x : Ω), _x s)] (hij : i j) (hs : measurable_set s) :
measure_theory.is_stopping_time 𝒢 (s.piecewise (λ (_x : Ω), i) (λ (_x : Ω), j))
theorem measure_theory.stopped_value_piecewise_const {Ω : Type u_1} {s : set Ω} [decidable_pred (λ (_x : Ω), _x s)] {ι' : Type u_2} {i j : ι'} {f : ι' Ω } :
measure_theory.stopped_value f (s.piecewise (λ (_x : Ω), i) (λ (_x : Ω), j)) = s.piecewise (f i) (f j)
theorem measure_theory.stopped_value_piecewise_const' {Ω : Type u_1} {s : set Ω} [decidable_pred (λ (_x : Ω), _x s)] {ι' : Type u_2} {i j : ι'} {f : ι' Ω } :
measure_theory.stopped_value f (s.piecewise (λ (_x : Ω), i) (λ (_x : Ω), j)) = s.indicator (f i) + s.indicator (f j)

Conditional expectation with respect to the σ-algebra generated by a stopping time #