# mathlibdocumentation

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 #

• 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-strongly measurable
• measure_theory.prog_measurable: 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 strongly measurable with respect to the product measurable_space structure where the σ-algebra used for α is f i.
• 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.is_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.is_stopping_time.measurable_space: the σ-algebra associated with a stopping time

## Main results #

• adapted.prog_measurable_of_continuous: a continuous adapted process is progressively measurable.
• prog_measurable.stopped_process: the stopped process of a progressively measurable process is progressively measurable.
• mem_ℒp_stopped_process: if a process belongs to ℒp at every time in ℕ, then its stopped process belongs to ℒp as well.

## 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 ι] :
(λ (_x : , ι →
Equations
@[protected]
theorem measure_theory.filtration.mono {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [preorder ι] {i j : ι} (f : 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 : m) (i : ι) :
f i m
@[protected, ext]
theorem measure_theory.filtration.ext {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [preorder ι] {f g : 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 : ι) :
hm') i = m'
@[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 : 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 : 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 ) (i : ι) :
(has_Sup.Sup s) i = has_Sup.Sup ((λ (f : , f i) '' s)
@[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 ) (i : ι) :
(has_Inf.Inf s) i = (has_Inf.Inf ((λ (f : , f i) '' s)) m
@[protected, instance]
noncomputable def measure_theory.filtration.complete_lattice {α : 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.

Instances of this typeclass
@[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 : ι) :
@[protected, instance]
def measure_theory.is_finite_measure.sigma_finite_filtration {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [preorder ι] (μ : measure_theory.measure α) (f : m)  :
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
• = ∀ (i : ι),
theorem measure_theory.adapted.add {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} [preorder ι] {u v : ι → α → β} {f : m} [has_add β] (hu : u) (hv : v) :
(u + v)
theorem measure_theory.adapted.neg {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} [preorder ι] {u : ι → α → β} {f : m} [add_group β] (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.prog_measurable {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} [preorder ι] (f : 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 α} [preorder ι] (f : m) (b : β) :
(λ (_x : ι) (_x : α), b)
@[protected]
theorem measure_theory.prog_measurable.adapted {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} [preorder ι] {u : ι → α → β} {f : m} (h : u) :
@[protected]
theorem measure_theory.prog_measurable.comp {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} [preorder ι] {u : ι → α → β} {f : m} {t : ι → α → ι} [borel_space ι] (h : u) (ht : t) (ht_le : ∀ (i : ι) (x : α), t i x i) :
(λ (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 α} [preorder ι] {u v : ι → α → β} {f : m} [has_mul β] (hu : u) (hv : v) :
(λ (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 α} [preorder ι] {u v : ι → α → β} {f : m} [has_add β] (hu : u) (hv : v) :
(λ (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 α} [preorder ι] {f : m} {γ : Type u_4} {U : γ → ι → α → β} {s : finset γ} (h : ∀ (c : γ), c s) :
(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 α} [preorder ι] {f : m} {γ : Type u_4} [comm_monoid β] {U : γ → ι → α → β} {s : finset γ} (h : ∀ (c : γ), c s) :
(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 α} [preorder ι] {f : m} {γ : Type u_4} {U : γ → ι → α → β} {s : finset γ} (h : ∀ (c : γ), c s) :
(λ (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 α} [preorder ι] {f : m} {γ : Type u_4} [comm_monoid β] {U : γ → ι → α → β} {s : finset γ} (h : ∀ (c : γ), c s) :
(λ (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 α} [preorder ι] {u : ι → α → β} {f : m} [add_group β] (hu : u) :
(λ (i : ι) (x : α), -u i x)
@[protected]
theorem measure_theory.prog_measurable.inv {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} [preorder ι] {u : ι → α → β} {f : m} [group β] (hu : u) :
(λ (i : ι) (x : α), (u i x)⁻¹)
@[protected]
theorem measure_theory.prog_measurable.div {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} [preorder ι] {u v : ι → α → β} {f : m} [group β] (hu : u) (hv : v) :
(λ (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 α} [preorder ι] {u v : ι → α → β} {f : m} [add_group β] (hu : u) (hv : v) :
(λ (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 α} [preorder ι] {u : ι → α → β} {f : m} {γ : Type u_4} (fltr : filter γ) [fltr.ne_bot] [fltr.is_countably_generated] {U : γ → ι → α → β} (h : ∀ (l : γ), ) (h_tendsto : fltr (nhds u)) :
theorem measure_theory.prog_measurable_of_tendsto {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} [preorder ι] {u : ι → α → β} {f : m} {U : ι → α → β} (h : ∀ (l : ), ) (h_tendsto : (nhds u)) :
theorem measure_theory.adapted.prog_measurable_of_continuous {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} [preorder ι] {u : ι → α → β} {f : m} (h : u) (hu_cont : ∀ (x : α), continuous (λ (i : ι), u i x)) :

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 α} [mβ : measurable_space β] [borel_space β] [preorder ι] (u : ι → α → β) (hum : ∀ (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 α} [mβ : measurable_space β] [borel_space β] [preorder ι] {u : ι → α → β} (hum : ∀ (i : ι), ) :

### Stopping times #

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_const {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [preorder ι] (f : m) (i : ι) :
(λ (x : α), i)
@[protected]
theorem measure_theory.is_stopping_time.measurable_set_le {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [preorder ι] {f : m} {τ : α → ι} (hτ : τ) (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 : m} {τ : α → ι} [pred_order ι] (hτ : τ) (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 : m} {τ : α → ι} (hτ : τ) (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 : m} {τ : α → ι} (hτ : τ) (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 : m} {τ : α → ι} (hτ : τ) (i : ι) :
measurable_set {x : α | τ x < i}
theorem measure_theory.is_stopping_time.measurable_set_ge {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [linear_order ι] {f : m} {τ : α → ι} (hτ : τ) (i : ι) :
measurable_set {x : α | i τ x}
theorem measure_theory.is_stopping_time.measurable_set_eq {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [linear_order ι] {f : m} {τ : α → ι} (hτ : τ) (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 : m} {τ : α → ι} (hτ : τ) {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 : 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} {ι : Type u_3} {m : measurable_space α} [preorder ι] [encodable ι] {f : 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 : m} {τ π : α → ι} (hτ : τ) (hπ : π) :
(λ (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 : m} {τ : α → ι} (hτ : τ) (i : ι) :
(λ (x : α), linear_order.max (τ x) i)
@[protected]
theorem measure_theory.is_stopping_time.min {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [linear_order ι] {f : m} {τ π : α → ι} (hτ : τ) (hπ : π) :
(λ (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 : m} {τ : α → ι} (hτ : τ) (i : ι) :
(λ (x : α), linear_order.min (τ x) i)
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)
theorem measure_theory.is_stopping_time.add_const_nat {α : Type u_1} {m : measurable_space α} {f : m} {τ : α → } (hτ : τ) {i : } :
(λ (x : α), τ x + i)
theorem measure_theory.is_stopping_time.add {α : Type u_1} {m : measurable_space α} {f : m} {τ π : α → } (hτ : τ) (hπ : π) :
+ π)
@[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_of_encodable {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [preorder ι] {f : m} {τ : α → ι} [encodable ι] (hτ : τ) :
theorem measure_theory.is_stopping_time.measurable_space_le' {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [preorder ι] {f : m} {τ : α → ι} (hτ : τ) :
theorem measure_theory.is_stopping_time.measurable_space_le {α : Type u_1} {m : measurable_space α} {ι : Type u_2} {f : m} {τ : α → ι} (hτ : τ) :
@[simp]
theorem measure_theory.is_stopping_time.measurable_space_const {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [preorder ι] (f : m) (i : ι) :
theorem measure_theory.is_stopping_time.measurable_set_inter_eq_iff {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [preorder ι] {f : m} {τ : α → ι} (hτ : τ) (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 : m} {τ : α → ι} (hτ : τ) {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 : m} {τ : α → ι} (hτ : τ) {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 : m} {τ : α → ι} (hτ : τ) (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 : m} {τ : α → ι} (hτ : τ) (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 : m} {τ : α → ι} (hτ : τ) (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 : m} {τ : α → ι} (hτ : τ) (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 : m} {τ : α → ι} (hτ : τ) (i : ι) :
measurable_set {x : α | τ x < i}
@[protected]
theorem measure_theory.is_stopping_time.measurable {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [linear_order ι] {f : m} {τ : α → ι} [borel_space ι] (hτ : τ) :
@[protected]
theorem measure_theory.is_stopping_time.measurable_of_le {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [linear_order ι] {f : m} {τ : α → ι} [borel_space ι] (hτ : τ) {i : ι} (hτ_le : ∀ (x : α), τ x i) :
theorem measure_theory.is_stopping_time.measurable_space_min {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [linear_order ι] {f : m} {τ π : α → ι} (hτ : τ) (hπ : π) :
theorem measure_theory.is_stopping_time.measurable_set_min_iff {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [linear_order ι] {f : m} {τ π : α → ι} (hτ : τ) (hπ : π) (s : set α) :
theorem measure_theory.is_stopping_time.measurable_space_min_const {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [linear_order ι] {f : m} {τ : α → ι} (hτ : τ) {i : ι} :
theorem measure_theory.is_stopping_time.measurable_set_min_const_iff {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [linear_order ι] {f : m} {τ : α → ι} (hτ : τ) (s : set α) {i : ι} :
theorem measure_theory.is_stopping_time.measurable_set_inter_le {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [linear_order ι] {f : m} {τ π : α → ι} [borel_space ι] (hτ : τ) (hπ : π) (s : set α) (hs : measurable_set s) :
measurable_set (s {x : α | τ x π x})
theorem measure_theory.is_stopping_time.measurable_set_inter_le_iff {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [linear_order ι] {f : m} {τ π : α → ι} [borel_space ι] (hτ : τ) (hπ : π) (s : set α) :
measurable_set (s {x : α | τ x π x}) measurable_set (s {x : α | τ x π x})
theorem measure_theory.is_stopping_time.measurable_set_le_stopping_time {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [linear_order ι] {f : m} {τ π : α → ι} [borel_space ι] (hτ : τ) (hπ : π) :
measurable_set {x : α | τ x π x}
theorem measure_theory.is_stopping_time.measurable_set_stopping_time_le {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [linear_order ι] {f : m} {τ π : α → ι} [borel_space ι] (hτ : τ) (hπ : π) :
measurable_set {x : α | τ x π x}
theorem measure_theory.is_stopping_time.measurable_set_eq_stopping_time {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [linear_order ι] {f : m} {τ π : α → ι} [add_group ι] [borel_space ι] (hτ : τ) (hπ : π) :
measurable_set {x : α | τ x = π x}
theorem measure_theory.is_stopping_time.measurable_set_eq_stopping_time_of_encodable {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [linear_order ι] {f : m} {τ π : α → ι} [encodable ι] [borel_space ι] (hτ : τ) (hπ : π) :
measurable_set {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
• = λ (x : α), u (τ x) x
theorem measure_theory.stopped_value_const {α : Type u_1} {β : Type u_2} {ι : Type u_3} (u : ι → α → β) (i : ι) :
(λ (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
• = λ (i : ι) (x : α), u (τ 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.prog_measurable_min_stopping_time {α : Type u_1} {ι : Type u_3} {m : measurable_space α} [linear_order ι] [borel_space ι] {τ : α → ι} {f : m} (hτ : τ) :
(λ (i : ι) (x : α), (τ x))
theorem measure_theory.prog_measurable.stopped_process {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} [linear_order ι] [borel_space ι] {u : ι → α → β} {τ : α → ι} {f : m} (h : u) (hτ : τ) :
theorem measure_theory.prog_measurable.adapted_stopped_process {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} [linear_order ι] [borel_space ι] {u : ι → α → β} {τ : α → ι} {f : m} (h : u) (hτ : τ) :
theorem measure_theory.prog_measurable.strongly_measurable_stopped_process {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} [linear_order ι] [borel_space ι] {u : ι → α → β} {τ : α → ι} {f : m} (hu : u) (hτ : τ) (i : ι) :
theorem measure_theory.strongly_measurable_stopped_value_of_le {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} [linear_order ι] [borel_space ι] {u : ι → α → β} {τ : α → ι} {f : m} (h : u) (hτ : τ) {n : ι} (hτ_le : ∀ (x : α), τ x n) :
theorem measure_theory.measurable_stopped_value {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} [linear_order ι] [borel_space ι] {u : ι → α → β} {τ : α → ι} {f : m} [borel_space β] (hf_prog : u) (hτ : τ) :

### Filtrations indexed by ℕ#

theorem measure_theory.stopped_value_sub_eq_sum {α : Type u_1} {β : Type u_2} {u : α → β} {τ π : α → } (hle : τ π) :
= λ (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 : α → β} {τ π : α → } (hle : τ π) {N : } (hbdd : ∀ (x : α), π x N) :
= λ (x : α), (finset.range (N + 1)).sum (λ (i : ), {x : α | τ x i i < π x}.indicator (u (i + 1) - u i)) x
theorem measure_theory.adapted.prog_measurable_of_nat {α : Type u_1} {β : Type u_2} {m : measurable_space α} {f : m} {u : α → β} (h : u) :

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.

theorem measure_theory.adapted.stopped_process_of_nat {α : Type u_1} {β : Type u_2} {m : measurable_space α} {f : m} {u : α → β} {τ : α → } (hu : u) (hτ : τ) :

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

theorem measure_theory.adapted.strongly_measurable_stopped_process_of_nat {α : Type u_1} {β : Type u_2} {m : measurable_space α} {f : m} {u : α → β} {τ : α → } (hτ : τ) (hu : u) (n : ) :
theorem measure_theory.stopped_value_eq {α : Type u_1} {β : Type u_2} {u : α → β} {τ : α → } {N : } (hbdd : ∀ (x : α), τ x N) :
= λ (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 : α → β} {τ : α → } (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 : m} {u : α → β} {τ : α → } [normed_group β] {p : ennreal} {μ : 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 β] {μ : 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 : ennreal} {μ : 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 β] {μ : measure_theory.measure α} (hτ : τ) (hu : ∀ (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 ι] {𝒢 : m} {τ η : α → ι} {i : ι} {s : set α} [decidable_pred (λ (_x : α), _x s)] (hτ_st : τ) (hη_st : η) (hτ : ∀ (x : α), i τ x) (hη : ∀ (x : α), i η x) (hs : measurable_set s) :
(s.piecewise τ η)

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 ι] {𝒢 : m} {i j : ι} {s : set α} [decidable_pred (λ (_x : α), _x s)] (hij : i j) (hs : measurable_set s) :
(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 : ι' → α → } :
(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 : ι' → α → } :
(s.piecewise (λ (_x : α), i) (λ (_x : α), j)) = s.indicator (f i) + s.indicator (f j)