Stopping times, stopped processes and stopped values #
Definition and properties of stopping times.
Main definitions #
MeasureTheory.IsStoppingTime: a stopping time with respect to some filtrationfon a measurable spaceΩis a functionτ : Ω → WithTop ιsuch that for alli : ι, the preimage of{j | j ≤ i}alongτisf i-measurableMeasureTheory.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ℒpat every time inℕ, then its stopped process belongs toℒpas 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 #
def
MeasureTheory.IsStoppingTime
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
(f : Filtration ι m)
(τ : Ω → WithTop ι)
:
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
theorem
MeasureTheory.isStoppingTime_const
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
(f : Filtration ι m)
(i : ι)
:
IsStoppingTime f fun (x : Ω) => ↑i
theorem
MeasureTheory.IsStoppingTime.measurableSet_le
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{τ : Ω → WithTop ι}
(hτ : IsStoppingTime f τ)
(i : ι)
:
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 : ι)
:
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 : ι)
:
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 : ι)
:
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 : ι)
:
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 : ι)
:
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 : ι)
:
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 : ι)
:
theorem
MeasureTheory.IsStoppingTime.measurableSet_gt
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[LinearOrder ι]
{f : Filtration ι m}
{τ : Ω → WithTop ι}
(hτ : IsStoppingTime f τ)
(i : ι)
:
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)
:
Auxiliary lemma for MeasureTheory.IsStoppingTime.measurableSet_lt.
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 : ι)
:
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 : ι)
:
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 : ι)
:
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)
:
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)
:
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 τ
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 (τ ω) (π ω)
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
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 (τ ω) (π ω)
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
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
theorem
MeasureTheory.IsStoppingTime.add_const_nat
{Ω : Type u_1}
{m : MeasurableSpace Ω}
{f : Filtration ℕ m}
{τ : Ω → WithTop ℕ}
(hτ : IsStoppingTime f τ)
{i : ℕ}
:
IsStoppingTime f fun (ω : Ω) => τ ω + ↑i
theorem
MeasureTheory.IsStoppingTime.add
{Ω : Type u_1}
{m : MeasurableSpace Ω}
{f : Filtration ℕ m}
{τ π : Ω → WithTop ℕ}
(hτ : IsStoppingTime f τ)
(hπ : IsStoppingTime f π)
:
IsStoppingTime f (τ + π)
def
MeasureTheory.IsStoppingTime.measurableSpace
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{τ : Ω → WithTop ι}
(hτ : IsStoppingTime f τ)
:
The associated σ-algebra with a stopping time.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
MeasureTheory.IsStoppingTime.measurableSet
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{τ : Ω → WithTop ι}
(hτ : IsStoppingTime f τ)
(s : Set Ω)
:
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 : τ ≤ π)
:
theorem
MeasureTheory.IsStoppingTime.measurableSpace_le
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{τ : Ω → WithTop ι}
(hτ : IsStoppingTime f τ)
:
@[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 τ)
:
@[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 τ)
:
@[simp]
theorem
MeasureTheory.IsStoppingTime.measurableSpace_const
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
(f : Filtration ι m)
(i : ι)
:
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 : ι)
:
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)
:
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)
:
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 ≤ τ ω)
:
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 ⋯)
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 ⋯)
theorem
MeasureTheory.IsStoppingTime.measurableSet_le'
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[LinearOrder ι]
{f : Filtration ι m}
{τ : Ω → WithTop ι}
(hτ : IsStoppingTime f τ)
(i : ι)
:
theorem
MeasureTheory.IsStoppingTime.measurableSet_gt'
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[LinearOrder ι]
{f : Filtration ι m}
{τ : Ω → WithTop ι}
(hτ : IsStoppingTime f τ)
(i : ι)
:
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 : ι)
:
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 : ι)
:
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 : ι)
:
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 : ι)
:
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 : ι)
:
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 : ι)
:
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 : ι)
:
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 : ι)
:
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 : ι)
:
theorem
MeasureTheory.IsStoppingTime.measurable
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[LinearOrder ι]
{f : Filtration ι m}
{τ : Ω → WithTop ι}
[TopologicalSpace ι]
[OrderTopology ι]
[SecondCountableTopology ι]
(hτ : IsStoppingTime f τ)
:
theorem
MeasureTheory.IsStoppingTime.measurable'
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[LinearOrder ι]
{f : Filtration ι m}
{τ : Ω → WithTop ι}
[TopologicalSpace ι]
[OrderTopology ι]
[SecondCountableTopology ι]
(hτ : IsStoppingTime f τ)
:
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 τ)
:
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)
:
theorem
MeasureTheory.IsStoppingTime.measurableSpace_min
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[LinearOrder ι]
{f : Filtration ι m}
{τ π : Ω → WithTop ι}
(hτ : IsStoppingTime f τ)
(hπ : IsStoppingTime f π)
:
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 Ω)
:
theorem
MeasureTheory.IsStoppingTime.measurableSpace_min_const
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[LinearOrder ι]
{f : Filtration ι m}
{τ : Ω → WithTop ι}
(hτ : IsStoppingTime f τ)
{i : ι}
:
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 : ι}
:
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)
:
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 Ω)
:
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 : ι)
:
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 π)
:
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 π)
:
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 π)
:
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 π)
:
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 π)
:
@[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 π)
:
Alias of MeasureTheory.IsStoppingTime.measurableSet_eq_stopping_time.
Stopped value and stopped process #
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
theorem
MeasureTheory.stoppedValue_const
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[Nonempty ι]
(u : ι → Ω → β)
(i : ι)
:
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
theorem
MeasureTheory.stoppedProcess_eq_stoppedValue
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[Nonempty ι]
[LinearOrder ι]
{u : ι → Ω → β}
{τ : Ω → WithTop ι}
:
theorem
MeasureTheory.stoppedProcess_eq_stoppedValue_apply
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[Nonempty ι]
[LinearOrder ι]
{u : ι → Ω → β}
{τ : Ω → WithTop ι}
(i : ι)
(ω : Ω)
:
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 ι)) (τ ω)) ω
theorem
MeasureTheory.stoppedValue_stoppedProcess_apply
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[Nonempty ι]
[LinearOrder ι]
{u : ι → Ω → β}
{τ σ : Ω → WithTop ι}
{ω : Ω}
(hω : σ ω ≠ ⊤)
:
theorem
MeasureTheory.stoppedValue_stoppedProcess_ae_eq
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Nonempty ι]
[LinearOrder ι]
{u : ι → Ω → β}
{τ σ : Ω → WithTop ι}
{μ : Measure Ω}
(hσ : ∀ᵐ (ω : Ω) ∂μ, σ ω ≠ ⊤)
:
theorem
MeasureTheory.stoppedProcess_eq_of_le
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[Nonempty ι]
[LinearOrder ι]
{u : ι → Ω → β}
{τ : Ω → WithTop ι}
{i : ι}
{ω : Ω}
(h : ↑i ≤ τ ω)
:
theorem
MeasureTheory.stoppedProcess_eq_of_ge
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[Nonempty ι]
[LinearOrder ι]
{u : ι → Ω → β}
{τ : Ω → WithTop ι}
{i : ι}
{ω : Ω}
(h : τ ω ≤ ↑i)
:
theorem
MeasureTheory.stoppedProcess_indicator_comm
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[Nonempty ι]
[LinearOrder ι]
{u : ι → Ω → β}
{τ : Ω → WithTop ι}
[Zero β]
{s : Set Ω}
(i : ι)
:
theorem
MeasureTheory.stoppedProcess_indicator_comm'
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[Nonempty ι]
[LinearOrder ι]
{u : ι → Ω → β}
{τ : Ω → WithTop ι}
[Zero β]
{s : Set Ω}
:
stoppedProcess (fun (i : ι) => s.indicator (u i)) τ = fun (i : ι) => s.indicator (stoppedProcess u τ i)
@[simp]
theorem
MeasureTheory.stoppedProcess_stoppedProcess
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[Nonempty ι]
[LinearOrder ι]
{u : ι → Ω → β}
{τ σ : Ω → WithTop ι}
:
theorem
MeasureTheory.stoppedProcess_stoppedProcess'
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[Nonempty ι]
[LinearOrder ι]
{u : ι → Ω → β}
{τ σ : Ω → WithTop ι}
:
theorem
MeasureTheory.stoppedProcess_stoppedProcess_of_le_right
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[Nonempty ι]
[LinearOrder ι]
{u : ι → Ω → β}
{τ σ : Ω → WithTop ι}
(h : σ ≤ τ)
:
theorem
MeasureTheory.stoppedProcess_stoppedProcess_of_le_left
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[Nonempty ι]
[LinearOrder ι]
{u : ι → Ω → β}
{τ σ : Ω → WithTop ι}
(h : τ ≤ σ)
:
theorem
MeasureTheory.progMeasurable_min_stopping_time
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Nonempty ι]
[LinearOrder ι]
{τ : Ω → WithTop ι}
[MeasurableSpace ι]
[TopologicalSpace ι]
[OrderTopology ι]
[SecondCountableTopology ι]
[BorelSpace ι]
{f : Filtration ι m}
[TopologicalSpace.PseudoMetrizableSpace ι]
(hτ : IsStoppingTime f τ)
:
ProgMeasurable f fun (i : ι) (ω : Ω) => (min (↑i) (τ ω)).untopA
theorem
MeasureTheory.ProgMeasurable.stoppedProcess
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Nonempty ι]
[LinearOrder ι]
{u : ι → Ω → β}
{τ : Ω → WithTop ι}
[MeasurableSpace ι]
[TopologicalSpace ι]
[OrderTopology ι]
[SecondCountableTopology ι]
[BorelSpace ι]
[TopologicalSpace β]
{f : Filtration ι m}
[TopologicalSpace.PseudoMetrizableSpace ι]
(h : ProgMeasurable f u)
(hτ : IsStoppingTime f τ)
:
theorem
MeasureTheory.ProgMeasurable.stronglyAdapted_stoppedProcess
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Nonempty ι]
[LinearOrder ι]
{u : ι → Ω → β}
{τ : Ω → WithTop ι}
[MeasurableSpace ι]
[TopologicalSpace ι]
[OrderTopology ι]
[SecondCountableTopology ι]
[BorelSpace ι]
[TopologicalSpace β]
{f : Filtration ι m}
[TopologicalSpace.PseudoMetrizableSpace ι]
(h : ProgMeasurable f u)
(hτ : IsStoppingTime f τ)
:
theorem
MeasureTheory.ProgMeasurable.stronglyMeasurable_stoppedProcess
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Nonempty ι]
[LinearOrder ι]
{u : ι → Ω → β}
{τ : Ω → WithTop ι}
[MeasurableSpace ι]
[TopologicalSpace ι]
[OrderTopology ι]
[SecondCountableTopology ι]
[BorelSpace ι]
[TopologicalSpace β]
{f : Filtration ι m}
[TopologicalSpace.PseudoMetrizableSpace ι]
(hu : ProgMeasurable f u)
(hτ : IsStoppingTime f τ)
(i : ι)
:
theorem
MeasureTheory.stronglyMeasurable_stoppedValue_of_le
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Nonempty ι]
[LinearOrder ι]
{u : ι → Ω → β}
{τ : Ω → WithTop ι}
[MeasurableSpace ι]
[TopologicalSpace ι]
[OrderTopology ι]
[SecondCountableTopology ι]
[BorelSpace ι]
[TopologicalSpace β]
{f : Filtration ι m}
(h : ProgMeasurable f u)
(hτ : IsStoppingTime f τ)
{n : ι}
(hτ_le : ∀ (ω : Ω), τ ω ≤ ↑n)
:
theorem
MeasureTheory.measurableSet_preimage_stoppedValue_inter
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Nonempty ι]
[LinearOrder ι]
{u : ι → Ω → β}
{τ : Ω → WithTop ι}
[MeasurableSpace ι]
[TopologicalSpace ι]
[OrderTopology ι]
[SecondCountableTopology ι]
[BorelSpace ι]
[TopologicalSpace β]
{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})
theorem
MeasureTheory.measurable_stoppedValue
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Nonempty ι]
[LinearOrder ι]
{u : ι → Ω → β}
{τ : Ω → WithTop ι}
[MeasurableSpace ι]
[TopologicalSpace ι]
[OrderTopology ι]
[SecondCountableTopology ι]
[BorelSpace ι]
[TopologicalSpace β]
{f : Filtration ι m}
[TopologicalSpace.PseudoMetrizableSpace β]
[MeasurableSpace β]
[BorelSpace β]
(hf_prog : ProgMeasurable f u)
(hτ : IsStoppingTime f τ)
:
Measurable (stoppedValue u τ)
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)
:
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)
:
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)
:
theorem
MeasureTheory.stoppedProcess_eq''
{Ω : Type u_1}
{ι : Type u_3}
[Nonempty ι]
{τ : Ω → WithTop ι}
{E : Type u_4}
{u : ι → Ω → E}
[LinearOrder ι]
[LocallyFiniteOrderBot ι]
[AddCommMonoid E]
(n : ι)
:
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 μ
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 μ
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 τ) μ
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 τ) μ
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 μ
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 μ
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) μ
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) μ
theorem
MeasureTheory.StronglyAdapted.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 : StronglyAdapted f u)
(hu_cont : ∀ (ω : Ω), Continuous fun (i : ι) => u i ω)
(hτ : IsStoppingTime f τ)
:
The stopped process of a strongly adapted process with continuous paths is strongly adapted.
theorem
MeasureTheory.StronglyAdapted.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 : StronglyAdapted f u)
(hτ : IsStoppingTime f τ)
:
If the indexing order has the discrete topology, then the stopped process of a strongly adapted process is strongly adapted.
theorem
MeasureTheory.StronglyAdapted.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 : StronglyAdapted f u)
(hu_cont : ∀ (ω : Ω), Continuous fun (i : ι) => u i ω)
(hτ : IsStoppingTime f τ)
(n : ι)
:
theorem
MeasureTheory.StronglyAdapted.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 : StronglyAdapted f u)
(hτ : IsStoppingTime f τ)
(n : ι)
:
Filtrations indexed by ℕ #
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)) ω
theorem
MeasureTheory.stoppedValue_sub_eq_sum'
{Ω : Type u_1}
{β : Type u_2}
{u : ℕ → Ω → β}
{τ π : Ω → ℕ∞}
[AddCommGroup β]
(hle : τ ≤ π)
{N : ℕ}
(hbdd : ∀ (ω : Ω), π ω ≤ ↑N)
:
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
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.
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)
theorem
MeasureTheory.stoppedValue_piecewise_const
{Ω : Type u_1}
{s : Set Ω}
[DecidablePred fun (x : Ω) => x ∈ s]
{ι' : Type u_4}
{α : Type u_5}
[Nonempty ι']
{i j : ι'}
{f : ι' → Ω → α}
:
theorem
MeasureTheory.stoppedValue_piecewise_const'
{Ω : Type u_1}
{s : Set Ω}
[DecidablePred fun (x : Ω) => x ∈ s]
{ι' : Type u_4}
{α : Type u_5}
[AddCommGroup α]
[Nonempty ι']
{i j : ι'}
{f : ι' → Ω → α}
:
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 : 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 : ι)
:
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 : ι)
:
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 ⋯)]
:
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 : ι)
:
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 ⋯)]
: