mathlib documentation

probability.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 #

Main results #

Tags #

filtration, stopping time, stochastic process

Filtrations #

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 sub-σ-algebras of m.

Instances for measure_theory.filtration
@[protected, instance]
def measure_theory.filtration.has_coe_to_fun {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [preorder ι] :
Equations
@[protected]
theorem measure_theory.filtration.mono {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [preorder ι] {i j : ι} (f : measure_theory.filtration ι m) (hij : i j) :
f i f j
@[protected]
theorem measure_theory.filtration.le {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [preorder ι] (f : measure_theory.filtration ι m) (i : ι) :
f i m
@[protected, ext]
theorem measure_theory.filtration.ext {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [preorder ι] {f g : measure_theory.filtration ι m} (h : f = g) :
f = g
def measure_theory.filtration.const {α : Type u_1} (ι : Type u_3) {m : measurable_space α} [preorder ι] (m' : measurable_space α) (hm' : m' m) :

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

Equations
@[simp]
theorem measure_theory.filtration.const_apply {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [preorder ι] {m' : measurable_space α} {hm' : m' m} (i : ι) :
@[protected, instance]
def measure_theory.filtration.inhabited {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [preorder ι] :
Equations
@[protected, instance]
def measure_theory.filtration.has_le {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [preorder ι] :
Equations
@[protected, instance]
def measure_theory.filtration.has_bot {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [preorder ι] :
Equations
@[protected, instance]
def measure_theory.filtration.has_top {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [preorder ι] :
Equations
@[protected, instance]
def measure_theory.filtration.has_sup {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [preorder ι] :
Equations
@[norm_cast]
theorem measure_theory.filtration.coe_fn_sup {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [preorder ι] {f g : measure_theory.filtration ι m} :
(f g) = f g
@[protected, instance]
def measure_theory.filtration.has_inf {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [preorder ι] :
Equations
@[norm_cast]
theorem measure_theory.filtration.coe_fn_inf {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [preorder ι] {f g : measure_theory.filtration ι m} :
(f g) = f g
@[protected, instance]
def measure_theory.filtration.has_Sup {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [preorder ι] :
Equations
theorem measure_theory.filtration.Sup_def {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [preorder ι] (s : set (measure_theory.filtration ι m)) (i : ι) :
@[protected, instance]
noncomputable def measure_theory.filtration.has_Inf {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [preorder ι] :
Equations
theorem measure_theory.filtration.Inf_def {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [preorder ι] (s : set (measure_theory.filtration ι m)) (i : ι) :
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.

Instances of this typeclass
@[protected, instance]
def measure_theory.adapted {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} [topological_space β] [preorder ι] (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 α} [topological_space β] [preorder ι] {u v : ι → α → β} {f : measure_theory.filtration ι m} [has_add β] [has_continuous_add β] (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 α} [topological_space β] [preorder ι] {u : ι → α → β} {f : measure_theory.filtration ι m} [add_group β] [topological_add_group β] (hu : measure_theory.adapted f u) :
theorem measure_theory.adapted.smul {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} [topological_space β] [preorder ι] {u : ι → α → β} {f : measure_theory.filtration ι m} [has_scalar β] [has_continuous_smul β] (c : ) (hu : measure_theory.adapted f u) :
theorem measure_theory.adapted_zero {α : Type u_1} (β : Type u_2) {ι : Type u_3} {m : measurable_space α} [topological_space β] [preorder ι] [has_zero β] (f : measure_theory.filtration ι m) :
def measure_theory.prog_measurable {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} [topological_space β] [preorder ι] [measurable_space ι] (f : measure_theory.filtration ι m) (u : ι → α → β) :
Prop

Progressively measurable process. A sequence of functions u is said to be progressively measurable with respect to a filtration f if at each point in time i, u restricted to set.Iic i × α is measurable with respect to the product measurable_space structure where the σ-algebra used for α is f i. The usual definition uses the interval [0,i], which we replace by set.Iic i. We recover the usual definition for index types ℝ≥0 or .

Equations
theorem measure_theory.prog_measurable_const {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} [topological_space β] [preorder ι] [measurable_space ι] (f : measure_theory.filtration ι m) (b : β) :
measure_theory.prog_measurable f (λ (_x : ι) (_x : α), b)
@[protected]
theorem measure_theory.prog_measurable.adapted {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} [topological_space β] [preorder ι] {u : ι → α → β} {f : measure_theory.filtration ι m} [measurable_space ι] (h : measure_theory.prog_measurable f u) :
@[protected]
theorem measure_theory.prog_measurable.comp {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} [topological_space β] [preorder ι] {u : ι → α → β} {f : measure_theory.filtration ι m} [measurable_space ι] {t : ι → α → ι} [topological_space ι] [borel_space ι] [topological_space.metrizable_space ι] (h : measure_theory.prog_measurable f u) (ht : measure_theory.prog_measurable f t) (ht_le : ∀ (i : ι) (x : α), t i x i) :
measure_theory.prog_measurable f (λ (i : ι) (x : α), u (t i x) x)
@[protected]
theorem measure_theory.prog_measurable.mul {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} [topological_space β] [preorder ι] {u v : ι → α → β} {f : measure_theory.filtration ι m} [measurable_space ι] [has_mul β] [has_continuous_mul β] (hu : measure_theory.prog_measurable f u) (hv : measure_theory.prog_measurable f v) :
measure_theory.prog_measurable f (λ (i : ι) (x : α), u i x * v i x)
@[protected]
theorem measure_theory.prog_measurable.add {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} [topological_space β] [preorder ι] {u v : ι → α → β} {f : measure_theory.filtration ι m} [measurable_space ι] [has_add β] [has_continuous_add β] (hu : measure_theory.prog_measurable f u) (hv : measure_theory.prog_measurable f v) :
measure_theory.prog_measurable f (λ (i : ι) (x : α), u i x + v i x)
@[protected]
theorem measure_theory.prog_measurable.finset_sum' {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} [topological_space β] [preorder ι] {f : measure_theory.filtration ι m} [measurable_space ι] {γ : Type u_4} [add_comm_monoid β] [has_continuous_add β] {U : γ → ι → α → β} {s : finset γ} (h : ∀ (c : γ), c smeasure_theory.prog_measurable f (U c)) :
measure_theory.prog_measurable f (s.sum (λ (c : γ), U c))
@[protected]
theorem measure_theory.prog_measurable.finset_prod' {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} [topological_space β] [preorder ι] {f : measure_theory.filtration ι m} [measurable_space ι] {γ : Type u_4} [comm_monoid β] [has_continuous_mul β] {U : γ → ι → α → β} {s : finset γ} (h : ∀ (c : γ), c smeasure_theory.prog_measurable f (U c)) :
measure_theory.prog_measurable f (s.prod (λ (c : γ), U c))
@[protected]
theorem measure_theory.prog_measurable.finset_sum {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} [topological_space β] [preorder ι] {f : measure_theory.filtration ι m} [measurable_space ι] {γ : Type u_4} [add_comm_monoid β] [has_continuous_add β] {U : γ → ι → α → β} {s : finset γ} (h : ∀ (c : γ), c smeasure_theory.prog_measurable f (U c)) :
measure_theory.prog_measurable f (λ (i : ι) (a : α), s.sum (λ (c : γ), U c i a))
@[protected]
theorem measure_theory.prog_measurable.finset_prod {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} [topological_space β] [preorder ι] {f : measure_theory.filtration ι m} [measurable_space ι] {γ : Type u_4} [comm_monoid β] [has_continuous_mul β] {U : γ → ι → α → β} {s : finset γ} (h : ∀ (c : γ), c smeasure_theory.prog_measurable f (U c)) :
measure_theory.prog_measurable f (λ (i : ι) (a : α), s.prod (λ (c : γ), U c i a))
@[protected]
theorem measure_theory.prog_measurable.neg {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} [topological_space β] [preorder ι] {u : ι → α → β} {f : measure_theory.filtration ι m} [measurable_space ι] [add_group β] [topological_add_group β] (hu : measure_theory.prog_measurable f u) :
measure_theory.prog_measurable f (λ (i : ι) (x : α), -u i x)
@[protected]
theorem measure_theory.prog_measurable.inv {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} [topological_space β] [preorder ι] {u : ι → α → β} {f : measure_theory.filtration ι m} [measurable_space ι] [group β] [topological_group β] (hu : measure_theory.prog_measurable f u) :
measure_theory.prog_measurable f (λ (i : ι) (x : α), (u i x)⁻¹)
@[protected]
theorem measure_theory.prog_measurable.div {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} [topological_space β] [preorder ι] {u v : ι → α → β} {f : measure_theory.filtration ι m} [measurable_space ι] [group β] [topological_group β] (hu : measure_theory.prog_measurable f u) (hv : measure_theory.prog_measurable f v) :
measure_theory.prog_measurable f (λ (i : ι) (x : α), u i x / v i x)
@[protected]
theorem measure_theory.prog_measurable.sub {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} [topological_space β] [preorder ι] {u v : ι → α → β} {f : measure_theory.filtration ι m} [measurable_space ι] [add_group β] [topological_add_group β] (hu : measure_theory.prog_measurable f u) (hv : measure_theory.prog_measurable f v) :
measure_theory.prog_measurable f (λ (i : ι) (x : α), u i x - v i x)
theorem measure_theory.prog_measurable_of_tendsto' {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} [topological_space β] [preorder ι] {u : ι → α → β} {f : measure_theory.filtration ι m} {γ : Type u_4} [measurable_space ι] [topological_space.metrizable_space β] (fltr : filter γ) [fltr.ne_bot] [fltr.is_countably_generated] {U : γ → ι → α → β} (h : ∀ (l : γ), measure_theory.prog_measurable f (U l)) (h_tendsto : filter.tendsto U fltr (nhds u)) :
theorem measure_theory.prog_measurable_of_tendsto {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} [topological_space β] [preorder ι] {u : ι → α → β} {f : measure_theory.filtration ι m} [measurable_space ι] [topological_space.metrizable_space β] {U : ι → α → β} (h : ∀ (l : ), measure_theory.prog_measurable f (U l)) (h_tendsto : filter.tendsto U filter.at_top (nhds u)) :

A continuous and adapted process is progressively measurable.

def measure_theory.filtration.natural {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} [topological_space β] [topological_space.metrizable_space β] [mβ : measurable_space β] [borel_space β] [preorder ι] (u : ι → α → β) (hum : ∀ (i : ι), measure_theory.strongly_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 α} [topological_space β] [topological_space.metrizable_space β] [mβ : measurable_space β] [borel_space β] [preorder ι] {u : ι → α → β} (hum : ∀ (i : ι), measure_theory.strongly_measurable (u i)) :

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 {x : α | τ x 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 {x : α | τ x < 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 {x : α | i < τ x}
theorem measure_theory.is_stopping_time.measurable_set_lt_of_is_lub {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [linear_order ι] {f : measure_theory.filtration ι m} {τ : α → ι} [topological_space ι] [order_topology ι] [topological_space.first_countable_topology ι] (hτ : measure_theory.is_stopping_time f τ) (i : ι) (h_lub : is_lub (set.Iio i) i) :
measurable_set {x : α | τ x < i}

Auxiliary lemma for is_stopping_time.measurable_set_lt.

theorem measure_theory.is_stopping_time.measurable_set_lt {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [linear_order ι] {f : measure_theory.filtration ι m} {τ : α → ι} [topological_space ι] [order_topology ι] [topological_space.first_countable_topology ι] (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} {ι : Type u_3} {m : measurable_space α} [linear_order ι] {f : measure_theory.filtration ι m} {τ : α → ι} [topological_space ι] [order_topology ι] [topological_space.first_countable_topology ι] (hτ : measure_theory.is_stopping_time f τ) (i : ι) :
measurable_set {x : α | τ x = i}
theorem measure_theory.is_stopping_time.measurable_set_eq_le {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [linear_order ι] {f : measure_theory.filtration ι m} {τ : α → ι} [topological_space ι] [order_topology ι] [topological_space.first_countable_topology ι] (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_le {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [linear_order ι] {f : measure_theory.filtration ι m} {τ : α → ι} [topological_space ι] [order_topology ι] [topological_space.first_countable_topology ι] (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} {ι : Type u_3} {m : measurable_space α} [preorder ι] [encodable ι] {f : measure_theory.filtration ι m} {τ : α → ι} (hτ : ∀ (i : ι), measurable_set {x : α | τ x = 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 (λ (x : α), linear_order.max (τ x) (π x))
@[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 (λ (x : α), linear_order.min (τ x) (π x))
@[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 : ι) :
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)
theorem measure_theory.is_stopping_time.add_const_nat {α : Type u_1} {m : measurable_space α} {f : measure_theory.filtration m} {τ : α → } (hτ : measure_theory.is_stopping_time f τ) {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_of_encodable {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [preorder ι] {f : measure_theory.filtration ι m} {τ : α → ι} [encodable ι] (hτ : measure_theory.is_stopping_time f τ) :
@[simp]
theorem measure_theory.is_stopping_time.measurable_space_const {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [preorder ι] (f : measure_theory.filtration ι m) (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 {x : α | τ x = i}) measurable_set (s {x : α | τ x = 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 : ∀ (x : α), τ x i) :
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 : ∀ (x : α), i τ x) :
@[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 {x : α | τ x 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 {x : α | i < τ x}
@[protected]
theorem measure_theory.is_stopping_time.measurable_set_eq' {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [linear_order ι] {f : measure_theory.filtration ι m} {τ : α → ι} [topological_space ι] [order_topology ι] [topological_space.first_countable_topology ι] (hτ : measure_theory.is_stopping_time f τ) (i : ι) :
measurable_set {x : α | τ x = i}
@[protected]
theorem measure_theory.is_stopping_time.measurable_set_ge' {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [linear_order ι] {f : measure_theory.filtration ι m} {τ : α → ι} [topological_space ι] [order_topology ι] [topological_space.first_countable_topology ι] (hτ : measure_theory.is_stopping_time f τ) (i : ι) :
measurable_set {x : α | i τ x}
@[protected]
theorem measure_theory.is_stopping_time.measurable_set_lt' {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [linear_order ι] {f : measure_theory.filtration ι m} {τ : α → ι} [topological_space ι] [order_topology ι] [topological_space.first_countable_topology ι] (hτ : measure_theory.is_stopping_time f τ) (i : ι) :
measurable_set {x : α | τ x < i}
@[protected]
theorem measure_theory.is_stopping_time.measurable_of_le {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [linear_order ι] {f : measure_theory.filtration ι m} {τ : α → ι} [topological_space ι] [measurable_space ι] [borel_space ι] [order_topology ι] [topological_space.second_countable_topology ι] (hτ : measure_theory.is_stopping_time f τ) {i : ι} (hτ_le : ∀ (x : α), τ x i) :
theorem measure_theory.is_stopping_time.measurable_space_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 : ι} :
theorem measure_theory.is_stopping_time.measurable_set_min_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 : ι} :
theorem measure_theory.is_stopping_time.measurable_set_inter_le_iff {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [linear_order ι] {f : measure_theory.filtration ι m} {τ π : α → ι} [topological_space ι] [topological_space.second_countable_topology ι] [order_topology ι] [measurable_space ι] [borel_space ι] (hτ : measure_theory.is_stopping_time f τ) (hπ : measure_theory.is_stopping_time f π) (s : set α) :
measurable_set (s {x : α | τ x π x}) measurable_set (s {x : α | τ x π x})

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

Equations
theorem measure_theory.stopped_value_const {α : Type u_1} {β : Type u_2} {ι : Type u_3} (u : ι → α → β) (i : ι) :
measure_theory.stopped_value u (λ (x : α), 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 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.strongly_measurable_stopped_value_of_le {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} [linear_order ι] [measurable_space ι] [topological_space ι] [order_topology ι] [topological_space.second_countable_topology ι] [borel_space ι] [topological_space β] {u : ι → α → β} {τ : α → ι} {f : measure_theory.filtration ι m} (h : measure_theory.prog_measurable f u) (hτ : measure_theory.is_stopping_time f τ) {n : ι} (hτ_le : ∀ (x : α), τ x n) :

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 τ = λ (x : α), (finset.Ico (τ x) (π x)).sum (λ (i : ), 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 : α), (finset.range (N + 1)).sum (λ (i : ), {x : α | τ x i i < π x}.indicator (u (i + 1) - u i)) x

For filtrations indexed by , adapted and prog_measurable are equivalent. This lemma provides adapted f u → prog_measurable f u. See prog_measurable.adapted for the reverse direction, which is true more generally.

For filtrations indexed by , the stopped process obtained from an adapted process is adapted.

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 : α), (finset.range (N + 1)).sum (λ (i : ), {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) + (finset.range n).sum (λ (i : ), {a : α | τ a = i}.indicator (u i))
theorem measure_theory.mem_ℒp_stopped_process {α : Type u_1} {β : Type u_2} {m : measurable_space α} {f : measure_theory.filtration m} {u : α → β} {τ : α → } [normed_group β] {p : ennreal} {μ : 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 : α → β} {τ : α → } [normed_group β] {μ : 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 : α → β} {τ : α → } [normed_group β] {p : ennreal} {μ : 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 : α → β} {τ : α → } [normed_group β] {μ : measure_theory.measure α} (hτ : measure_theory.is_stopping_time f τ) (hu : ∀ (n : ), measure_theory.integrable (u n) μ) {N : } (hbdd : ∀ (x : α), τ x N) :
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τ : ∀ (x : α), i τ x) (hη : ∀ (x : α), i η x) (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)