# Stopping times, stopped processes and stopped values #

Definition and properties of stopping times.

## Main definitions #

• MeasureTheory.IsStoppingTime: 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
• MeasureTheory.IsStoppingTime.measurableSpace: the σ-algebra associated with a stopping time

## Main results #

• ProgMeasurable.stoppedProcess: the stopped process of a progressively measurable process is progressively measurable.
• memℒp_stoppedProcess: 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 MeasureTheory.IsStoppingTime {Ω : Type u_1} {ι : Type u_3} {m : } [] (f : ) (τ : Ωι) :

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
Instances For
theorem MeasureTheory.isStoppingTime_const {Ω : Type u_1} {ι : Type u_3} {m : } [] (f : ) (i : ι) :
MeasureTheory.IsStoppingTime f fun (x : Ω) => i
theorem MeasureTheory.IsStoppingTime.measurableSet_le {Ω : Type u_1} {ι : Type u_3} {m : } [] {f : } {τ : Ωι} (hτ : ) (i : ι) :
MeasurableSet {ω : Ω | τ ω i}
theorem MeasureTheory.IsStoppingTime.measurableSet_lt_of_pred {Ω : Type u_1} {ι : Type u_3} {m : } [] {f : } {τ : Ωι} [] (hτ : ) (i : ι) :
MeasurableSet {ω : Ω | τ ω < i}
theorem MeasureTheory.IsStoppingTime.measurableSet_eq_of_countable_range {Ω : Type u_1} {ι : Type u_3} {m : } [] {τ : Ωι} {f : } (hτ : ) (h_countable : (Set.range τ).Countable) (i : ι) :
MeasurableSet {ω : Ω | τ ω = i}
theorem MeasureTheory.IsStoppingTime.measurableSet_eq_of_countable {Ω : Type u_1} {ι : Type u_3} {m : } [] {τ : Ωι} {f : } [] (hτ : ) (i : ι) :
MeasurableSet {ω : Ω | τ ω = i}
theorem MeasureTheory.IsStoppingTime.measurableSet_lt_of_countable_range {Ω : Type u_1} {ι : Type u_3} {m : } [] {τ : Ωι} {f : } (hτ : ) (h_countable : (Set.range τ).Countable) (i : ι) :
MeasurableSet {ω : Ω | τ ω < i}
theorem MeasureTheory.IsStoppingTime.measurableSet_lt_of_countable {Ω : Type u_1} {ι : Type u_3} {m : } [] {τ : Ωι} {f : } [] (hτ : ) (i : ι) :
MeasurableSet {ω : Ω | τ ω < i}
theorem MeasureTheory.IsStoppingTime.measurableSet_ge_of_countable_range {Ω : Type u_1} {m : } {ι : Type u_4} [] {τ : Ωι} {f : } (hτ : ) (h_countable : (Set.range τ).Countable) (i : ι) :
MeasurableSet {ω : Ω | i τ ω}
theorem MeasureTheory.IsStoppingTime.measurableSet_ge_of_countable {Ω : Type u_1} {m : } {ι : Type u_4} [] {τ : Ωι} {f : } [] (hτ : ) (i : ι) :
MeasurableSet {ω : Ω | i τ ω}
theorem MeasureTheory.IsStoppingTime.measurableSet_gt {Ω : Type u_1} {ι : Type u_3} {m : } [] {f : } {τ : Ωι} (hτ : ) (i : ι) :
MeasurableSet {ω : Ω | i < τ ω}
theorem MeasureTheory.IsStoppingTime.measurableSet_lt_of_isLUB {Ω : Type u_1} {ι : Type u_3} {m : } [] {f : } {τ : Ωι} [] [] (hτ : ) (i : ι) (h_lub : IsLUB (Set.Iio i) i) :
MeasurableSet {ω : Ω | τ ω < i}

Auxiliary lemma for MeasureTheory.IsStoppingTime.measurableSet_lt.

theorem MeasureTheory.IsStoppingTime.measurableSet_lt {Ω : Type u_1} {ι : Type u_3} {m : } [] {f : } {τ : Ωι} [] [] (hτ : ) (i : ι) :
MeasurableSet {ω : Ω | τ ω < i}
theorem MeasureTheory.IsStoppingTime.measurableSet_ge {Ω : Type u_1} {ι : Type u_3} {m : } [] {f : } {τ : Ωι} [] [] (hτ : ) (i : ι) :
MeasurableSet {ω : Ω | i τ ω}
theorem MeasureTheory.IsStoppingTime.measurableSet_eq {Ω : Type u_1} {ι : Type u_3} {m : } [] {f : } {τ : Ωι} [] [] (hτ : ) (i : ι) :
MeasurableSet {ω : Ω | τ ω = i}
theorem MeasureTheory.IsStoppingTime.measurableSet_eq_le {Ω : Type u_1} {ι : Type u_3} {m : } [] {f : } {τ : Ωι} [] [] (hτ : ) {i : ι} {j : ι} (hle : i j) :
MeasurableSet {ω : Ω | τ ω = i}
theorem MeasureTheory.IsStoppingTime.measurableSet_lt_le {Ω : Type u_1} {ι : Type u_3} {m : } [] {f : } {τ : Ωι} [] [] (hτ : ) {i : ι} {j : ι} (hle : i j) :
MeasurableSet {ω : Ω | τ ω < i}
theorem MeasureTheory.isStoppingTime_of_measurableSet_eq {Ω : Type u_1} {ι : Type u_3} {m : } [] [] {f : } {τ : Ωι} (hτ : ∀ (i : ι), MeasurableSet {ω : Ω | τ ω = i}) :
theorem MeasureTheory.IsStoppingTime.max {Ω : Type u_1} {ι : Type u_3} {m : } [] {f : } {τ : Ωι} {π : Ωι} (hτ : ) (hπ : ) :
MeasureTheory.IsStoppingTime f fun (ω : Ω) => max (τ ω) (π ω)
theorem MeasureTheory.IsStoppingTime.max_const {Ω : Type u_1} {ι : Type u_3} {m : } [] {f : } {τ : Ωι} (hτ : ) (i : ι) :
MeasureTheory.IsStoppingTime f fun (ω : Ω) => max (τ ω) i
theorem MeasureTheory.IsStoppingTime.min {Ω : Type u_1} {ι : Type u_3} {m : } [] {f : } {τ : Ωι} {π : Ωι} (hτ : ) (hπ : ) :
MeasureTheory.IsStoppingTime f fun (ω : Ω) => min (τ ω) (π ω)
theorem MeasureTheory.IsStoppingTime.min_const {Ω : Type u_1} {ι : Type u_3} {m : } [] {f : } {τ : Ωι} (hτ : ) (i : ι) :
MeasureTheory.IsStoppingTime f fun (ω : Ω) => min (τ ω) i
theorem MeasureTheory.IsStoppingTime.add_const {Ω : Type u_1} {ι : Type u_3} {m : } [] [] [CovariantClass ι ι (Function.swap fun (x1 x2 : ι) => x1 + x2) fun (x1 x2 : ι) => x1 x2] [CovariantClass ι ι (fun (x1 x2 : ι) => x1 + x2) fun (x1 x2 : ι) => x1 x2] {f : } {τ : Ωι} (hτ : ) {i : ι} (hi : 0 i) :
MeasureTheory.IsStoppingTime f fun (ω : Ω) => τ ω + i
theorem MeasureTheory.IsStoppingTime.add_const_nat {Ω : Type u_1} {m : } {f : } {τ : Ω} (hτ : ) {i : } :
MeasureTheory.IsStoppingTime f fun (ω : Ω) => τ ω + i
theorem MeasureTheory.IsStoppingTime.add {Ω : Type u_1} {m : } {f : } {τ : Ω} {π : Ω} (hτ : ) (hπ : ) :
def MeasureTheory.IsStoppingTime.measurableSpace {Ω : Type u_1} {ι : Type u_3} {m : } [] {f : } {τ : Ωι} (hτ : ) :

The associated σ-algebra with a stopping time.

Equations
• .measurableSpace = { MeasurableSet' := fun (s : Set Ω) => ∀ (i : ι), MeasurableSet (s {ω : Ω | τ ω i}), measurableSet_empty := , measurableSet_compl := , measurableSet_iUnion := }
Instances For
theorem MeasureTheory.IsStoppingTime.measurableSet {Ω : Type u_1} {ι : Type u_3} {m : } [] {f : } {τ : Ωι} (hτ : ) (s : Set Ω) :
∀ (i : ι), MeasurableSet (s {ω : Ω | τ ω i})
theorem MeasureTheory.IsStoppingTime.measurableSpace_mono {Ω : Type u_1} {ι : Type u_3} {m : } [] {f : } {τ : Ωι} {π : Ωι} (hτ : ) (hπ : ) (hle : τ π) :
.measurableSpace .measurableSpace
theorem MeasureTheory.IsStoppingTime.measurableSpace_le_of_countable {Ω : Type u_1} {ι : Type u_3} {m : } [] {f : } {τ : Ωι} [] (hτ : ) :
.measurableSpace m
theorem MeasureTheory.IsStoppingTime.measurableSpace_le' {Ω : Type u_1} {ι : Type u_3} {m : } [] {f : } {τ : Ωι} [Filter.atTop.IsCountablyGenerated] [Filter.atTop.NeBot] (hτ : ) :
.measurableSpace m
theorem MeasureTheory.IsStoppingTime.measurableSpace_le {Ω : Type u_1} {m : } {ι : Type u_4} [] {f : } {τ : Ωι} [Filter.atTop.IsCountablyGenerated] (hτ : ) :
.measurableSpace m
@[simp]
theorem MeasureTheory.IsStoppingTime.measurableSpace_const {Ω : Type u_1} {ι : Type u_3} {m : } [] (f : ) (i : ι) :
.measurableSpace = f i
theorem MeasureTheory.IsStoppingTime.measurableSet_inter_eq_iff {Ω : Type u_1} {ι : Type u_3} {m : } [] {f : } {τ : Ωι} (hτ : ) (s : Set Ω) (i : ι) :
MeasurableSet (s {ω : Ω | τ ω = i}) MeasurableSet (s {ω : Ω | τ ω = i})
theorem MeasureTheory.IsStoppingTime.measurableSpace_le_of_le_const {Ω : Type u_1} {ι : Type u_3} {m : } [] {f : } {τ : Ωι} (hτ : ) {i : ι} (hτ_le : ∀ (ω : Ω), τ ω i) :
.measurableSpace f i
theorem MeasureTheory.IsStoppingTime.measurableSpace_le_of_le {Ω : Type u_1} {ι : Type u_3} {m : } [] {f : } {τ : Ωι} (hτ : ) {n : ι} (hτ_le : ∀ (ω : Ω), τ ω n) :
.measurableSpace m
theorem MeasureTheory.IsStoppingTime.le_measurableSpace_of_const_le {Ω : Type u_1} {ι : Type u_3} {m : } [] {f : } {τ : Ωι} (hτ : ) {i : ι} (hτ_le : ∀ (ω : Ω), i τ ω) :
f i .measurableSpace
instance MeasureTheory.IsStoppingTime.sigmaFinite_stopping_time {Ω : Type u_1} {m : } {ι : Type u_4} [] [] [Filter.atTop.IsCountablyGenerated] {μ : } {f : } {τ : Ωι} (hτ : ) :
Equations
• =
instance MeasureTheory.IsStoppingTime.sigmaFinite_stopping_time_of_le {Ω : Type u_1} {m : } {ι : Type u_4} [] [] {μ : } {f : } {τ : Ωι} (hτ : ) {n : ι} (hτ_le : ∀ (ω : Ω), τ ω n) :
Equations
• =
theorem MeasureTheory.IsStoppingTime.measurableSet_le' {Ω : Type u_1} {ι : Type u_3} {m : } [] {f : } {τ : Ωι} (hτ : ) (i : ι) :
MeasurableSet {ω : Ω | τ ω i}
theorem MeasureTheory.IsStoppingTime.measurableSet_gt' {Ω : Type u_1} {ι : Type u_3} {m : } [] {f : } {τ : Ωι} (hτ : ) (i : ι) :
MeasurableSet {ω : Ω | i < τ ω}
theorem MeasureTheory.IsStoppingTime.measurableSet_eq' {Ω : Type u_1} {ι : Type u_3} {m : } [] {f : } {τ : Ωι} [] [] (hτ : ) (i : ι) :
MeasurableSet {ω : Ω | τ ω = i}
theorem MeasureTheory.IsStoppingTime.measurableSet_ge' {Ω : Type u_1} {ι : Type u_3} {m : } [] {f : } {τ : Ωι} [] [] (hτ : ) (i : ι) :
MeasurableSet {ω : Ω | i τ ω}
theorem MeasureTheory.IsStoppingTime.measurableSet_lt' {Ω : Type u_1} {ι : Type u_3} {m : } [] {f : } {τ : Ωι} [] [] (hτ : ) (i : ι) :
MeasurableSet {ω : Ω | τ ω < i}
theorem MeasureTheory.IsStoppingTime.measurableSet_eq_of_countable_range' {Ω : Type u_1} {ι : Type u_3} {m : } [] {f : } {τ : Ωι} (hτ : ) (h_countable : (Set.range τ).Countable) (i : ι) :
MeasurableSet {ω : Ω | τ ω = i}
theorem MeasureTheory.IsStoppingTime.measurableSet_eq_of_countable' {Ω : Type u_1} {ι : Type u_3} {m : } [] {f : } {τ : Ωι} [] (hτ : ) (i : ι) :
MeasurableSet {ω : Ω | τ ω = i}
theorem MeasureTheory.IsStoppingTime.measurableSet_ge_of_countable_range' {Ω : Type u_1} {ι : Type u_3} {m : } [] {f : } {τ : Ωι} (hτ : ) (h_countable : (Set.range τ).Countable) (i : ι) :
MeasurableSet {ω : Ω | i τ ω}
theorem MeasureTheory.IsStoppingTime.measurableSet_ge_of_countable' {Ω : Type u_1} {ι : Type u_3} {m : } [] {f : } {τ : Ωι} [] (hτ : ) (i : ι) :
MeasurableSet {ω : Ω | i τ ω}
theorem MeasureTheory.IsStoppingTime.measurableSet_lt_of_countable_range' {Ω : Type u_1} {ι : Type u_3} {m : } [] {f : } {τ : Ωι} (hτ : ) (h_countable : (Set.range τ).Countable) (i : ι) :
MeasurableSet {ω : Ω | τ ω < i}
theorem MeasureTheory.IsStoppingTime.measurableSet_lt_of_countable' {Ω : Type u_1} {ι : Type u_3} {m : } [] {f : } {τ : Ωι} [] (hτ : ) (i : ι) :
MeasurableSet {ω : Ω | τ ω < i}
theorem MeasureTheory.IsStoppingTime.measurableSpace_le_of_countable_range {Ω : Type u_1} {ι : Type u_3} {m : } [] {f : } {τ : Ωι} (hτ : ) (h_countable : (Set.range τ).Countable) :
.measurableSpace m
theorem MeasureTheory.IsStoppingTime.measurable {Ω : Type u_1} {ι : Type u_3} {m : } [] {f : } {τ : Ωι} [] [] [] [] (hτ : ) :
theorem MeasureTheory.IsStoppingTime.measurable_of_le {Ω : Type u_1} {ι : Type u_3} {m : } [] {f : } {τ : Ωι} [] [] [] [] (hτ : ) {i : ι} (hτ_le : ∀ (ω : Ω), τ ω i) :
theorem MeasureTheory.IsStoppingTime.measurableSpace_min {Ω : Type u_1} {ι : Type u_3} {m : } [] {f : } {τ : Ωι} {π : Ωι} (hτ : ) (hπ : ) :
.measurableSpace = .measurableSpace .measurableSpace
theorem MeasureTheory.IsStoppingTime.measurableSet_min_iff {Ω : Type u_1} {ι : Type u_3} {m : } [] {f : } {τ : Ωι} {π : Ωι} (hτ : ) (hπ : ) (s : Set Ω) :
theorem MeasureTheory.IsStoppingTime.measurableSpace_min_const {Ω : Type u_1} {ι : Type u_3} {m : } [] {f : } {τ : Ωι} (hτ : ) {i : ι} :
.measurableSpace = .measurableSpace f i
theorem MeasureTheory.IsStoppingTime.measurableSet_min_const_iff {Ω : Type u_1} {ι : Type u_3} {m : } [] {f : } {τ : Ωι} (hτ : ) (s : Set Ω) {i : ι} :
theorem MeasureTheory.IsStoppingTime.measurableSet_inter_le {Ω : Type u_1} {ι : Type u_3} {m : } [] {f : } {τ : Ωι} {π : Ωι} [] [] [] [] (hτ : ) (hπ : ) (s : Set Ω) (hs : ) :
MeasurableSet (s {ω : Ω | τ ω π ω})
theorem MeasureTheory.IsStoppingTime.measurableSet_inter_le_iff {Ω : Type u_1} {ι : Type u_3} {m : } [] {f : } {τ : Ωι} {π : Ωι} [] [] [] [] (hτ : ) (hπ : ) (s : Set Ω) :
MeasurableSet (s {ω : Ω | τ ω π ω}) MeasurableSet (s {ω : Ω | τ ω π ω})
theorem MeasureTheory.IsStoppingTime.measurableSet_inter_le_const_iff {Ω : Type u_1} {ι : Type u_3} {m : } [] {f : } {τ : Ωι} (hτ : ) (s : Set Ω) (i : ι) :
MeasurableSet (s {ω : Ω | τ ω i}) MeasurableSet (s {ω : Ω | τ ω i})
theorem MeasureTheory.IsStoppingTime.measurableSet_le_stopping_time {Ω : Type u_1} {ι : Type u_3} {m : } [] {f : } {τ : Ωι} {π : Ωι} [] [] [] [] (hτ : ) (hπ : ) :
MeasurableSet {ω : Ω | τ ω π ω}
theorem MeasureTheory.IsStoppingTime.measurableSet_stopping_time_le {Ω : Type u_1} {ι : Type u_3} {m : } [] {f : } {τ : Ωι} {π : Ωι} [] [] [] [] (hτ : ) (hπ : ) :
MeasurableSet {ω : Ω | τ ω π ω}
theorem MeasureTheory.IsStoppingTime.measurableSet_eq_stopping_time {Ω : Type u_1} {ι : Type u_3} {m : } [] {f : } {τ : Ωι} {π : Ωι} [] [] [] [] [] [] (hτ : ) (hπ : ) :
MeasurableSet {ω : Ω | τ ω = π ω}
theorem MeasureTheory.IsStoppingTime.measurableSet_eq_stopping_time_of_countable {Ω : Type u_1} {ι : Type u_3} {m : } [] {f : } {τ : Ωι} {π : Ωι} [] [] [] [] [] (hτ : ) (hπ : ) :
MeasurableSet {ω : Ω | τ ω = π ω}

## Stopped value and stopped process #

def MeasureTheory.stoppedValue {Ω : 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 (τ ω) ω
Instances For
theorem MeasureTheory.stoppedValue_const {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} (u : ιΩβ) (i : ι) :
(MeasureTheory.stoppedValue u fun (x : Ω) => i) = u i
def MeasureTheory.stoppedProcess {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [] (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 occurred.

Equations
• = u (min i (τ ω)) ω
Instances For
theorem MeasureTheory.stoppedProcess_eq_stoppedValue {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [] {u : ιΩβ} {τ : Ωι} :
= fun (i : ι) => MeasureTheory.stoppedValue u fun (ω : Ω) => min i (τ ω)
theorem MeasureTheory.stoppedValue_stoppedProcess {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [] {u : ιΩβ} {τ : Ωι} {σ : Ωι} :
= MeasureTheory.stoppedValue u fun (ω : Ω) => min (σ ω) (τ ω)
theorem MeasureTheory.stoppedProcess_eq_of_le {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [] {u : ιΩβ} {τ : Ωι} {i : ι} {ω : Ω} (h : i τ ω) :
= u i ω
theorem MeasureTheory.stoppedProcess_eq_of_ge {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [] {u : ιΩβ} {τ : Ωι} {i : ι} {ω : Ω} (h : τ ω i) :
= u (τ ω) ω
theorem MeasureTheory.progMeasurable_min_stopping_time {Ω : Type u_1} {ι : Type u_3} {m : } [] [] [] [] [] {τ : Ωι} {f : } (hτ : ) :
MeasureTheory.ProgMeasurable f fun (i : ι) (ω : Ω) => min i (τ ω)
theorem MeasureTheory.ProgMeasurable.stoppedProcess {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } [] [] [] [] [] [] {u : ιΩβ} {τ : Ωι} {f : } (h : ) (hτ : ) :
theorem MeasureTheory.ProgMeasurable.adapted_stoppedProcess {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } [] [] [] [] [] [] {u : ιΩβ} {τ : Ωι} {f : } (h : ) (hτ : ) :
theorem MeasureTheory.ProgMeasurable.stronglyMeasurable_stoppedProcess {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } [] [] [] [] [] [] {u : ιΩβ} {τ : Ωι} {f : } (hu : ) (hτ : ) (i : ι) :
theorem MeasureTheory.stronglyMeasurable_stoppedValue_of_le {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } [] [] [] [] [] [] {u : ιΩβ} {τ : Ωι} {f : } (h : ) (hτ : ) {n : ι} (hτ_le : ∀ (ω : Ω), τ ω n) :
theorem MeasureTheory.measurable_stoppedValue {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } [] [] [] [] [] [] {u : ιΩβ} {τ : Ωι} {f : } [] [] (hf_prog : ) (hτ : ) :
theorem MeasureTheory.stoppedValue_eq_of_mem_finset {Ω : Type u_1} {ι : Type u_3} {τ : Ωι} {E : Type u_4} {u : ιΩE} [] {s : } (hbdd : ∀ (ω : Ω), τ ω s) :
= is, {ω : Ω | τ ω = i}.indicator (u i)
theorem MeasureTheory.stoppedValue_eq' {Ω : Type u_1} {ι : Type u_3} {τ : Ωι} {E : Type u_4} {u : ιΩE} [] [] {N : ι} (hbdd : ∀ (ω : Ω), τ ω N) :
= i, {ω : Ω | τ ω = i}.indicator (u i)
theorem MeasureTheory.stoppedProcess_eq_of_mem_finset {Ω : Type u_1} {ι : Type u_3} {τ : Ωι} {E : Type u_4} {u : ιΩE} [] [] {s : } (n : ι) (hbdd : ∀ (ω : Ω), τ ω < nτ ω s) :
= {a : Ω | n τ a}.indicator (u n) + iFinset.filter (fun (x : ι) => x < n) s, {ω : Ω | τ ω = i}.indicator (u i)
theorem MeasureTheory.stoppedProcess_eq'' {Ω : Type u_1} {ι : Type u_3} {τ : Ωι} {E : Type u_4} {u : ιΩE} [] [] (n : ι) :
= {a : Ω | n τ a}.indicator (u n) + i, {ω : Ω | τ ω = i}.indicator (u i)
theorem MeasureTheory.memℒp_stoppedValue_of_mem_finset {Ω : Type u_1} {ι : Type u_3} {m : } {μ : } {τ : Ωι} {E : Type u_4} {p : ENNReal} {u : ιΩE} [] {ℱ : } (hτ : ) (hu : ∀ (n : ι), MeasureTheory.Memℒp (u n) p μ) {s : } (hbdd : ∀ (ω : Ω), τ ω s) :
theorem MeasureTheory.memℒp_stoppedValue {Ω : Type u_1} {ι : Type u_3} {m : } {μ : } {τ : Ωι} {E : Type u_4} {p : ENNReal} {u : ιΩE} [] {ℱ : } (hτ : ) (hu : ∀ (n : ι), MeasureTheory.Memℒp (u n) p μ) {N : ι} (hbdd : ∀ (ω : Ω), τ ω N) :
theorem MeasureTheory.integrable_stoppedValue_of_mem_finset {Ω : Type u_1} {ι : Type u_3} {m : } {μ : } {τ : Ωι} {E : Type u_4} {u : ιΩE} [] {ℱ : } (hτ : ) (hu : ∀ (n : ι), MeasureTheory.Integrable (u n) μ) {s : } (hbdd : ∀ (ω : Ω), τ ω s) :
theorem MeasureTheory.integrable_stoppedValue {Ω : Type u_1} (ι : Type u_3) {m : } {μ : } {τ : Ωι} {E : Type u_4} {u : ιΩE} [] {ℱ : } (hτ : ) (hu : ∀ (n : ι), MeasureTheory.Integrable (u n) μ) {N : ι} (hbdd : ∀ (ω : Ω), τ ω N) :
theorem MeasureTheory.memℒp_stoppedProcess_of_mem_finset {Ω : Type u_1} {ι : Type u_3} {m : } {μ : } {τ : Ωι} {E : Type u_4} {p : ENNReal} {u : ιΩE} [] [] [] {ℱ : } (hτ : ) (hu : ∀ (n : ι), MeasureTheory.Memℒp (u n) p μ) (n : ι) {s : } (hbdd : ∀ (ω : Ω), τ ω < nτ ω s) :
theorem MeasureTheory.memℒp_stoppedProcess {Ω : Type u_1} {ι : Type u_3} {m : } {μ : } {τ : Ωι} {E : Type u_4} {p : ENNReal} {u : ιΩE} [] [] [] {ℱ : } (hτ : ) (hu : ∀ (n : ι), MeasureTheory.Memℒp (u n) p μ) (n : ι) :
theorem MeasureTheory.integrable_stoppedProcess_of_mem_finset {Ω : Type u_1} {ι : Type u_3} {m : } {μ : } {τ : Ωι} {E : Type u_4} {u : ιΩE} [] [] [] {ℱ : } (hτ : ) (hu : ∀ (n : ι), MeasureTheory.Integrable (u n) μ) (n : ι) {s : } (hbdd : ∀ (ω : Ω), τ ω < nτ ω s) :
theorem MeasureTheory.integrable_stoppedProcess {Ω : Type u_1} {ι : Type u_3} {m : } {μ : } {τ : Ωι} {E : Type u_4} {u : ιΩE} [] [] [] {ℱ : } (hτ : ) (hu : ∀ (n : ι), MeasureTheory.Integrable (u n) μ) (n : ι) :
theorem MeasureTheory.Adapted.stoppedProcess {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } [] [] [] [] [] [] {f : } {u : ιΩβ} {τ : Ωι} (hu : ) (hu_cont : ∀ (ω : Ω), Continuous fun (i : ι) => u i ω) (hτ : ) :

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

theorem MeasureTheory.Adapted.stoppedProcess_of_discrete {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } [] [] [] [] [] [] {f : } {u : ιΩβ} {τ : Ωι} [] (hu : ) (hτ : ) :

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

theorem MeasureTheory.Adapted.stronglyMeasurable_stoppedProcess {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } [] [] [] [] [] [] {f : } {u : ιΩβ} {τ : Ωι} (hu : ) (hu_cont : ∀ (ω : Ω), Continuous fun (i : ι) => u i ω) (hτ : ) (n : ι) :
theorem MeasureTheory.Adapted.stronglyMeasurable_stoppedProcess_of_discrete {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } [] [] [] [] [] [] {f : } {u : ιΩβ} {τ : Ωι} [] (hu : ) (hτ : ) (n : ι) :

### Filtrations indexed by ℕ#

theorem MeasureTheory.stoppedValue_sub_eq_sum {Ω : Type u_1} {β : Type u_2} {u : Ωβ} {τ : Ω} {π : Ω} [] (hle : τ π) :
= fun (ω : Ω) => (∑ iFinset.Ico (τ ω) (π ω), (u (i + 1) - u i)) ω
theorem MeasureTheory.stoppedValue_sub_eq_sum' {Ω : Type u_1} {β : Type u_2} {u : Ωβ} {τ : Ω} {π : Ω} [] (hle : τ π) {N : } (hbdd : ∀ (ω : Ω), π ω N) :
= fun (ω : Ω) => (∑ iFinset.range (N + 1), {ω : Ω | τ ω i i < π ω}.indicator (u (i + 1) - u i)) ω
theorem MeasureTheory.stoppedValue_eq {Ω : Type u_1} {β : Type u_2} {u : Ωβ} {τ : Ω} [] {N : } (hbdd : ∀ (ω : Ω), τ ω N) :
= fun (x : Ω) => (∑ iFinset.range (N + 1), {ω : Ω | τ ω = i}.indicator (u i)) x
theorem MeasureTheory.stoppedProcess_eq {Ω : Type u_1} {β : Type u_2} {u : Ωβ} {τ : Ω} [] (n : ) :
= {a : Ω | n τ a}.indicator (u n) + i, {ω : Ω | τ ω = i}.indicator (u i)
theorem MeasureTheory.stoppedProcess_eq' {Ω : Type u_1} {β : Type u_2} {u : Ωβ} {τ : Ω} [] (n : ) :
= {a : Ω | n + 1 τ a}.indicator (u n) + iFinset.range (n + 1), {a : Ω | τ a = i}.indicator (u i)
theorem MeasureTheory.IsStoppingTime.piecewise_of_le {Ω : Type u_1} {ι : Type u_3} {m : } [] {𝒢 : } {τ : Ωι} {η : Ωι} {i : ι} {s : Set Ω} [DecidablePred fun (x : Ω) => x s] (hτ_st : ) (hη_st : ) (hτ : ∀ (ω : Ω), i τ ω) (hη : ∀ (ω : Ω), i η ω) (hs : ) :
MeasureTheory.IsStoppingTime 𝒢 (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 MeasureTheory.isStoppingTime_piecewise_const {Ω : Type u_1} {ι : Type u_3} {m : } [] {𝒢 : } {i : ι} {j : ι} {s : Set Ω} [DecidablePred fun (x : Ω) => x s] (hij : i j) (hs : ) :
MeasureTheory.IsStoppingTime 𝒢 (s.piecewise (fun (x : Ω) => i) fun (x : Ω) => j)
theorem MeasureTheory.stoppedValue_piecewise_const {Ω : Type u_1} {s : Set Ω} [DecidablePred fun (x : Ω) => x s] {ι' : Type u_4} {i : ι'} {j : ι'} {f : ι'Ω} :
MeasureTheory.stoppedValue f (s.piecewise (fun (x : Ω) => i) fun (x : Ω) => j) = s.piecewise (f i) (f j)
theorem MeasureTheory.stoppedValue_piecewise_const' {Ω : Type u_1} {s : Set Ω} [DecidablePred fun (x : Ω) => x s] {ι' : Type u_4} {i : ι'} {j : ι'} {f : ι'Ω} :
MeasureTheory.stoppedValue f (s.piecewise (fun (x : Ω) => i) fun (x : Ω) => j) = s.indicator (f i) + s.indicator (f j)

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

theorem MeasureTheory.condexp_stopping_time_ae_eq_restrict_eq_of_countable_range {Ω : Type u_1} {ι : Type u_3} {m : } [] {μ : } {ℱ : } {τ : Ωι} {E : Type u_4} [] [] {f : ΩE} (hτ : ) (h_countable : (Set.range τ).Countable) [MeasureTheory.SigmaFinite (μ.trim )] (i : ι) :
MeasureTheory.condexp .measurableSpace μ f =ᵐ[μ.restrict {x : Ω | τ x = i}] MeasureTheory.condexp ( i) μ f
theorem MeasureTheory.condexp_stopping_time_ae_eq_restrict_eq_of_countable {Ω : Type u_1} {ι : Type u_3} {m : } [] {μ : } {ℱ : } {τ : Ωι} {E : Type u_4} [] [] {f : ΩE} [] (hτ : ) [MeasureTheory.SigmaFinite (μ.trim )] (i : ι) :
MeasureTheory.condexp .measurableSpace μ f =ᵐ[μ.restrict {x : Ω | τ x = i}] MeasureTheory.condexp ( i) μ f
theorem MeasureTheory.condexp_min_stopping_time_ae_eq_restrict_le_const {Ω : Type u_1} {ι : Type u_3} {m : } [] {μ : } {ℱ : } {τ : Ωι} {E : Type u_4} [] [] {f : ΩE} [Filter.atTop.IsCountablyGenerated] (hτ : ) (i : ι) [MeasureTheory.SigmaFinite (μ.trim )] :
MeasureTheory.condexp .measurableSpace μ f =ᵐ[μ.restrict {x : Ω | τ x i}] MeasureTheory.condexp .measurableSpace μ f
theorem MeasureTheory.condexp_stopping_time_ae_eq_restrict_eq {Ω : Type u_1} {ι : Type u_3} {m : } [] {μ : } {ℱ : } {τ : Ωι} {E : Type u_4} [] [] {f : ΩE} [Filter.atTop.IsCountablyGenerated] [] [] (hτ : ) [MeasureTheory.SigmaFinite (μ.trim )] (i : ι) :
MeasureTheory.condexp .measurableSpace μ f =ᵐ[μ.restrict {x : Ω | τ x = i}] MeasureTheory.condexp ( i) μ f
theorem MeasureTheory.condexp_min_stopping_time_ae_eq_restrict_le {Ω : Type u_1} {ι : Type u_3} {m : } [] {μ : } {ℱ : } {τ : Ωι} {σ : Ωι} {E : Type u_4} [] [] {f : ΩE} [Filter.atTop.IsCountablyGenerated] [] [] [] [] (hτ : ) (hσ : ) [MeasureTheory.SigmaFinite (μ.trim )] :
MeasureTheory.condexp .measurableSpace μ f =ᵐ[μ.restrict {x : Ω | τ x σ x}] MeasureTheory.condexp .measurableSpace μ f