# 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` on a measurable space `Ω` is a function `τ : Ω → WithTop ι` 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.
- `memLp_stoppedProcess`: if a process belongs to `ℒp` at every time in `ℕ`, then its stopped process belongs to `ℒp` as well.

## Implementation notes #

For a filtration on a type `ι`, we define stopping times as functions from the measurable space `Ω` to `WithTop ι`, which allows stopping times that can take an infinite value, represented by `⊤ : WithTop ι`.

This means that if we have a process `X : ι → Ω → β` and a stopping time `τ : Ω → WithTop ι`, then to consider the value of `X` at the stopping time `τ ω`, we need to write `X (τ ω).untopA ω`, in which `(τ ω).untopA` is the value of `τ ω` in `ι` if `τ ω ≠ ⊤` and some arbitrary value if `τ ω = ⊤`.

While indexing would be more convenient if we defined stopping times as functions from `Ω` to `ι`, this would prevent us from using stopping times as in standard mathematical literature, where a typical example of stopping time is the first time an event occurs, which may never happen. Consider for example the first time a coin lands heads when flipping it infinitely many times: this is almost surely finite, but possibly infinite. We could also not use a function `Ω → ι` with arbitrary value for the infinite case, because this would be incompatible with the stopping time property.

## Tags #

stopping time, stochastic process

### Stopping times #

source
def MeasureTheory.IsStoppingTime {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] (f : Filtration ι m) (τ : Ω → WithTop ι) :
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

- MeasureTheory.IsStoppingTime f τ = ∀ (i : ι), MeasurableSet {ω : Ω | τ ω ≤ ↑i}

Instances For

source
theorem MeasureTheory.isStoppingTime_const {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] (f : Filtration ι m) (i : ι) :
IsStoppingTime f fun (x : Ω) => ↑i
source
theorem MeasureTheory.IsStoppingTime.measurableSet_le {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] {f : Filtration ι m} {τ : Ω → WithTop ι} (hτ : IsStoppingTime f τ) (i : ι) :
MeasurableSet {ω : Ω | τ ω ≤ ↑i}
source
theorem MeasureTheory.IsStoppingTime.measurableSet_lt_of_pred {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] {f : Filtration ι m} {τ : Ω → WithTop ι} [PredOrder ι] (hτ : IsStoppingTime f τ) (i : ι) :
MeasurableSet {ω : Ω | τ ω < ↑i}
source
theorem MeasureTheory.IsStoppingTime.measurableSet_eq_of_countable_range {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [PartialOrder ι] {τ : Ω → WithTop ι} {f : Filtration ι m} (hτ : IsStoppingTime f τ) (h_countable : (Set.range τ).Countable) (i : ι) :
MeasurableSet {ω : Ω | τ ω = ↑i}
source
theorem MeasureTheory.IsStoppingTime.measurableSet_eq_of_countable {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [PartialOrder ι] {τ : Ω → WithTop ι} {f : Filtration ι m} [Countable ι] (hτ : IsStoppingTime f τ) (i : ι) :
MeasurableSet {ω : Ω | τ ω = ↑i}
source
theorem MeasureTheory.IsStoppingTime.measurableSet_lt_of_countable_range {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [PartialOrder ι] {τ : Ω → WithTop ι} {f : Filtration ι m} (hτ : IsStoppingTime f τ) (h_countable : (Set.range τ).Countable) (i : ι) :
MeasurableSet {ω : Ω | τ ω < ↑i}
source
theorem MeasureTheory.IsStoppingTime.measurableSet_lt_of_countable {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [PartialOrder ι] {τ : Ω → WithTop ι} {f : Filtration ι m} [Countable ι] (hτ : IsStoppingTime f τ) (i : ι) :
MeasurableSet {ω : Ω | τ ω < ↑i}
source
theorem MeasureTheory.IsStoppingTime.measurableSet_ge_of_countable_range {Ω : Type u_1} {m : MeasurableSpace Ω} {ι : Type u_4} [LinearOrder ι] {τ : Ω → WithTop ι} {f : Filtration ι m} (hτ : IsStoppingTime f τ) (h_countable : (Set.range τ).Countable) (i : ι) :
MeasurableSet {ω : Ω | ↑i ≤ τ ω}
source
theorem MeasureTheory.IsStoppingTime.measurableSet_ge_of_countable {Ω : Type u_1} {m : MeasurableSpace Ω} {ι : Type u_4} [LinearOrder ι] {τ : Ω → WithTop ι} {f : Filtration ι m} [Countable ι] (hτ : IsStoppingTime f τ) (i : ι) :
MeasurableSet {ω : Ω | ↑i ≤ τ ω}
source
theorem MeasureTheory.IsStoppingTime.measurableSet_gt {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [LinearOrder ι] {f : Filtration ι m} {τ : Ω → WithTop ι} (hτ : IsStoppingTime f τ) (i : ι) :
MeasurableSet {ω : Ω | ↑i < τ ω}
source
theorem MeasureTheory.IsStoppingTime.measurableSet_lt_of_isLUB {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [LinearOrder ι] {f : Filtration ι m} {τ : Ω → WithTop ι} [TopologicalSpace ι] [OrderTopology ι] [FirstCountableTopology ι] (hτ : IsStoppingTime f τ) (i : ι) (h_lub : IsLUB (Set.Iio i) i) :
MeasurableSet {ω : Ω | τ ω < ↑i}

Auxiliary lemma for `MeasureTheory.IsStoppingTime.measurableSet_lt`.

source
theorem MeasureTheory.IsStoppingTime.measurableSet_lt {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [LinearOrder ι] {f : Filtration ι m} {τ : Ω → WithTop ι} [TopologicalSpace ι] [OrderTopology ι] [FirstCountableTopology ι] (hτ : IsStoppingTime f τ) (i : ι) :
MeasurableSet {ω : Ω | τ ω < ↑i}
source
theorem MeasureTheory.IsStoppingTime.measurableSet_ge {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [LinearOrder ι] {f : Filtration ι m} {τ : Ω → WithTop ι} [TopologicalSpace ι] [OrderTopology ι] [FirstCountableTopology ι] (hτ : IsStoppingTime f τ) (i : ι) :
MeasurableSet {ω : Ω | ↑i ≤ τ ω}
source
theorem MeasureTheory.IsStoppingTime.measurableSet_eq {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [LinearOrder ι] {f : Filtration ι m} {τ : Ω → WithTop ι} [TopologicalSpace ι] [OrderTopology ι] [FirstCountableTopology ι] (hτ : IsStoppingTime f τ) (i : ι) :
MeasurableSet {ω : Ω | τ ω = ↑i}
source
theorem MeasureTheory.IsStoppingTime.measurableSet_eq_le {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [LinearOrder ι] {f : Filtration ι m} {τ : Ω → WithTop ι} [TopologicalSpace ι] [OrderTopology ι] [FirstCountableTopology ι] (hτ : IsStoppingTime f τ) {i j : ι} (hle : i ≤ j) :
MeasurableSet {ω : Ω | τ ω = ↑i}
source
theorem MeasureTheory.IsStoppingTime.measurableSet_lt_le {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [LinearOrder ι] {f : Filtration ι m} {τ : Ω → WithTop ι} [TopologicalSpace ι] [OrderTopology ι] [FirstCountableTopology ι] (hτ : IsStoppingTime f τ) {i j : ι} (hle : i ≤ j) :
MeasurableSet {ω : Ω | τ ω < ↑i}
source
theorem MeasureTheory.isStoppingTime_of_measurableSet_eq {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] [Countable ι] {f : Filtration ι m} {τ : Ω → WithTop ι} (hτ : ∀ (i : ι), MeasurableSet {ω : Ω | τ ω = ↑i}) :
IsStoppingTime f τ
source
theorem MeasureTheory.IsStoppingTime.max {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [LinearOrder ι] {f : Filtration ι m} {τ π : Ω → WithTop ι} (hτ : IsStoppingTime f τ) (hπ : IsStoppingTime f π) :
IsStoppingTime f fun (ω : Ω) => max (τ ω) (π ω)
source
theorem MeasureTheory.IsStoppingTime.max_const {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [LinearOrder ι] {f : Filtration ι m} {τ : Ω → WithTop ι} (hτ : IsStoppingTime f τ) (i : ι) :
IsStoppingTime f fun (ω : Ω) => max (τ ω) ↑i
source
theorem MeasureTheory.IsStoppingTime.min {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [LinearOrder ι] {f : Filtration ι m} {τ π : Ω → WithTop ι} (hτ : IsStoppingTime f τ) (hπ : IsStoppingTime f π) :
IsStoppingTime f fun (ω : Ω) => min (τ ω) (π ω)
source
theorem MeasureTheory.IsStoppingTime.min_const {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [LinearOrder ι] {f : Filtration ι m} {τ : Ω → WithTop ι} (hτ : IsStoppingTime f τ) (i : ι) :
IsStoppingTime f fun (ω : Ω) => min (τ ω) ↑i
source
theorem MeasureTheory.IsStoppingTime.add_const {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [AddGroup ι] [Preorder ι] [AddRightMono ι] [AddLeftMono ι] {f : Filtration ι m} {τ : Ω → WithTop ι} (hτ : IsStoppingTime f τ) {i : ι} (hi : 0 ≤ i) :
IsStoppingTime f fun (ω : Ω) => τ ω + ↑i
source
theorem MeasureTheory.IsStoppingTime.add_const_nat {Ω : Type u_1} {m : MeasurableSpace Ω} {f : Filtration ℕ m} {τ : Ω → WithTop ℕ} (hτ : IsStoppingTime f τ) {i : ℕ} :
IsStoppingTime f fun (ω : Ω) => τ ω + ↑i
source
theorem MeasureTheory.IsStoppingTime.add {Ω : Type u_1} {m : MeasurableSpace Ω} {f : Filtration ℕ m} {τ π : Ω → WithTop ℕ} (hτ : IsStoppingTime f τ) (hπ : IsStoppingTime f π) :
IsStoppingTime f (τ + π)
source
def MeasureTheory.IsStoppingTime.measurableSpace {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] {f : Filtration ι m} {τ : Ω → WithTop ι} (hτ : IsStoppingTime f τ) :
MeasurableSpace Ω

The associated σ-algebra with a stopping time.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
theorem MeasureTheory.IsStoppingTime.measurableSet {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] {f : Filtration ι m} {τ : Ω → WithTop ι} (hτ : IsStoppingTime f τ) (s : Set Ω) :
MeasurableSet s ↔ MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω : Ω | τ ω ≤ ↑i})
source
theorem MeasureTheory.IsStoppingTime.measurableSpace_mono {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] {f : Filtration ι m} {τ π : Ω → WithTop ι} (hτ : IsStoppingTime f τ) (hπ : IsStoppingTime f π) (hle : τ ≤ π) :
hτ.measurableSpace ≤ hπ.measurableSpace
source
theorem MeasureTheory.IsStoppingTime.measurableSpace_le {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] {f : Filtration ι m} {τ : Ω → WithTop ι} (hτ : IsStoppingTime f τ) :
hτ.measurableSpace ≤ m
source
@[deprecated MeasureTheory.IsStoppingTime.measurableSpace_le (since := "2025-09-08")]
theorem MeasureTheory.IsStoppingTime.measurableSpace_le_of_countable {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] {f : Filtration ι m} {τ : Ω → WithTop ι} (hτ : IsStoppingTime f τ) :
hτ.measurableSpace ≤ m

Alias of `MeasureTheory.IsStoppingTime.measurableSpace_le`.

source
@[deprecated MeasureTheory.IsStoppingTime.measurableSpace_le (since := "2025-09-08")]
theorem MeasureTheory.IsStoppingTime.measurableSpace_le_of_countable_range {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] {f : Filtration ι m} {τ : Ω → WithTop ι} (hτ : IsStoppingTime f τ) :
hτ.measurableSpace ≤ m

Alias of `MeasureTheory.IsStoppingTime.measurableSpace_le`.

source
@[simp]
theorem MeasureTheory.IsStoppingTime.measurableSpace_const {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] (f : Filtration ι m) (i : ι) :
⋯.measurableSpace = ↑f i
source
theorem MeasureTheory.IsStoppingTime.measurableSet_inter_eq_iff {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] {f : Filtration ι m} {τ : Ω → WithTop ι} (hτ : IsStoppingTime f τ) (s : Set Ω) (i : ι) :
MeasurableSet (s ∩ {ω : Ω | τ ω = ↑i}) ↔ MeasurableSet (s ∩ {ω : Ω | τ ω = ↑i})
source
theorem MeasureTheory.IsStoppingTime.measurableSpace_le_of_le_const {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] {f : Filtration ι m} {τ : Ω → WithTop ι} (hτ : IsStoppingTime f τ) {i : ι} (hτ_le : ∀ (ω : Ω), τ ω ≤ ↑i) :
hτ.measurableSpace ≤ ↑f i
source
theorem MeasureTheory.IsStoppingTime.measurableSpace_le_of_le {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] {f : Filtration ι m} {τ : Ω → WithTop ι} (hτ : IsStoppingTime f τ) {n : ι} (hτ_le : ∀ (ω : Ω), τ ω ≤ ↑n) :
hτ.measurableSpace ≤ m
source
theorem MeasureTheory.IsStoppingTime.le_measurableSpace_of_const_le {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] {f : Filtration ι m} {τ : Ω → WithTop ι} (hτ : IsStoppingTime f τ) {i : ι} (hτ_le : ∀ (ω : Ω), ↑i ≤ τ ω) :
↑f i ≤ hτ.measurableSpace
source
instance MeasureTheory.IsStoppingTime.sigmaFinite_stopping_time {Ω : Type u_1} {m : MeasurableSpace Ω} {ι : Type u_4} [SemilatticeSup ι] [OrderBot ι] {μ : Measure Ω} {f : Filtration ι m} {τ : Ω → WithTop ι} [SigmaFiniteFiltration μ f] (hτ : IsStoppingTime f τ) :
SigmaFinite (μ.trim ⋯)
source
instance MeasureTheory.IsStoppingTime.sigmaFinite_stopping_time_of_le {Ω : Type u_1} {m : MeasurableSpace Ω} {ι : Type u_4} [SemilatticeSup ι] [OrderBot ι] {μ : Measure Ω} {f : Filtration ι m} {τ : Ω → WithTop ι} [SigmaFiniteFiltration μ f] (hτ : IsStoppingTime f τ) {n : ι} (hτ_le : ∀ (ω : Ω), τ ω ≤ ↑n) :
SigmaFinite (μ.trim ⋯)
source
theorem MeasureTheory.IsStoppingTime.measurableSet_le' {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [LinearOrder ι] {f : Filtration ι m} {τ : Ω → WithTop ι} (hτ : IsStoppingTime f τ) (i : ι) :
MeasurableSet {ω : Ω | τ ω ≤ ↑i}
source
theorem MeasureTheory.IsStoppingTime.measurableSet_gt' {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [LinearOrder ι] {f : Filtration ι m} {τ : Ω → WithTop ι} (hτ : IsStoppingTime f τ) (i : ι) :
MeasurableSet {ω : Ω | ↑i < τ ω}
source
theorem MeasureTheory.IsStoppingTime.measurableSet_eq' {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [LinearOrder ι] {f : Filtration ι m} {τ : Ω → WithTop ι} [TopologicalSpace ι] [OrderTopology ι] [FirstCountableTopology ι] (hτ : IsStoppingTime f τ) (i : ι) :
MeasurableSet {ω : Ω | τ ω = ↑i}
source
theorem MeasureTheory.IsStoppingTime.measurableSet_ge' {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [LinearOrder ι] {f : Filtration ι m} {τ : Ω → WithTop ι} [TopologicalSpace ι] [OrderTopology ι] [FirstCountableTopology ι] (hτ : IsStoppingTime f τ) (i : ι) :
MeasurableSet {ω : Ω | ↑i ≤ τ ω}
source
theorem MeasureTheory.IsStoppingTime.measurableSet_lt' {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [LinearOrder ι] {f : Filtration ι m} {τ : Ω → WithTop ι} [TopologicalSpace ι] [OrderTopology ι] [FirstCountableTopology ι] (hτ : IsStoppingTime f τ) (i : ι) :
MeasurableSet {ω : Ω | τ ω < ↑i}
source
theorem MeasureTheory.IsStoppingTime.measurableSet_eq_of_countable_range' {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [LinearOrder ι] {f : Filtration ι m} {τ : Ω → WithTop ι} (hτ : IsStoppingTime f τ) (h_countable : (Set.range τ).Countable) (i : ι) :
MeasurableSet {ω : Ω | τ ω = ↑i}
source
theorem MeasureTheory.IsStoppingTime.measurableSet_eq_of_countable' {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [LinearOrder ι] {f : Filtration ι m} {τ : Ω → WithTop ι} [Countable ι] (hτ : IsStoppingTime f τ) (i : ι) :
MeasurableSet {ω : Ω | τ ω = ↑i}
source
theorem MeasureTheory.IsStoppingTime.measurableSet_ge_of_countable_range' {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [LinearOrder ι] {f : Filtration ι m} {τ : Ω → WithTop ι} (hτ : IsStoppingTime f τ) (h_countable : (Set.range τ).Countable) (i : ι) :
MeasurableSet {ω : Ω | ↑i ≤ τ ω}
source
theorem MeasureTheory.IsStoppingTime.measurableSet_ge_of_countable' {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [LinearOrder ι] {f : Filtration ι m} {τ : Ω → WithTop ι} [Countable ι] (hτ : IsStoppingTime f τ) (i : ι) :
MeasurableSet {ω : Ω | ↑i ≤ τ ω}
source
theorem MeasureTheory.IsStoppingTime.measurableSet_lt_of_countable_range' {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [LinearOrder ι] {f : Filtration ι m} {τ : Ω → WithTop ι} (hτ : IsStoppingTime f τ) (h_countable : (Set.range τ).Countable) (i : ι) :
MeasurableSet {ω : Ω | τ ω < ↑i}
source
theorem MeasureTheory.IsStoppingTime.measurableSet_lt_of_countable' {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [LinearOrder ι] {f : Filtration ι m} {τ : Ω → WithTop ι} [Countable ι] (hτ : IsStoppingTime f τ) (i : ι) :
MeasurableSet {ω : Ω | τ ω < ↑i}
source
theorem MeasureTheory.IsStoppingTime.measurable {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [LinearOrder ι] {f : Filtration ι m} {τ : Ω → WithTop ι} [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] (hτ : IsStoppingTime f τ) :
Measurable τ
source
theorem MeasureTheory.IsStoppingTime.measurable' {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [LinearOrder ι] {f : Filtration ι m} {τ : Ω → WithTop ι} [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] (hτ : IsStoppingTime f τ) :
Measurable τ
source
theorem MeasureTheory.IsStoppingTime.measurableSet_eq_top {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [LinearOrder ι] {f : Filtration ι m} {τ : Ω → WithTop ι} [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] (hτ : IsStoppingTime f τ) :
MeasurableSet {ω : Ω | τ ω = ⊤}
source
theorem MeasureTheory.IsStoppingTime.measurable_of_le {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [LinearOrder ι] {f : Filtration ι m} {τ : Ω → WithTop ι} [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] (hτ : IsStoppingTime f τ) {i : ι} (hτ_le : ∀ (ω : Ω), τ ω ≤ ↑i) :
Measurable τ
source
theorem MeasureTheory.IsStoppingTime.measurableSpace_min {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [LinearOrder ι] {f : Filtration ι m} {τ π : Ω → WithTop ι} (hτ : IsStoppingTime f τ) (hπ : IsStoppingTime f π) :
⋯.measurableSpace = hτ.measurableSpace ⊓ hπ.measurableSpace
source
theorem MeasureTheory.IsStoppingTime.measurableSet_min_iff {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [LinearOrder ι] {f : Filtration ι m} {τ π : Ω → WithTop ι} (hτ : IsStoppingTime f τ) (hπ : IsStoppingTime f π) (s : Set Ω) :
MeasurableSet s ↔ MeasurableSet s ∧ MeasurableSet s
source
theorem MeasureTheory.IsStoppingTime.measurableSpace_min_const {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [LinearOrder ι] {f : Filtration ι m} {τ : Ω → WithTop ι} (hτ : IsStoppingTime f τ) {i : ι} :
⋯.measurableSpace = hτ.measurableSpace ⊓ ↑f i
source
theorem MeasureTheory.IsStoppingTime.measurableSet_min_const_iff {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [LinearOrder ι] {f : Filtration ι m} {τ : Ω → WithTop ι} (hτ : IsStoppingTime f τ) (s : Set Ω) {i : ι} :
MeasurableSet s ↔ MeasurableSet s ∧ MeasurableSet s
source
theorem MeasureTheory.IsStoppingTime.measurableSet_inter_le {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [LinearOrder ι] {f : Filtration ι m} {τ π : Ω → WithTop ι} [TopologicalSpace ι] [SecondCountableTopology ι] [OrderTopology ι] (hτ : IsStoppingTime f τ) (hπ : IsStoppingTime f π) (s : Set Ω) (hs : MeasurableSet s) :
MeasurableSet (s ∩ {ω : Ω | τ ω ≤ π ω})
source
theorem MeasureTheory.IsStoppingTime.measurableSet_inter_le_iff {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [LinearOrder ι] {f : Filtration ι m} {τ π : Ω → WithTop ι} [TopologicalSpace ι] [SecondCountableTopology ι] [OrderTopology ι] (hτ : IsStoppingTime f τ) (hπ : IsStoppingTime f π) (s : Set Ω) :
MeasurableSet (s ∩ {ω : Ω | τ ω ≤ π ω}) ↔ MeasurableSet (s ∩ {ω : Ω | τ ω ≤ π ω})
source
theorem MeasureTheory.IsStoppingTime.measurableSet_inter_le_const_iff {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [LinearOrder ι] {f : Filtration ι m} {τ : Ω → WithTop ι} (hτ : IsStoppingTime f τ) (s : Set Ω) (i : ι) :
MeasurableSet (s ∩ {ω : Ω | τ ω ≤ ↑i}) ↔ MeasurableSet (s ∩ {ω : Ω | τ ω ≤ ↑i})
source
theorem MeasureTheory.IsStoppingTime.measurableSet_le_stopping_time {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [LinearOrder ι] {f : Filtration ι m} {τ π : Ω → WithTop ι} [TopologicalSpace ι] [SecondCountableTopology ι] [OrderTopology ι] (hτ : IsStoppingTime f τ) (hπ : IsStoppingTime f π) :
MeasurableSet {ω : Ω | τ ω ≤ π ω}
source
theorem MeasureTheory.IsStoppingTime.measurableSet_stopping_time_le_min {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [LinearOrder ι] {f : Filtration ι m} {τ π : Ω → WithTop ι} [TopologicalSpace ι] [SecondCountableTopology ι] [OrderTopology ι] (hτ : IsStoppingTime f τ) (hπ : IsStoppingTime f π) :
MeasurableSet {ω : Ω | τ ω ≤ π ω}
source
theorem MeasureTheory.IsStoppingTime.measurableSet_stopping_time_le {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [LinearOrder ι] {f : Filtration ι m} {τ π : Ω → WithTop ι} [TopologicalSpace ι] [SecondCountableTopology ι] [OrderTopology ι] (hτ : IsStoppingTime f τ) (hπ : IsStoppingTime f π) :
MeasurableSet {ω : Ω | τ ω ≤ π ω}
source
theorem MeasureTheory.IsStoppingTime.measurableSet_eq_stopping_time_min {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [LinearOrder ι] {f : Filtration ι m} {τ π : Ω → WithTop ι} [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] (hτ : IsStoppingTime f τ) (hπ : IsStoppingTime f π) :
MeasurableSet {ω : Ω | τ ω = π ω}
source
theorem MeasureTheory.IsStoppingTime.measurableSet_eq_stopping_time {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [LinearOrder ι] {f : Filtration ι m} {τ π : Ω → WithTop ι} [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] (hτ : IsStoppingTime f τ) (hπ : IsStoppingTime f π) :
MeasurableSet {ω : Ω | τ ω = π ω}
source
@[deprecated MeasureTheory.IsStoppingTime.measurableSet_eq_stopping_time (since := "2025-09-08")]
theorem MeasureTheory.IsStoppingTime.measurableSet_eq_stopping_time_of_countable {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [LinearOrder ι] {f : Filtration ι m} {τ π : Ω → WithTop ι} [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] (hτ : IsStoppingTime f τ) (hπ : IsStoppingTime f π) :
MeasurableSet {ω : Ω | τ ω = π ω}

Alias of `MeasureTheory.IsStoppingTime.measurableSet_eq_stopping_time`.

## Stopped value and stopped process #

source
noncomputable def MeasureTheory.stoppedValue {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [Nonempty ι] (u : ι → Ω → β) (τ : Ω → WithTop ι) :
Ω → β

Given a map `u : ι → Ω → E`, its stopped value with respect to the stopping time `τ` is the map `x ↦ u (τ ω) ω`.

Equations

- MeasureTheory.stoppedValue u τ ω = u (τ ω).untopA ω

Instances For

source
theorem MeasureTheory.stoppedValue_const {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [Nonempty ι] (u : ι → Ω → β) (i : ι) :
(stoppedValue u fun (x : Ω) => ↑i) = u i
source
noncomputable def MeasureTheory.stoppedProcess {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [Nonempty ι] [LinearOrder ι] (u : ι → Ω → β) (τ : Ω → WithTop ι) :
ι → Ω → β

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

- MeasureTheory.stoppedProcess u τ i ω = u (min (↑i) (τ ω)).untopA ω

Instances For

source
theorem MeasureTheory.stoppedProcess_eq_stoppedValue {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [Nonempty ι] [LinearOrder ι] {u : ι → Ω → β} {τ : Ω → WithTop ι} :
stoppedProcess u τ = fun (i : ι) => stoppedValue u fun (ω : Ω) => min (↑i) (τ ω)
source
theorem MeasureTheory.stoppedValue_stoppedProcess {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [Nonempty ι] [LinearOrder ι] {u : ι → Ω → β} {τ σ : Ω → WithTop ι} :
stoppedValue (stoppedProcess u τ) σ = fun (ω : Ω) => if σ ω ≠ ⊤ then stoppedValue u (fun (ω : Ω) => min (σ ω) (τ ω)) ω else stoppedValue u (fun (ω : Ω) => min (↑(Classical.arbitrary ι)) (τ ω)) ω
source
theorem MeasureTheory.stoppedValue_stoppedProcess_ae_eq {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [Nonempty ι] [LinearOrder ι] {u : ι → Ω → β} {τ σ : Ω → WithTop ι} {μ : Measure Ω} (hσ : ∀ᵐ (ω : Ω) ∂μ, σ ω ≠ ⊤) :
stoppedValue (stoppedProcess u τ) σ =ᶠ[ae μ] stoppedValue u fun (ω : Ω) => min (σ ω) (τ ω)
source
theorem MeasureTheory.stoppedProcess_eq_of_le {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [Nonempty ι] [LinearOrder ι] {u : ι → Ω → β} {τ : Ω → WithTop ι} {i : ι} {ω : Ω} (h : ↑i ≤ τ ω) :
stoppedProcess u τ i ω = u i ω
source
theorem MeasureTheory.stoppedProcess_eq_of_ge {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [Nonempty ι] [LinearOrder ι] {u : ι → Ω → β} {τ : Ω → WithTop ι} {i : ι} {ω : Ω} (h : τ ω ≤ ↑i) :
stoppedProcess u τ i ω = u (τ ω).untopA ω
source
theorem MeasureTheory.progMeasurable_min_stopping_time {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Nonempty ι] [LinearOrder ι] [MeasurableSpace ι] [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] [BorelSpace ι] {τ : Ω → WithTop ι} {f : Filtration ι m} [TopologicalSpace.PseudoMetrizableSpace ι] (hτ : IsStoppingTime f τ) :
ProgMeasurable f fun (i : ι) (ω : Ω) => (min (↑i) (τ ω)).untopA
source
theorem MeasureTheory.ProgMeasurable.stoppedProcess {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [Nonempty ι] [LinearOrder ι] [MeasurableSpace ι] [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] [BorelSpace ι] [TopologicalSpace β] {u : ι → Ω → β} {τ : Ω → WithTop ι} {f : Filtration ι m} [TopologicalSpace.PseudoMetrizableSpace ι] (h : ProgMeasurable f u) (hτ : IsStoppingTime f τ) :
ProgMeasurable f (MeasureTheory.stoppedProcess u τ)
source
theorem MeasureTheory.ProgMeasurable.adapted_stoppedProcess {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [Nonempty ι] [LinearOrder ι] [MeasurableSpace ι] [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] [BorelSpace ι] [TopologicalSpace β] {u : ι → Ω → β} {τ : Ω → WithTop ι} {f : Filtration ι m} [TopologicalSpace.PseudoMetrizableSpace ι] (h : ProgMeasurable f u) (hτ : IsStoppingTime f τ) :
Adapted f (MeasureTheory.stoppedProcess u τ)
source
theorem MeasureTheory.ProgMeasurable.stronglyMeasurable_stoppedProcess {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [Nonempty ι] [LinearOrder ι] [MeasurableSpace ι] [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] [BorelSpace ι] [TopologicalSpace β] {u : ι → Ω → β} {τ : Ω → WithTop ι} {f : Filtration ι m} [TopologicalSpace.PseudoMetrizableSpace ι] (hu : ProgMeasurable f u) (hτ : IsStoppingTime f τ) (i : ι) :
StronglyMeasurable (MeasureTheory.stoppedProcess u τ i)
source
theorem MeasureTheory.stronglyMeasurable_stoppedValue_of_le {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [Nonempty ι] [LinearOrder ι] [MeasurableSpace ι] [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] [BorelSpace ι] [TopologicalSpace β] {u : ι → Ω → β} {τ : Ω → WithTop ι} {f : Filtration ι m} (h : ProgMeasurable f u) (hτ : IsStoppingTime f τ) {n : ι} (hτ_le : ∀ (ω : Ω), τ ω ≤ ↑n) :
StronglyMeasurable (stoppedValue u τ)
source
theorem MeasureTheory.measurableSet_preimage_stoppedValue_inter {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [Nonempty ι] [LinearOrder ι] [MeasurableSpace ι] [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] [BorelSpace ι] [TopologicalSpace β] {u : ι → Ω → β} {τ : Ω → WithTop ι} {f : Filtration ι m} [TopologicalSpace.PseudoMetrizableSpace β] [MeasurableSpace β] [BorelSpace β] (hf_prog : ProgMeasurable f u) (hτ : IsStoppingTime f τ) {t : Set β} (ht : MeasurableSet t) (i : ι) :
MeasurableSet (stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω ≤ ↑i})
source
theorem MeasureTheory.measurable_stoppedValue {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [Nonempty ι] [LinearOrder ι] [MeasurableSpace ι] [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] [BorelSpace ι] [TopologicalSpace β] {u : ι → Ω → β} {τ : Ω → WithTop ι} {f : Filtration ι m} [TopologicalSpace.PseudoMetrizableSpace β] [MeasurableSpace β] [BorelSpace β] (hf_prog : ProgMeasurable f u) (hτ : IsStoppingTime f τ) :
Measurable (stoppedValue u τ)
source
theorem MeasureTheory.stoppedValue_eq_of_mem_finset {Ω : Type u_1} {ι : Type u_3} [Nonempty ι] {τ : Ω → WithTop ι} {E : Type u_4} {u : ι → Ω → E} [AddCommMonoid E] {s : Finset ι} (hbdd : ∀ (ω : Ω), τ ω ∈ WithTop.some '' ↑s) :
stoppedValue u τ = ∑ i ∈ s, {ω : Ω | τ ω = ↑i}.indicator (u i)
source
theorem MeasureTheory.stoppedValue_eq' {Ω : Type u_1} {ι : Type u_3} [Nonempty ι] {τ : Ω → WithTop ι} {E : Type u_4} {u : ι → Ω → E} [Preorder ι] [LocallyFiniteOrderBot ι] [AddCommMonoid E] {N : ι} (hbdd : ∀ (ω : Ω), τ ω ≤ ↑N) :
stoppedValue u τ = ∑ i ∈ Finset.Iic N, {ω : Ω | τ ω = ↑i}.indicator (u i)
source
theorem MeasureTheory.stoppedProcess_eq_of_mem_finset {Ω : Type u_1} {ι : Type u_3} [Nonempty ι] {τ : Ω → WithTop ι} {E : Type u_4} {u : ι → Ω → E} [LinearOrder ι] [AddCommMonoid E] {s : Finset ι} (n : ι) (hbdd : ∀ (ω : Ω), τ ω < ↑n → τ ω ∈ WithTop.some '' ↑s) :
stoppedProcess u τ n = {a : Ω | ↑n ≤ τ a}.indicator (u n) + ∑ i ∈ s with i < n, {ω : Ω | τ ω = ↑i}.indicator (u i)
source
theorem MeasureTheory.stoppedProcess_eq'' {Ω : Type u_1} {ι : Type u_3} [Nonempty ι] {τ : Ω → WithTop ι} {E : Type u_4} {u : ι → Ω → E} [LinearOrder ι] [LocallyFiniteOrderBot ι] [AddCommMonoid E] (n : ι) :
stoppedProcess u τ n = {a : Ω | ↑n ≤ τ a}.indicator (u n) + ∑ i ∈ Finset.Iio n, {ω : Ω | τ ω = ↑i}.indicator (u i)
source
theorem MeasureTheory.memLp_stoppedValue_of_mem_finset {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Nonempty ι] {μ : Measure Ω} {τ : Ω → WithTop ι} {E : Type u_4} {p : ENNReal} {u : ι → Ω → E} [PartialOrder ι] {ℱ : Filtration ι m} [NormedAddCommGroup E] (hτ : IsStoppingTime ℱ τ) (hu : ∀ (n : ι), MemLp (u n) p μ) {s : Finset ι} (hbdd : ∀ (ω : Ω), τ ω ∈ WithTop.some '' ↑s) :
MemLp (stoppedValue u τ) p μ
source
theorem MeasureTheory.memLp_stoppedValue {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Nonempty ι] {μ : Measure Ω} {τ : Ω → WithTop ι} {E : Type u_4} {p : ENNReal} {u : ι → Ω → E} [PartialOrder ι] {ℱ : Filtration ι m} [NormedAddCommGroup E] [LocallyFiniteOrderBot ι] (hτ : IsStoppingTime ℱ τ) (hu : ∀ (n : ι), MemLp (u n) p μ) {N : ι} (hbdd : ∀ (ω : Ω), τ ω ≤ ↑N) :
MemLp (stoppedValue u τ) p μ
source
theorem MeasureTheory.integrable_stoppedValue_of_mem_finset {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Nonempty ι] {μ : Measure Ω} {τ : Ω → WithTop ι} {E : Type u_4} {u : ι → Ω → E} [PartialOrder ι] {ℱ : Filtration ι m} [NormedAddCommGroup E] (hτ : IsStoppingTime ℱ τ) (hu : ∀ (n : ι), Integrable (u n) μ) {s : Finset ι} (hbdd : ∀ (ω : Ω), τ ω ∈ WithTop.some '' ↑s) :
Integrable (stoppedValue u τ) μ
source
theorem MeasureTheory.integrable_stoppedValue {Ω : Type u_1} (ι : Type u_3) {m : MeasurableSpace Ω} [Nonempty ι] {μ : Measure Ω} {τ : Ω → WithTop ι} {E : Type u_4} {u : ι → Ω → E} [PartialOrder ι] {ℱ : Filtration ι m} [NormedAddCommGroup E] [LocallyFiniteOrderBot ι] (hτ : IsStoppingTime ℱ τ) (hu : ∀ (n : ι), Integrable (u n) μ) {N : ι} (hbdd : ∀ (ω : Ω), τ ω ≤ ↑N) :
Integrable (stoppedValue u τ) μ
source
theorem MeasureTheory.memLp_stoppedProcess_of_mem_finset {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Nonempty ι] {μ : Measure Ω} {τ : Ω → WithTop ι} {E : Type u_4} {p : ENNReal} {u : ι → Ω → E} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [FirstCountableTopology ι] {ℱ : Filtration ι m} [NormedAddCommGroup E] (hτ : IsStoppingTime ℱ τ) (hu : ∀ (n : ι), MemLp (u n) p μ) (n : ι) {s : Finset ι} (hbdd : ∀ (ω : Ω), τ ω < ↑n → τ ω ∈ WithTop.some '' ↑s) :
MemLp (stoppedProcess u τ n) p μ
source
theorem MeasureTheory.memLp_stoppedProcess {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Nonempty ι] {μ : Measure Ω} {τ : Ω → WithTop ι} {E : Type u_4} {p : ENNReal} {u : ι → Ω → E} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [FirstCountableTopology ι] {ℱ : Filtration ι m} [NormedAddCommGroup E] [LocallyFiniteOrderBot ι] (hτ : IsStoppingTime ℱ τ) (hu : ∀ (n : ι), MemLp (u n) p μ) (n : ι) :
MemLp (stoppedProcess u τ n) p μ
source
theorem MeasureTheory.integrable_stoppedProcess_of_mem_finset {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Nonempty ι] {μ : Measure Ω} {τ : Ω → WithTop ι} {E : Type u_4} {u : ι → Ω → E} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [FirstCountableTopology ι] {ℱ : Filtration ι m} [NormedAddCommGroup E] (hτ : IsStoppingTime ℱ τ) (hu : ∀ (n : ι), Integrable (u n) μ) (n : ι) {s : Finset ι} (hbdd : ∀ (ω : Ω), τ ω < ↑n → τ ω ∈ WithTop.some '' ↑s) :
Integrable (stoppedProcess u τ n) μ
source
theorem MeasureTheory.integrable_stoppedProcess {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Nonempty ι] {μ : Measure Ω} {τ : Ω → WithTop ι} {E : Type u_4} {u : ι → Ω → E} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [FirstCountableTopology ι] {ℱ : Filtration ι m} [NormedAddCommGroup E] [LocallyFiniteOrderBot ι] (hτ : IsStoppingTime ℱ τ) (hu : ∀ (n : ι), Integrable (u n) μ) (n : ι) :
Integrable (stoppedProcess u τ n) μ
source
theorem MeasureTheory.Adapted.stoppedProcess {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [Nonempty ι] [LinearOrder ι] [TopologicalSpace ι] [SecondCountableTopology ι] [OrderTopology ι] [MeasurableSpace ι] [BorelSpace ι] {f : Filtration ι m} {u : ι → Ω → β} {τ : Ω → WithTop ι} [TopologicalSpace.MetrizableSpace ι] (hu : Adapted f u) (hu_cont : ∀ (ω : Ω), Continuous fun (i : ι) => u i ω) (hτ : IsStoppingTime f τ) :
Adapted f (MeasureTheory.stoppedProcess u τ)

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

source
theorem MeasureTheory.Adapted.stoppedProcess_of_discrete {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [Nonempty ι] [LinearOrder ι] [TopologicalSpace ι] [SecondCountableTopology ι] [OrderTopology ι] [MeasurableSpace ι] [BorelSpace ι] {f : Filtration ι m} {u : ι → Ω → β} {τ : Ω → WithTop ι} [DiscreteTopology ι] (hu : Adapted f u) (hτ : IsStoppingTime f τ) :
Adapted f (MeasureTheory.stoppedProcess u τ)

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

source
theorem MeasureTheory.Adapted.stronglyMeasurable_stoppedProcess {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [Nonempty ι] [LinearOrder ι] [TopologicalSpace ι] [SecondCountableTopology ι] [OrderTopology ι] [MeasurableSpace ι] [BorelSpace ι] {f : Filtration ι m} {u : ι → Ω → β} {τ : Ω → WithTop ι} [TopologicalSpace.MetrizableSpace ι] (hu : Adapted f u) (hu_cont : ∀ (ω : Ω), Continuous fun (i : ι) => u i ω) (hτ : IsStoppingTime f τ) (n : ι) :
StronglyMeasurable (MeasureTheory.stoppedProcess u τ n)
source
theorem MeasureTheory.Adapted.stronglyMeasurable_stoppedProcess_of_discrete {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [Nonempty ι] [LinearOrder ι] [TopologicalSpace ι] [SecondCountableTopology ι] [OrderTopology ι] [MeasurableSpace ι] [BorelSpace ι] {f : Filtration ι m} {u : ι → Ω → β} {τ : Ω → WithTop ι} [DiscreteTopology ι] (hu : Adapted f u) (hτ : IsStoppingTime f τ) (n : ι) :
StronglyMeasurable (MeasureTheory.stoppedProcess u τ n)

### Filtrations indexed by `ℕ` #

source
theorem MeasureTheory.stoppedValue_sub_eq_sum {Ω : Type u_1} {β : Type u_2} {u : ℕ → Ω → β} {τ π : Ω → ℕ∞} [AddCommGroup β] (hle : τ ≤ π) (hπ : ∀ (ω : Ω), ↑(π ω) ≠ ⊤) :
stoppedValue u π - stoppedValue u τ = fun (ω : Ω) => (∑ i ∈ Finset.Ico (WithTop.untopA (τ ω)) (WithTop.untopA (π ω)), (u (i + 1) - u i)) ω
source
theorem MeasureTheory.stoppedValue_sub_eq_sum' {Ω : Type u_1} {β : Type u_2} {u : ℕ → Ω → β} {τ π : Ω → ℕ∞} [AddCommGroup β] (hle : τ ≤ π) {N : ℕ} (hbdd : ∀ (ω : Ω), π ω ≤ ↑N) :
stoppedValue u π - stoppedValue u τ = fun (ω : Ω) => (∑ i ∈ Finset.range (N + 1), {ω : Ω | τ ω ≤ ↑i ∧ ↑i < π ω}.indicator (u (i + 1) - u i)) ω
source
theorem MeasureTheory.stoppedValue_eq {Ω : Type u_1} {β : Type u_2} {u : ℕ → Ω → β} {τ : Ω → ℕ∞} [AddCommMonoid β] {N : ℕ} (hbdd : ∀ (ω : Ω), τ ω ≤ ↑N) :
stoppedValue u τ = fun (x : Ω) => (∑ i ∈ Finset.range (N + 1), {ω : Ω | τ ω = ↑i}.indicator (u i)) x
source
theorem MeasureTheory.stoppedProcess_eq {Ω : Type u_1} {β : Type u_2} {u : ℕ → Ω → β} {τ : Ω → ℕ∞} [AddCommMonoid β] (n : ℕ) :
stoppedProcess u τ n = {a : Ω | ↑n ≤ τ a}.indicator (u n) + ∑ i ∈ Finset.range n, {ω : Ω | τ ω = ↑i}.indicator (u i)
source
theorem MeasureTheory.stoppedProcess_eq' {Ω : Type u_1} {β : Type u_2} {u : ℕ → Ω → β} {τ : Ω → ℕ∞} [AddCommMonoid β] (n : ℕ) :
stoppedProcess u τ n = {a : Ω | ↑n + 1 ≤ τ a}.indicator (u n) + ∑ i ∈ Finset.range (n + 1), {a : Ω | τ a = ↑i}.indicator (u i)
source
theorem MeasureTheory.IsStoppingTime.piecewise_of_le {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] {𝒢 : Filtration ι m} {τ η : Ω → WithTop ι} {i : ι} {s : Set Ω} [DecidablePred fun (x : Ω) => x ∈ s] (hτ_st : IsStoppingTime 𝒢 τ) (hη_st : IsStoppingTime 𝒢 η) (hτ : ∀ (ω : Ω), ↑i ≤ τ ω) (hη : ∀ (ω : Ω), ↑i ≤ η ω) (hs : MeasurableSet s) :
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.

source
theorem MeasureTheory.isStoppingTime_piecewise_const {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] {𝒢 : Filtration ι m} {i j : ι} {s : Set Ω} [DecidablePred fun (x : Ω) => x ∈ s] (hij : i ≤ j) (hs : MeasurableSet s) :
IsStoppingTime 𝒢 (s.piecewise (fun (x : Ω) => ↑i) fun (x : Ω) => ↑j)
source
theorem MeasureTheory.stoppedValue_piecewise_const {Ω : Type u_1} {s : Set Ω} [DecidablePred fun (x : Ω) => x ∈ s] {ι' : Type u_4} [Nonempty ι'] {i j : ι'} {f : ι' → Ω → ℝ} :
stoppedValue f (s.piecewise (fun (x : Ω) => ↑i) fun (x : Ω) => ↑j) = s.piecewise (f i) (f j)
source
theorem MeasureTheory.stoppedValue_piecewise_const' {Ω : Type u_1} {s : Set Ω} [DecidablePred fun (x : Ω) => x ∈ s] {ι' : Type u_4} [Nonempty ι'] {i j : ι'} {f : ι' → Ω → ℝ} :
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 #

source
theorem MeasureTheory.condExp_stopping_time_ae_eq_restrict_eq_of_countable_range {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [LinearOrder ι] {μ : Measure Ω} {ℱ : Filtration ι m} {τ : Ω → WithTop ι} {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : Ω → E} [SigmaFiniteFiltration μ ℱ] (hτ : IsStoppingTime ℱ τ) (h_countable : (Set.range τ).Countable) [SigmaFinite (μ.trim ⋯)] (i : ι) :
μ[f|hτ.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x = ↑i})] μ[f|↑ℱ i]
source
theorem MeasureTheory.condExp_stopping_time_ae_eq_restrict_eq_of_countable {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [LinearOrder ι] {μ : Measure Ω} {ℱ : Filtration ι m} {τ : Ω → WithTop ι} {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : Ω → E} [Countable ι] [SigmaFiniteFiltration μ ℱ] (hτ : IsStoppingTime ℱ τ) [SigmaFinite (μ.trim ⋯)] (i : ι) :
μ[f|hτ.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x = ↑i})] μ[f|↑ℱ i]
source
theorem MeasureTheory.condExp_min_stopping_time_ae_eq_restrict_le_const {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [LinearOrder ι] {μ : Measure Ω} {ℱ : Filtration ι m} {τ : Ω → WithTop ι} {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : Ω → E} (hτ : IsStoppingTime ℱ τ) (i : ι) [SigmaFinite (μ.trim ⋯)] :
μ[f|⋯.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x ≤ ↑i})] μ[f|hτ.measurableSpace]
source
theorem MeasureTheory.condExp_stopping_time_ae_eq_restrict_eq {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [LinearOrder ι] {μ : Measure Ω} {ℱ : Filtration ι m} {τ : Ω → WithTop ι} {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : Ω → E} [TopologicalSpace ι] [OrderTopology ι] [FirstCountableTopology ι] [SigmaFiniteFiltration μ ℱ] (hτ : IsStoppingTime ℱ τ) [SigmaFinite (μ.trim ⋯)] (i : ι) :
μ[f|hτ.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x = ↑i})] μ[f|↑ℱ i]
source
theorem MeasureTheory.condExp_min_stopping_time_ae_eq_restrict_le {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [LinearOrder ι] {μ : Measure Ω} {ℱ : Filtration ι m} {τ σ : Ω → WithTop ι} {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : Ω → E} [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] (hτ : IsStoppingTime ℱ τ) (hσ : IsStoppingTime ℱ σ) [SigmaFinite (μ.trim ⋯)] :
μ[f|⋯.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x ≤ σ x})] μ[f|hτ.measurableSpace]