mathlib3documentation

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 #

• `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 #

• `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 #

stopping time, stochastic process

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 : ι) :
(λ (ω : Ω), 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 {ω : Ω | τ ω 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 {ω : Ω | τ ω < i}
@[protected]
theorem measure_theory.is_stopping_time.measurable_set_eq_of_countable_range {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} {τ : Ω ι} {f : m} (hτ : τ) (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 Ω} {τ : Ω ι} {f : m} [countable ι] (hτ : τ) (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 Ω} {τ : Ω ι} {f : m} (hτ : τ) (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 Ω} {τ : Ω ι} {f : m} [countable ι] (hτ : τ) (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 : m} (hτ : τ) (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 : m} [countable ι] (hτ : τ) (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 : m} {τ : Ω ι} (hτ : τ) (i : ι) :
measurable_set {ω : Ω | i < τ ω}
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 {ω : Ω | τ ω < 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 {ω : Ω | τ ω < 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 {ω : Ω | i τ ω}
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 {ω : Ω | τ ω = 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 {ω : Ω | τ ω = 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 {ω : Ω | τ ω < i}
theorem measure_theory.is_stopping_time_of_measurable_set_eq {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] [countable ι] {f : 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 : m} {τ π : Ω ι} (hτ : τ) (hπ : π) :
(λ (ω : Ω), linear_order.max (τ ω) (π ω))
@[protected]
theorem measure_theory.is_stopping_time.max_const {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [linear_order ι] {f : m} {τ : Ω ι} (hτ : τ) (i : ι) :
(λ (ω : Ω), linear_order.max (τ ω) i)
@[protected]
theorem measure_theory.is_stopping_time.min {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [linear_order ι] {f : m} {τ π : Ω ι} (hτ : τ) (hπ : π) :
(λ (ω : Ω), linear_order.min (τ ω) (π ω))
@[protected]
theorem measure_theory.is_stopping_time.min_const {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [linear_order ι] {f : m} {τ : Ω ι} (hτ : τ) (i : ι) :
(λ (ω : Ω), linear_order.min (τ ω) 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) :
(λ (ω : Ω), τ ω + i)
theorem measure_theory.is_stopping_time.add_const_nat {Ω : Type u_1} {m : measurable_space Ω} {f : m} {τ : Ω } (hτ : τ) {i : } :
(λ (ω : Ω), τ ω + 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 {ω : Ω | τ ω 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_countable {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] {f : m} {τ : Ω ι} [countable ι] (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 {ω : Ω | τ ω = 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 : m} {τ : Ω ι} (hτ : τ) {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 : m} {τ : Ω ι} (hτ : τ) {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 : m} {τ : Ω ι} (hτ : τ) {i : ι} (hτ_le : (ω : Ω), i τ ω) :
@[protected, instance]
def measure_theory.is_stopping_time.sigma_finite_stopping_time {Ω : Type u_1} {m : measurable_space Ω} {ι : Type u_2} [order_bot ι] {μ : measure_theory.measure Ω} {f : m} {τ : Ω ι} (hτ : τ) :
@[protected, instance]
def measure_theory.is_stopping_time.sigma_finite_stopping_time_of_le {Ω : Type u_1} {m : measurable_space Ω} {ι : Type u_2} [order_bot ι] {μ : measure_theory.measure Ω} {f : m} {τ : Ω ι} (hτ : τ) {n : ι} (hτ_le : (ω : Ω), τ ω n) :
@[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 {ω : Ω | τ ω 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 {ω : Ω | i < τ ω}
@[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 {ω : Ω | τ ω = 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 {ω : Ω | i τ ω}
@[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 {ω : Ω | τ ω < 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 : m} {τ : Ω ι} (hτ : τ) (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 : m} {τ : Ω ι} [countable ι] (hτ : τ) (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 : m} {τ : Ω ι} (hτ : τ) (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 : m} {τ : Ω ι} [countable ι] (hτ : τ) (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 : m} {τ : Ω ι} (hτ : τ) (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 : m} {τ : Ω ι} [countable ι] (hτ : τ) (i : ι) :
measurable_set {ω : Ω | τ ω < i}
@[protected]
theorem measure_theory.is_stopping_time.measurable_space_le_of_countable_range {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [linear_order ι] {f : m} {τ : Ω ι} (hτ : τ) (h_countable : (set.range τ).countable) :
@[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 : (ω : Ω), τ ω 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 {ω : Ω | τ ω π ω})
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 {ω : Ω | τ ω π ω}) measurable_set (s {ω : Ω | τ ω π ω})
theorem measure_theory.is_stopping_time.measurable_set_inter_le_const_iff {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [linear_order ι] {f : m} {τ : Ω ι} (hτ : τ) (s : set Ω) (i : ι) :
measurable_set (s {ω : Ω | τ ω i}) measurable_set (s {ω : Ω | τ ω i})
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 {ω : Ω | τ ω π ω}
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 {ω : Ω | τ ω π ω}
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 {ω : Ω | τ ω = π ω}
theorem measure_theory.is_stopping_time.measurable_set_eq_stopping_time_of_countable {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [linear_order ι] {f : m} {τ π : Ω ι} [countable ι] [borel_space ι] (hτ : τ) (hπ : π) :
measurable_set {ω : Ω | τ ω = π ω}

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
• = λ (ω : Ω), u (τ ω) ω
theorem measure_theory.stopped_value_const {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} (u : ι Ω β) (i : ι) :
(λ (ω : Ω), 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
• = λ (i : ι) (ω : Ω), u (τ ω)) ω
theorem measure_theory.stopped_process_eq_stopped_value {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [linear_order ι] {u : ι Ω β} {τ : Ω ι} :
= λ (i : ι), (λ (ω : Ω), (τ ω))
theorem measure_theory.stopped_value_stopped_process {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [linear_order ι] {u : ι Ω β} {τ σ : Ω ι} :
= (λ (ω : Ω), linear_order.min (σ ω) (τ ω))
theorem measure_theory.stopped_process_eq_of_le {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [linear_order ι] {u : ι Ω β} {τ : Ω ι} {i : ι} {ω : Ω} (h : i τ ω) :
= u i ω
theorem measure_theory.stopped_process_eq_of_ge {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [linear_order ι] {u : ι Ω β} {τ : Ω ι} {i : ι} {ω : Ω} (h : τ ω i) :
= u (τ ω) ω
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 : ι) (ω : Ω), (τ ω))
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 : (ω : Ω), τ ω 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τ : τ) :
theorem measure_theory.stopped_value_eq_of_mem_finset {Ω : Type u_1} {ι : Type u_3} {τ : Ω ι} {E : Type u_4} {u : ι Ω E} {s : finset ι} (hbdd : (ω : Ω), τ ω s) :
= 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 ι] {N : ι} (hbdd : (ω : Ω), τ ω N) :
= (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 ι] {s : finset ι} (n : ι) (hbdd : (ω : Ω), τ ω < n τ ω s) :
= {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 ι] (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} {ℱ : m} (hτ : τ) (hu : (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} {ℱ : m} (hτ : τ) (hu : (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} {ℱ : m} (hτ : τ) (hu : (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} {ℱ : m} (hτ : τ) (hu : (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 ι] {ℱ : m} (hτ : τ) (hu : (n : ι), p μ) (n : ι) {s : finset ι} (hbdd : (ω : Ω), τ ω < n τ ω s) :
theorem measure_theory.mem_ℒp_stopped_process {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} {μ : measure_theory.measure Ω} {τ : Ω ι} {E : Type u_4} {p : ennreal} {u : ι Ω E} [linear_order ι] {ℱ : m} (hτ : τ) (hu : (n : ι), p μ) (n : ι) :
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 ι] {ℱ : m} (hτ : τ) (hu : (n : ι), μ) (n : ι) {s : finset ι} (hbdd : (ω : Ω), τ ω < n τ ω s) :
theorem measure_theory.integrable_stopped_process {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} {μ : measure_theory.measure Ω} {τ : Ω ι} {E : Type u_4} {u : ι Ω E} [linear_order ι] {ℱ : m} (hτ : τ) (hu : (n : ι), μ) (n : ι) :
theorem measure_theory.adapted.stopped_process {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space Ω} [linear_order ι] [borel_space ι] {f : m} {u : ι Ω β} {τ : Ω ι} (hu : u) (hu_cont : (ω : Ω), continuous (λ (i : ι), u i ω)) (hτ : τ) :

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

theorem measure_theory.adapted.stopped_process_of_discrete {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space Ω} [linear_order ι] [borel_space ι] {f : m} {u : ι Ω β} {τ : Ω ι} (hu : u) (hτ : τ) :

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

theorem measure_theory.adapted.strongly_measurable_stopped_process {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space Ω} [linear_order ι] [borel_space ι] {f : m} {u : ι Ω β} {τ : Ω ι} (hu : u) (hu_cont : (ω : Ω), continuous (λ (i : ι), u i ω)) (hτ : τ) (n : ι) :
theorem measure_theory.adapted.strongly_measurable_stopped_process_of_discrete {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space Ω} [linear_order ι] [borel_space ι] {f : m} {u : ι Ω β} {τ : Ω ι} (hu : u) (hτ : τ) (n : ι) :

Filtrations indexed by `ℕ`#

theorem measure_theory.stopped_value_sub_eq_sum {Ω : Type u_1} {β : Type u_2} {u : Ω β} {τ π : Ω } (hle : τ π) :
= λ (ω : Ω), (finset.Ico (τ ω) (π ω)).sum (λ (i : ), u (i + 1) - u i) ω
theorem measure_theory.stopped_value_sub_eq_sum' {Ω : Type u_1} {β : Type u_2} {u : Ω β} {τ π : Ω } (hle : τ π) {N : } (hbdd : (ω : Ω), π ω N) :
= λ (ω : Ω), (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 : Ω β} {τ : Ω } {N : } (hbdd : (ω : Ω), τ ω N) :
= λ (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 : Ω β} {τ : Ω } (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 : Ω β} {τ : Ω } (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 ι] {𝒢 : m} {τ η : Ω ι} {i : ι} {s : set Ω} [decidable_pred (λ (_x : Ω), _x s)] (hτ_st : τ) (hη_st : η) (hτ : (ω : Ω), i τ ω) (hη : (ω : Ω), i η ω) (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)

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

theorem measure_theory.condexp_stopping_time_ae_eq_restrict_eq_of_countable_range {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [linear_order ι] {μ : measure_theory.measure Ω} {ℱ : m} {τ : Ω ι} {E : Type u_4} [ E] {f : Ω E} (hτ : τ) (h_countable : (set.range τ).countable) [measure_theory.sigma_finite (μ.trim _)] (i : ι) :
=ᵐ[μ.restrict {x : Ω | τ x = i}] μ f
theorem measure_theory.condexp_stopping_time_ae_eq_restrict_eq_of_countable {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [linear_order ι] {μ : measure_theory.measure Ω} {ℱ : m} {τ : Ω ι} {E : Type u_4} [ E] {f : Ω E} [countable ι] (hτ : τ) [measure_theory.sigma_finite (μ.trim _)] (i : ι) :
=ᵐ[μ.restrict {x : Ω | τ x = i}] μ f
theorem measure_theory.condexp_min_stopping_time_ae_eq_restrict_le_const {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [linear_order ι] {μ : measure_theory.measure Ω} {ℱ : m} {τ : Ω ι} {E : Type u_4} [ E] {f : Ω E} (hτ : τ) (i : ι) [measure_theory.sigma_finite (μ.trim _)] :
=ᵐ[μ.restrict {x : Ω | τ x i}]
theorem measure_theory.condexp_stopping_time_ae_eq_restrict_eq {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [linear_order ι] {μ : measure_theory.measure Ω} {ℱ : m} {τ : Ω ι} {E : Type u_4} [ E] {f : Ω E} (hτ : τ) [measure_theory.sigma_finite (μ.trim _)] (i : ι) :
=ᵐ[μ.restrict {x : Ω | τ x = i}] μ f
theorem measure_theory.condexp_min_stopping_time_ae_eq_restrict_le {Ω : Type u_1} {ι : Type u_3} {m : measurable_space Ω} [linear_order ι] {μ : measure_theory.measure Ω} {ℱ : m} {τ σ : Ω ι} {E : Type u_4} [ E] {f : Ω E} [borel_space ι] (hτ : τ) (hσ : σ) [measure_theory.sigma_finite (μ.trim _)] :
=ᵐ[μ.restrict {x : Ω | τ x σ x}]