Stopping times, stopped processes and stopped values #
Definition and properties of stopping times.
Main definitions #
MeasureTheory.IsStoppingTime: a stopping time with respect to some filtrationfis a functionτ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.memℒp_stoppedProcess: if a process belongs toℒpat every time inℕ, then its stopped process belongs toℒpas well.
Tags #
stopping time, stochastic process
Stopping times #
def
MeasureTheory.IsStoppingTime
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
(f : MeasureTheory.Filtration ι m)
(τ : Ω → ι)
:
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 : MeasureTheory.Filtration ι m)
(i : ι)
:
MeasureTheory.IsStoppingTime f fun (x : Ω) => i
theorem
MeasureTheory.IsStoppingTime.measurableSet_le
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : MeasureTheory.Filtration ι m}
{τ : Ω → ι}
(hτ : MeasureTheory.IsStoppingTime f τ)
(i : ι)
:
MeasurableSet {ω : Ω | τ ω ≤ i}
theorem
MeasureTheory.IsStoppingTime.measurableSet_lt_of_pred
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : MeasureTheory.Filtration ι m}
{τ : Ω → ι}
[PredOrder ι]
(hτ : MeasureTheory.IsStoppingTime f τ)
(i : ι)
:
MeasurableSet {ω : Ω | τ ω < i}
theorem
MeasureTheory.IsStoppingTime.measurableSet_eq_of_countable_range
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[PartialOrder ι]
{τ : Ω → ι}
{f : MeasureTheory.Filtration ι m}
(hτ : MeasureTheory.IsStoppingTime f τ)
(h_countable : (Set.range τ).Countable)
(i : ι)
:
MeasurableSet {ω : Ω | τ ω = i}
theorem
MeasureTheory.IsStoppingTime.measurableSet_eq_of_countable
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[PartialOrder ι]
{τ : Ω → ι}
{f : MeasureTheory.Filtration ι m}
[Countable ι]
(hτ : MeasureTheory.IsStoppingTime f τ)
(i : ι)
:
MeasurableSet {ω : Ω | τ ω = i}
theorem
MeasureTheory.IsStoppingTime.measurableSet_lt_of_countable_range
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[PartialOrder ι]
{τ : Ω → ι}
{f : MeasureTheory.Filtration ι m}
(hτ : MeasureTheory.IsStoppingTime f τ)
(h_countable : (Set.range τ).Countable)
(i : ι)
:
MeasurableSet {ω : Ω | τ ω < i}
theorem
MeasureTheory.IsStoppingTime.measurableSet_lt_of_countable
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[PartialOrder ι]
{τ : Ω → ι}
{f : MeasureTheory.Filtration ι m}
[Countable ι]
(hτ : MeasureTheory.IsStoppingTime f τ)
(i : ι)
:
MeasurableSet {ω : Ω | τ ω < i}
theorem
MeasureTheory.IsStoppingTime.measurableSet_ge_of_countable_range
{Ω : Type u_1}
{m : MeasurableSpace Ω}
{ι : Type u_4}
[LinearOrder ι]
{τ : Ω → ι}
{f : MeasureTheory.Filtration ι m}
(hτ : MeasureTheory.IsStoppingTime f τ)
(h_countable : (Set.range τ).Countable)
(i : ι)
:
MeasurableSet {ω : Ω | i ≤ τ ω}
theorem
MeasureTheory.IsStoppingTime.measurableSet_ge_of_countable
{Ω : Type u_1}
{m : MeasurableSpace Ω}
{ι : Type u_4}
[LinearOrder ι]
{τ : Ω → ι}
{f : MeasureTheory.Filtration ι m}
[Countable ι]
(hτ : MeasureTheory.IsStoppingTime f τ)
(i : ι)
:
MeasurableSet {ω : Ω | i ≤ τ ω}
theorem
MeasureTheory.IsStoppingTime.measurableSet_gt
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[LinearOrder ι]
{f : MeasureTheory.Filtration ι m}
{τ : Ω → ι}
(hτ : MeasureTheory.IsStoppingTime f τ)
(i : ι)
:
MeasurableSet {ω : Ω | i < τ ω}
theorem
MeasureTheory.IsStoppingTime.measurableSet_lt_of_isLUB
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[LinearOrder ι]
{f : MeasureTheory.Filtration ι m}
{τ : Ω → ι}
[TopologicalSpace ι]
[OrderTopology ι]
[FirstCountableTopology ι]
(hτ : MeasureTheory.IsStoppingTime f τ)
(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 : MeasurableSpace Ω}
[LinearOrder ι]
{f : MeasureTheory.Filtration ι m}
{τ : Ω → ι}
[TopologicalSpace ι]
[OrderTopology ι]
[FirstCountableTopology ι]
(hτ : MeasureTheory.IsStoppingTime f τ)
(i : ι)
:
MeasurableSet {ω : Ω | τ ω < i}
theorem
MeasureTheory.IsStoppingTime.measurableSet_ge
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[LinearOrder ι]
{f : MeasureTheory.Filtration ι m}
{τ : Ω → ι}
[TopologicalSpace ι]
[OrderTopology ι]
[FirstCountableTopology ι]
(hτ : MeasureTheory.IsStoppingTime f τ)
(i : ι)
:
MeasurableSet {ω : Ω | i ≤ τ ω}
theorem
MeasureTheory.IsStoppingTime.measurableSet_eq
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[LinearOrder ι]
{f : MeasureTheory.Filtration ι m}
{τ : Ω → ι}
[TopologicalSpace ι]
[OrderTopology ι]
[FirstCountableTopology ι]
(hτ : MeasureTheory.IsStoppingTime f τ)
(i : ι)
:
MeasurableSet {ω : Ω | τ ω = i}
theorem
MeasureTheory.IsStoppingTime.measurableSet_eq_le
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[LinearOrder ι]
{f : MeasureTheory.Filtration ι m}
{τ : Ω → ι}
[TopologicalSpace ι]
[OrderTopology ι]
[FirstCountableTopology ι]
(hτ : MeasureTheory.IsStoppingTime f τ)
{i : ι}
{j : ι}
(hle : i ≤ j)
:
MeasurableSet {ω : Ω | τ ω = i}
theorem
MeasureTheory.IsStoppingTime.measurableSet_lt_le
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[LinearOrder ι]
{f : MeasureTheory.Filtration ι m}
{τ : Ω → ι}
[TopologicalSpace ι]
[OrderTopology ι]
[FirstCountableTopology ι]
(hτ : MeasureTheory.IsStoppingTime f τ)
{i : ι}
{j : ι}
(hle : i ≤ j)
:
MeasurableSet {ω : Ω | τ ω < i}
theorem
MeasureTheory.isStoppingTime_of_measurableSet_eq
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
[Countable ι]
{f : MeasureTheory.Filtration ι m}
{τ : Ω → ι}
(hτ : ∀ (i : ι), MeasurableSet {ω : Ω | τ ω = i})
:
theorem
MeasureTheory.IsStoppingTime.max
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[LinearOrder ι]
{f : MeasureTheory.Filtration ι m}
{τ : Ω → ι}
{π : Ω → ι}
(hτ : MeasureTheory.IsStoppingTime f τ)
(hπ : MeasureTheory.IsStoppingTime f π)
:
MeasureTheory.IsStoppingTime f fun (ω : Ω) => max (τ ω) (π ω)
theorem
MeasureTheory.IsStoppingTime.max_const
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[LinearOrder ι]
{f : MeasureTheory.Filtration ι m}
{τ : Ω → ι}
(hτ : MeasureTheory.IsStoppingTime f τ)
(i : ι)
:
MeasureTheory.IsStoppingTime f fun (ω : Ω) => max (τ ω) i
theorem
MeasureTheory.IsStoppingTime.min
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[LinearOrder ι]
{f : MeasureTheory.Filtration ι m}
{τ : Ω → ι}
{π : Ω → ι}
(hτ : MeasureTheory.IsStoppingTime f τ)
(hπ : MeasureTheory.IsStoppingTime f π)
:
MeasureTheory.IsStoppingTime f fun (ω : Ω) => min (τ ω) (π ω)
theorem
MeasureTheory.IsStoppingTime.min_const
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[LinearOrder ι]
{f : MeasureTheory.Filtration ι m}
{τ : Ω → ι}
(hτ : MeasureTheory.IsStoppingTime f τ)
(i : ι)
:
MeasureTheory.IsStoppingTime f fun (ω : Ω) => min (τ ω) i
theorem
MeasureTheory.IsStoppingTime.add_const
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[AddGroup ι]
[Preorder ι]
[CovariantClass ι ι (Function.swap fun (x x_1 : ι) => x + x_1) fun (x x_1 : ι) => x ≤ x_1]
[CovariantClass ι ι (fun (x x_1 : ι) => x + x_1) fun (x x_1 : ι) => x ≤ x_1]
{f : MeasureTheory.Filtration ι m}
{τ : Ω → ι}
(hτ : MeasureTheory.IsStoppingTime f τ)
{i : ι}
(hi : 0 ≤ i)
:
MeasureTheory.IsStoppingTime f fun (ω : Ω) => τ ω + i
theorem
MeasureTheory.IsStoppingTime.add_const_nat
{Ω : Type u_1}
{m : MeasurableSpace Ω}
{f : MeasureTheory.Filtration ℕ m}
{τ : Ω → ℕ}
(hτ : MeasureTheory.IsStoppingTime f τ)
{i : ℕ}
:
MeasureTheory.IsStoppingTime f fun (ω : Ω) => τ ω + i
theorem
MeasureTheory.IsStoppingTime.add
{Ω : Type u_1}
{m : MeasurableSpace Ω}
{f : MeasureTheory.Filtration ℕ m}
{τ : Ω → ℕ}
{π : Ω → ℕ}
(hτ : MeasureTheory.IsStoppingTime f τ)
(hπ : MeasureTheory.IsStoppingTime f π)
:
MeasureTheory.IsStoppingTime f (τ + π)
def
MeasureTheory.IsStoppingTime.measurableSpace
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : MeasureTheory.Filtration ι m}
{τ : Ω → ι}
(hτ : MeasureTheory.IsStoppingTime f τ)
:
The associated σ-algebra with a stopping time.
Equations
- hτ.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 : MeasurableSpace Ω}
[Preorder ι]
{f : MeasureTheory.Filtration ι m}
{τ : Ω → ι}
(hτ : MeasureTheory.IsStoppingTime f τ)
(s : Set Ω)
:
MeasurableSet s ↔ ∀ (i : ι), MeasurableSet (s ∩ {ω : Ω | τ ω ≤ i})
theorem
MeasureTheory.IsStoppingTime.measurableSpace_mono
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : MeasureTheory.Filtration ι m}
{τ : Ω → ι}
{π : Ω → ι}
(hτ : MeasureTheory.IsStoppingTime f τ)
(hπ : MeasureTheory.IsStoppingTime f π)
(hle : τ ≤ π)
:
hτ.measurableSpace ≤ hπ.measurableSpace
theorem
MeasureTheory.IsStoppingTime.measurableSpace_le_of_countable
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : MeasureTheory.Filtration ι m}
{τ : Ω → ι}
[Countable ι]
(hτ : MeasureTheory.IsStoppingTime f τ)
:
hτ.measurableSpace ≤ m
theorem
MeasureTheory.IsStoppingTime.measurableSpace_le'
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : MeasureTheory.Filtration ι m}
{τ : Ω → ι}
[Filter.atTop.IsCountablyGenerated]
[Filter.atTop.NeBot]
(hτ : MeasureTheory.IsStoppingTime f τ)
:
hτ.measurableSpace ≤ m
theorem
MeasureTheory.IsStoppingTime.measurableSpace_le
{Ω : Type u_1}
{m : MeasurableSpace Ω}
{ι : Type u_4}
[SemilatticeSup ι]
{f : MeasureTheory.Filtration ι m}
{τ : Ω → ι}
[Filter.atTop.IsCountablyGenerated]
(hτ : MeasureTheory.IsStoppingTime f τ)
:
hτ.measurableSpace ≤ m
@[simp]
theorem
MeasureTheory.IsStoppingTime.measurableSpace_const
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
(f : MeasureTheory.Filtration ι m)
(i : ι)
:
⋯.measurableSpace = ↑f i
theorem
MeasureTheory.IsStoppingTime.measurableSet_inter_eq_iff
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : MeasureTheory.Filtration ι m}
{τ : Ω → ι}
(hτ : MeasureTheory.IsStoppingTime f τ)
(s : Set Ω)
(i : ι)
:
MeasurableSet (s ∩ {ω : Ω | τ ω = i}) ↔ MeasurableSet (s ∩ {ω : Ω | τ ω = i})
theorem
MeasureTheory.IsStoppingTime.measurableSpace_le_of_le_const
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : MeasureTheory.Filtration ι m}
{τ : Ω → ι}
(hτ : MeasureTheory.IsStoppingTime f τ)
{i : ι}
(hτ_le : ∀ (ω : Ω), τ ω ≤ i)
:
hτ.measurableSpace ≤ ↑f i
theorem
MeasureTheory.IsStoppingTime.measurableSpace_le_of_le
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : MeasureTheory.Filtration ι m}
{τ : Ω → ι}
(hτ : MeasureTheory.IsStoppingTime f τ)
{n : ι}
(hτ_le : ∀ (ω : Ω), τ ω ≤ n)
:
hτ.measurableSpace ≤ m
theorem
MeasureTheory.IsStoppingTime.le_measurableSpace_of_const_le
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : MeasureTheory.Filtration ι m}
{τ : Ω → ι}
(hτ : MeasureTheory.IsStoppingTime f τ)
{i : ι}
(hτ_le : ∀ (ω : Ω), i ≤ τ ω)
:
↑f i ≤ hτ.measurableSpace
instance
MeasureTheory.IsStoppingTime.sigmaFinite_stopping_time
{Ω : Type u_1}
{m : MeasurableSpace Ω}
{ι : Type u_4}
[SemilatticeSup ι]
[OrderBot ι]
[Filter.atTop.IsCountablyGenerated]
{μ : MeasureTheory.Measure Ω}
{f : MeasureTheory.Filtration ι m}
{τ : Ω → ι}
[MeasureTheory.SigmaFiniteFiltration μ f]
(hτ : MeasureTheory.IsStoppingTime f τ)
:
MeasureTheory.SigmaFinite (μ.trim ⋯)
Equations
- ⋯ = ⋯
instance
MeasureTheory.IsStoppingTime.sigmaFinite_stopping_time_of_le
{Ω : Type u_1}
{m : MeasurableSpace Ω}
{ι : Type u_4}
[SemilatticeSup ι]
[OrderBot ι]
{μ : MeasureTheory.Measure Ω}
{f : MeasureTheory.Filtration ι m}
{τ : Ω → ι}
[MeasureTheory.SigmaFiniteFiltration μ f]
(hτ : MeasureTheory.IsStoppingTime f τ)
{n : ι}
(hτ_le : ∀ (ω : Ω), τ ω ≤ n)
:
MeasureTheory.SigmaFinite (μ.trim ⋯)
Equations
- ⋯ = ⋯
theorem
MeasureTheory.IsStoppingTime.measurableSet_le'
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[LinearOrder ι]
{f : MeasureTheory.Filtration ι m}
{τ : Ω → ι}
(hτ : MeasureTheory.IsStoppingTime f τ)
(i : ι)
:
MeasurableSet {ω : Ω | τ ω ≤ i}
theorem
MeasureTheory.IsStoppingTime.measurableSet_gt'
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[LinearOrder ι]
{f : MeasureTheory.Filtration ι m}
{τ : Ω → ι}
(hτ : MeasureTheory.IsStoppingTime f τ)
(i : ι)
:
MeasurableSet {ω : Ω | i < τ ω}
theorem
MeasureTheory.IsStoppingTime.measurableSet_eq'
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[LinearOrder ι]
{f : MeasureTheory.Filtration ι m}
{τ : Ω → ι}
[TopologicalSpace ι]
[OrderTopology ι]
[FirstCountableTopology ι]
(hτ : MeasureTheory.IsStoppingTime f τ)
(i : ι)
:
MeasurableSet {ω : Ω | τ ω = i}
theorem
MeasureTheory.IsStoppingTime.measurableSet_ge'
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[LinearOrder ι]
{f : MeasureTheory.Filtration ι m}
{τ : Ω → ι}
[TopologicalSpace ι]
[OrderTopology ι]
[FirstCountableTopology ι]
(hτ : MeasureTheory.IsStoppingTime f τ)
(i : ι)
:
MeasurableSet {ω : Ω | i ≤ τ ω}
theorem
MeasureTheory.IsStoppingTime.measurableSet_lt'
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[LinearOrder ι]
{f : MeasureTheory.Filtration ι m}
{τ : Ω → ι}
[TopologicalSpace ι]
[OrderTopology ι]
[FirstCountableTopology ι]
(hτ : MeasureTheory.IsStoppingTime f τ)
(i : ι)
:
MeasurableSet {ω : Ω | τ ω < i}
theorem
MeasureTheory.IsStoppingTime.measurableSet_eq_of_countable_range'
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[LinearOrder ι]
{f : MeasureTheory.Filtration ι m}
{τ : Ω → ι}
(hτ : MeasureTheory.IsStoppingTime f τ)
(h_countable : (Set.range τ).Countable)
(i : ι)
:
MeasurableSet {ω : Ω | τ ω = i}
theorem
MeasureTheory.IsStoppingTime.measurableSet_eq_of_countable'
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[LinearOrder ι]
{f : MeasureTheory.Filtration ι m}
{τ : Ω → ι}
[Countable ι]
(hτ : MeasureTheory.IsStoppingTime f τ)
(i : ι)
:
MeasurableSet {ω : Ω | τ ω = i}
theorem
MeasureTheory.IsStoppingTime.measurableSet_ge_of_countable_range'
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[LinearOrder ι]
{f : MeasureTheory.Filtration ι m}
{τ : Ω → ι}
(hτ : MeasureTheory.IsStoppingTime f τ)
(h_countable : (Set.range τ).Countable)
(i : ι)
:
MeasurableSet {ω : Ω | i ≤ τ ω}
theorem
MeasureTheory.IsStoppingTime.measurableSet_ge_of_countable'
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[LinearOrder ι]
{f : MeasureTheory.Filtration ι m}
{τ : Ω → ι}
[Countable ι]
(hτ : MeasureTheory.IsStoppingTime f τ)
(i : ι)
:
MeasurableSet {ω : Ω | i ≤ τ ω}
theorem
MeasureTheory.IsStoppingTime.measurableSet_lt_of_countable_range'
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[LinearOrder ι]
{f : MeasureTheory.Filtration ι m}
{τ : Ω → ι}
(hτ : MeasureTheory.IsStoppingTime f τ)
(h_countable : (Set.range τ).Countable)
(i : ι)
:
MeasurableSet {ω : Ω | τ ω < i}
theorem
MeasureTheory.IsStoppingTime.measurableSet_lt_of_countable'
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[LinearOrder ι]
{f : MeasureTheory.Filtration ι m}
{τ : Ω → ι}
[Countable ι]
(hτ : MeasureTheory.IsStoppingTime f τ)
(i : ι)
:
MeasurableSet {ω : Ω | τ ω < i}
theorem
MeasureTheory.IsStoppingTime.measurableSpace_le_of_countable_range
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[LinearOrder ι]
{f : MeasureTheory.Filtration ι m}
{τ : Ω → ι}
(hτ : MeasureTheory.IsStoppingTime f τ)
(h_countable : (Set.range τ).Countable)
:
hτ.measurableSpace ≤ m
theorem
MeasureTheory.IsStoppingTime.measurable
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[LinearOrder ι]
{f : MeasureTheory.Filtration ι m}
{τ : Ω → ι}
[TopologicalSpace ι]
[MeasurableSpace ι]
[BorelSpace ι]
[OrderTopology ι]
[SecondCountableTopology ι]
(hτ : MeasureTheory.IsStoppingTime f τ)
:
theorem
MeasureTheory.IsStoppingTime.measurable_of_le
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[LinearOrder ι]
{f : MeasureTheory.Filtration ι m}
{τ : Ω → ι}
[TopologicalSpace ι]
[MeasurableSpace ι]
[BorelSpace ι]
[OrderTopology ι]
[SecondCountableTopology ι]
(hτ : MeasureTheory.IsStoppingTime f τ)
{i : ι}
(hτ_le : ∀ (ω : Ω), τ ω ≤ i)
:
theorem
MeasureTheory.IsStoppingTime.measurableSpace_min
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[LinearOrder ι]
{f : MeasureTheory.Filtration ι m}
{τ : Ω → ι}
{π : Ω → ι}
(hτ : MeasureTheory.IsStoppingTime f τ)
(hπ : MeasureTheory.IsStoppingTime f π)
:
theorem
MeasureTheory.IsStoppingTime.measurableSet_min_iff
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[LinearOrder ι]
{f : MeasureTheory.Filtration ι m}
{τ : Ω → ι}
{π : Ω → ι}
(hτ : MeasureTheory.IsStoppingTime f τ)
(hπ : MeasureTheory.IsStoppingTime f π)
(s : Set Ω)
:
theorem
MeasureTheory.IsStoppingTime.measurableSpace_min_const
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[LinearOrder ι]
{f : MeasureTheory.Filtration ι m}
{τ : Ω → ι}
(hτ : MeasureTheory.IsStoppingTime f τ)
{i : ι}
:
theorem
MeasureTheory.IsStoppingTime.measurableSet_min_const_iff
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[LinearOrder ι]
{f : MeasureTheory.Filtration ι m}
{τ : Ω → ι}
(hτ : MeasureTheory.IsStoppingTime f τ)
(s : Set Ω)
{i : ι}
:
theorem
MeasureTheory.IsStoppingTime.measurableSet_inter_le
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[LinearOrder ι]
{f : MeasureTheory.Filtration ι m}
{τ : Ω → ι}
{π : Ω → ι}
[TopologicalSpace ι]
[SecondCountableTopology ι]
[OrderTopology ι]
[MeasurableSpace ι]
[BorelSpace ι]
(hτ : MeasureTheory.IsStoppingTime f τ)
(hπ : MeasureTheory.IsStoppingTime f π)
(s : Set Ω)
(hs : MeasurableSet s)
:
MeasurableSet (s ∩ {ω : Ω | τ ω ≤ π ω})
theorem
MeasureTheory.IsStoppingTime.measurableSet_inter_le_iff
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[LinearOrder ι]
{f : MeasureTheory.Filtration ι m}
{τ : Ω → ι}
{π : Ω → ι}
[TopologicalSpace ι]
[SecondCountableTopology ι]
[OrderTopology ι]
[MeasurableSpace ι]
[BorelSpace ι]
(hτ : MeasureTheory.IsStoppingTime f τ)
(hπ : MeasureTheory.IsStoppingTime f π)
(s : Set Ω)
:
MeasurableSet (s ∩ {ω : Ω | τ ω ≤ π ω}) ↔ MeasurableSet (s ∩ {ω : Ω | τ ω ≤ π ω})
theorem
MeasureTheory.IsStoppingTime.measurableSet_inter_le_const_iff
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[LinearOrder ι]
{f : MeasureTheory.Filtration ι m}
{τ : Ω → ι}
(hτ : MeasureTheory.IsStoppingTime f τ)
(s : Set Ω)
(i : ι)
:
MeasurableSet (s ∩ {ω : Ω | τ ω ≤ i}) ↔ MeasurableSet (s ∩ {ω : Ω | τ ω ≤ i})
theorem
MeasureTheory.IsStoppingTime.measurableSet_le_stopping_time
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[LinearOrder ι]
{f : MeasureTheory.Filtration ι m}
{τ : Ω → ι}
{π : Ω → ι}
[TopologicalSpace ι]
[SecondCountableTopology ι]
[OrderTopology ι]
[MeasurableSpace ι]
[BorelSpace ι]
(hτ : MeasureTheory.IsStoppingTime f τ)
(hπ : MeasureTheory.IsStoppingTime f π)
:
MeasurableSet {ω : Ω | τ ω ≤ π ω}
theorem
MeasureTheory.IsStoppingTime.measurableSet_stopping_time_le
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[LinearOrder ι]
{f : MeasureTheory.Filtration ι m}
{τ : Ω → ι}
{π : Ω → ι}
[TopologicalSpace ι]
[SecondCountableTopology ι]
[OrderTopology ι]
[MeasurableSpace ι]
[BorelSpace ι]
(hτ : MeasureTheory.IsStoppingTime f τ)
(hπ : MeasureTheory.IsStoppingTime f π)
:
MeasurableSet {ω : Ω | τ ω ≤ π ω}
theorem
MeasureTheory.IsStoppingTime.measurableSet_eq_stopping_time
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[LinearOrder ι]
{f : MeasureTheory.Filtration ι m}
{τ : Ω → ι}
{π : Ω → ι}
[AddGroup ι]
[TopologicalSpace ι]
[MeasurableSpace ι]
[BorelSpace ι]
[OrderTopology ι]
[MeasurableSingletonClass ι]
[SecondCountableTopology ι]
[MeasurableSub₂ ι]
(hτ : MeasureTheory.IsStoppingTime f τ)
(hπ : MeasureTheory.IsStoppingTime f π)
:
MeasurableSet {ω : Ω | τ ω = π ω}
theorem
MeasureTheory.IsStoppingTime.measurableSet_eq_stopping_time_of_countable
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[LinearOrder ι]
{f : MeasureTheory.Filtration ι m}
{τ : Ω → ι}
{π : Ω → ι}
[Countable ι]
[TopologicalSpace ι]
[MeasurableSpace ι]
[BorelSpace ι]
[OrderTopology ι]
[MeasurableSingletonClass ι]
[SecondCountableTopology ι]
(hτ : MeasureTheory.IsStoppingTime f τ)
(hπ : MeasureTheory.IsStoppingTime f π)
:
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
- MeasureTheory.stoppedValue u τ ω = 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}
[LinearOrder ι]
(u : ι → Ω → β)
(τ : Ω → ι)
:
ι → Ω → β
Given a map u : ι → Ω → E, the stopped process with respect to τ is u i ω if
i ≤ τ ω, and u (τ ω) ω otherwise.
Intuitively, the stopped process stops evolving once the stopping time has occured.
Equations
- MeasureTheory.stoppedProcess u τ i ω = u (min i (τ ω)) ω
Instances For
theorem
MeasureTheory.stoppedProcess_eq_stoppedValue
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[LinearOrder ι]
{u : ι → Ω → β}
{τ : Ω → ι}
:
MeasureTheory.stoppedProcess u τ = fun (i : ι) => MeasureTheory.stoppedValue u fun (ω : Ω) => min i (τ ω)
theorem
MeasureTheory.stoppedValue_stoppedProcess
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[LinearOrder ι]
{u : ι → Ω → β}
{τ : Ω → ι}
{σ : Ω → ι}
:
MeasureTheory.stoppedValue (MeasureTheory.stoppedProcess u τ) σ = MeasureTheory.stoppedValue u fun (ω : Ω) => min (σ ω) (τ ω)
theorem
MeasureTheory.stoppedProcess_eq_of_le
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[LinearOrder ι]
{u : ι → Ω → β}
{τ : Ω → ι}
{i : ι}
{ω : Ω}
(h : i ≤ τ ω)
:
MeasureTheory.stoppedProcess u τ i ω = u i ω
theorem
MeasureTheory.stoppedProcess_eq_of_ge
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[LinearOrder ι]
{u : ι → Ω → β}
{τ : Ω → ι}
{i : ι}
{ω : Ω}
(h : τ ω ≤ i)
:
MeasureTheory.stoppedProcess u τ i ω = u (τ ω) ω
theorem
MeasureTheory.progMeasurable_min_stopping_time
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[LinearOrder ι]
[MeasurableSpace ι]
[TopologicalSpace ι]
[OrderTopology ι]
[SecondCountableTopology ι]
[BorelSpace ι]
{τ : Ω → ι}
{f : MeasureTheory.Filtration ι m}
[TopologicalSpace.MetrizableSpace ι]
(hτ : MeasureTheory.IsStoppingTime f τ)
:
MeasureTheory.ProgMeasurable f fun (i : ι) (ω : Ω) => min i (τ ω)
theorem
MeasureTheory.ProgMeasurable.stoppedProcess
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[LinearOrder ι]
[MeasurableSpace ι]
[TopologicalSpace ι]
[OrderTopology ι]
[SecondCountableTopology ι]
[BorelSpace ι]
[TopologicalSpace β]
{u : ι → Ω → β}
{τ : Ω → ι}
{f : MeasureTheory.Filtration ι m}
[TopologicalSpace.MetrizableSpace ι]
(h : MeasureTheory.ProgMeasurable f u)
(hτ : MeasureTheory.IsStoppingTime f τ)
:
theorem
MeasureTheory.ProgMeasurable.adapted_stoppedProcess
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[LinearOrder ι]
[MeasurableSpace ι]
[TopologicalSpace ι]
[OrderTopology ι]
[SecondCountableTopology ι]
[BorelSpace ι]
[TopologicalSpace β]
{u : ι → Ω → β}
{τ : Ω → ι}
{f : MeasureTheory.Filtration ι m}
[TopologicalSpace.MetrizableSpace ι]
(h : MeasureTheory.ProgMeasurable f u)
(hτ : MeasureTheory.IsStoppingTime f τ)
:
theorem
MeasureTheory.ProgMeasurable.stronglyMeasurable_stoppedProcess
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[LinearOrder ι]
[MeasurableSpace ι]
[TopologicalSpace ι]
[OrderTopology ι]
[SecondCountableTopology ι]
[BorelSpace ι]
[TopologicalSpace β]
{u : ι → Ω → β}
{τ : Ω → ι}
{f : MeasureTheory.Filtration ι m}
[TopologicalSpace.MetrizableSpace ι]
(hu : MeasureTheory.ProgMeasurable f u)
(hτ : MeasureTheory.IsStoppingTime f τ)
(i : ι)
:
theorem
MeasureTheory.stronglyMeasurable_stoppedValue_of_le
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[LinearOrder ι]
[MeasurableSpace ι]
[TopologicalSpace ι]
[OrderTopology ι]
[SecondCountableTopology ι]
[BorelSpace ι]
[TopologicalSpace β]
{u : ι → Ω → β}
{τ : Ω → ι}
{f : MeasureTheory.Filtration ι m}
(h : MeasureTheory.ProgMeasurable f u)
(hτ : MeasureTheory.IsStoppingTime f τ)
{n : ι}
(hτ_le : ∀ (ω : Ω), τ ω ≤ n)
:
theorem
MeasureTheory.measurable_stoppedValue
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[LinearOrder ι]
[MeasurableSpace ι]
[TopologicalSpace ι]
[OrderTopology ι]
[SecondCountableTopology ι]
[BorelSpace ι]
[TopologicalSpace β]
{u : ι → Ω → β}
{τ : Ω → ι}
{f : MeasureTheory.Filtration ι m}
[TopologicalSpace.MetrizableSpace β]
[MeasurableSpace β]
[BorelSpace β]
(hf_prog : MeasureTheory.ProgMeasurable f u)
(hτ : MeasureTheory.IsStoppingTime f τ)
:
theorem
MeasureTheory.stoppedValue_eq_of_mem_finset
{Ω : Type u_1}
{ι : Type u_3}
{τ : Ω → ι}
{E : Type u_4}
{u : ι → Ω → E}
[AddCommMonoid E]
{s : Finset ι}
(hbdd : ∀ (ω : Ω), τ ω ∈ s)
:
MeasureTheory.stoppedValue u τ = s.sum fun (i : ι) => {ω : Ω | τ ω = i}.indicator (u i)
theorem
MeasureTheory.stoppedValue_eq'
{Ω : Type u_1}
{ι : Type u_3}
{τ : Ω → ι}
{E : Type u_4}
{u : ι → Ω → E}
[Preorder ι]
[LocallyFiniteOrderBot ι]
[AddCommMonoid E]
{N : ι}
(hbdd : ∀ (ω : Ω), τ ω ≤ N)
:
MeasureTheory.stoppedValue u τ = (Finset.Iic N).sum fun (i : ι) => {ω : Ω | τ ω = i}.indicator (u i)
theorem
MeasureTheory.stoppedProcess_eq_of_mem_finset
{Ω : Type u_1}
{ι : Type u_3}
{τ : Ω → ι}
{E : Type u_4}
{u : ι → Ω → E}
[LinearOrder ι]
[AddCommMonoid E]
{s : Finset ι}
(n : ι)
(hbdd : ∀ (ω : Ω), τ ω < n → τ ω ∈ s)
:
MeasureTheory.stoppedProcess u τ n = {a : Ω | n ≤ τ a}.indicator (u n) + (Finset.filter (fun (x : ι) => x < n) s).sum fun (i : ι) => {ω : Ω | τ ω = i}.indicator (u i)
theorem
MeasureTheory.stoppedProcess_eq''
{Ω : Type u_1}
{ι : Type u_3}
{τ : Ω → ι}
{E : Type u_4}
{u : ι → Ω → E}
[LinearOrder ι]
[LocallyFiniteOrderBot ι]
[AddCommMonoid E]
(n : ι)
:
MeasureTheory.stoppedProcess u τ n = {a : Ω | n ≤ τ a}.indicator (u n) + (Finset.Iio n).sum fun (i : ι) => {ω : Ω | τ ω = i}.indicator (u i)
theorem
MeasureTheory.memℒp_stoppedValue_of_mem_finset
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{τ : Ω → ι}
{E : Type u_4}
{p : ENNReal}
{u : ι → Ω → E}
[PartialOrder ι]
{ℱ : MeasureTheory.Filtration ι m}
[NormedAddCommGroup E]
(hτ : MeasureTheory.IsStoppingTime ℱ τ)
(hu : ∀ (n : ι), MeasureTheory.Memℒp (u n) p μ)
{s : Finset ι}
(hbdd : ∀ (ω : Ω), τ ω ∈ s)
:
theorem
MeasureTheory.memℒp_stoppedValue
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{τ : Ω → ι}
{E : Type u_4}
{p : ENNReal}
{u : ι → Ω → E}
[PartialOrder ι]
{ℱ : MeasureTheory.Filtration ι m}
[NormedAddCommGroup E]
[LocallyFiniteOrderBot ι]
(hτ : MeasureTheory.IsStoppingTime ℱ τ)
(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 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{τ : Ω → ι}
{E : Type u_4}
{u : ι → Ω → E}
[PartialOrder ι]
{ℱ : MeasureTheory.Filtration ι m}
[NormedAddCommGroup E]
(hτ : MeasureTheory.IsStoppingTime ℱ τ)
(hu : ∀ (n : ι), MeasureTheory.Integrable (u n) μ)
{s : Finset ι}
(hbdd : ∀ (ω : Ω), τ ω ∈ s)
:
theorem
MeasureTheory.integrable_stoppedValue
{Ω : Type u_1}
(ι : Type u_3)
{m : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{τ : Ω → ι}
{E : Type u_4}
{u : ι → Ω → E}
[PartialOrder ι]
{ℱ : MeasureTheory.Filtration ι m}
[NormedAddCommGroup E]
[LocallyFiniteOrderBot ι]
(hτ : MeasureTheory.IsStoppingTime ℱ τ)
(hu : ∀ (n : ι), MeasureTheory.Integrable (u n) μ)
{N : ι}
(hbdd : ∀ (ω : Ω), τ ω ≤ N)
:
theorem
MeasureTheory.memℒp_stoppedProcess_of_mem_finset
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{τ : Ω → ι}
{E : Type u_4}
{p : ENNReal}
{u : ι → Ω → E}
[LinearOrder ι]
[TopologicalSpace ι]
[OrderTopology ι]
[FirstCountableTopology ι]
{ℱ : MeasureTheory.Filtration ι m}
[NormedAddCommGroup E]
(hτ : MeasureTheory.IsStoppingTime ℱ τ)
(hu : ∀ (n : ι), MeasureTheory.Memℒp (u n) p μ)
(n : ι)
{s : Finset ι}
(hbdd : ∀ (ω : Ω), τ ω < n → τ ω ∈ s)
:
MeasureTheory.Memℒp (MeasureTheory.stoppedProcess u τ n) p μ
theorem
MeasureTheory.memℒp_stoppedProcess
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{τ : Ω → ι}
{E : Type u_4}
{p : ENNReal}
{u : ι → Ω → E}
[LinearOrder ι]
[TopologicalSpace ι]
[OrderTopology ι]
[FirstCountableTopology ι]
{ℱ : MeasureTheory.Filtration ι m}
[NormedAddCommGroup E]
[LocallyFiniteOrderBot ι]
(hτ : MeasureTheory.IsStoppingTime ℱ τ)
(hu : ∀ (n : ι), MeasureTheory.Memℒp (u n) p μ)
(n : ι)
:
MeasureTheory.Memℒp (MeasureTheory.stoppedProcess u τ n) p μ
theorem
MeasureTheory.integrable_stoppedProcess_of_mem_finset
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{τ : Ω → ι}
{E : Type u_4}
{u : ι → Ω → E}
[LinearOrder ι]
[TopologicalSpace ι]
[OrderTopology ι]
[FirstCountableTopology ι]
{ℱ : MeasureTheory.Filtration ι m}
[NormedAddCommGroup E]
(hτ : MeasureTheory.IsStoppingTime ℱ τ)
(hu : ∀ (n : ι), MeasureTheory.Integrable (u n) μ)
(n : ι)
{s : Finset ι}
(hbdd : ∀ (ω : Ω), τ ω < n → τ ω ∈ s)
:
theorem
MeasureTheory.integrable_stoppedProcess
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{τ : Ω → ι}
{E : Type u_4}
{u : ι → Ω → E}
[LinearOrder ι]
[TopologicalSpace ι]
[OrderTopology ι]
[FirstCountableTopology ι]
{ℱ : MeasureTheory.Filtration ι m}
[NormedAddCommGroup E]
[LocallyFiniteOrderBot ι]
(hτ : MeasureTheory.IsStoppingTime ℱ τ)
(hu : ∀ (n : ι), MeasureTheory.Integrable (u n) μ)
(n : ι)
:
theorem
MeasureTheory.Adapted.stoppedProcess
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[TopologicalSpace β]
[TopologicalSpace.PseudoMetrizableSpace β]
[LinearOrder ι]
[TopologicalSpace ι]
[SecondCountableTopology ι]
[OrderTopology ι]
[MeasurableSpace ι]
[BorelSpace ι]
{f : MeasureTheory.Filtration ι m}
{u : ι → Ω → β}
{τ : Ω → ι}
[TopologicalSpace.MetrizableSpace ι]
(hu : MeasureTheory.Adapted f u)
(hu_cont : ∀ (ω : Ω), Continuous fun (i : ι) => u i ω)
(hτ : MeasureTheory.IsStoppingTime f τ)
:
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 : MeasurableSpace Ω}
[TopologicalSpace β]
[TopologicalSpace.PseudoMetrizableSpace β]
[LinearOrder ι]
[TopologicalSpace ι]
[SecondCountableTopology ι]
[OrderTopology ι]
[MeasurableSpace ι]
[BorelSpace ι]
{f : MeasureTheory.Filtration ι m}
{u : ι → Ω → β}
{τ : Ω → ι}
[DiscreteTopology ι]
(hu : MeasureTheory.Adapted f u)
(hτ : MeasureTheory.IsStoppingTime f τ)
:
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 : MeasurableSpace Ω}
[TopologicalSpace β]
[TopologicalSpace.PseudoMetrizableSpace β]
[LinearOrder ι]
[TopologicalSpace ι]
[SecondCountableTopology ι]
[OrderTopology ι]
[MeasurableSpace ι]
[BorelSpace ι]
{f : MeasureTheory.Filtration ι m}
{u : ι → Ω → β}
{τ : Ω → ι}
[TopologicalSpace.MetrizableSpace ι]
(hu : MeasureTheory.Adapted f u)
(hu_cont : ∀ (ω : Ω), Continuous fun (i : ι) => u i ω)
(hτ : MeasureTheory.IsStoppingTime f τ)
(n : ι)
:
theorem
MeasureTheory.Adapted.stronglyMeasurable_stoppedProcess_of_discrete
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[TopologicalSpace β]
[TopologicalSpace.PseudoMetrizableSpace β]
[LinearOrder ι]
[TopologicalSpace ι]
[SecondCountableTopology ι]
[OrderTopology ι]
[MeasurableSpace ι]
[BorelSpace ι]
{f : MeasureTheory.Filtration ι m}
{u : ι → Ω → β}
{τ : Ω → ι}
[DiscreteTopology ι]
(hu : MeasureTheory.Adapted f u)
(hτ : MeasureTheory.IsStoppingTime f τ)
(n : ι)
:
Filtrations indexed by ℕ #
theorem
MeasureTheory.stoppedValue_sub_eq_sum
{Ω : Type u_1}
{β : Type u_2}
{u : ℕ → Ω → β}
{τ : Ω → ℕ}
{π : Ω → ℕ}
[AddCommGroup β]
(hle : τ ≤ π)
:
MeasureTheory.stoppedValue u π - MeasureTheory.stoppedValue u τ = fun (ω : Ω) =>
(Finset.Ico (τ ω) (π ω)).sum (fun (i : ℕ) => u (i + 1) - u i) ω
theorem
MeasureTheory.stoppedValue_sub_eq_sum'
{Ω : Type u_1}
{β : Type u_2}
{u : ℕ → Ω → β}
{τ : Ω → ℕ}
{π : Ω → ℕ}
[AddCommGroup β]
(hle : τ ≤ π)
{N : ℕ}
(hbdd : ∀ (ω : Ω), π ω ≤ N)
:
MeasureTheory.stoppedValue u π - MeasureTheory.stoppedValue u τ = fun (ω : Ω) =>
(Finset.range (N + 1)).sum (fun (i : ℕ) => {ω : Ω | τ ω ≤ i ∧ i < π ω}.indicator (u (i + 1) - u i)) ω
theorem
MeasureTheory.stoppedValue_eq
{Ω : Type u_1}
{β : Type u_2}
{u : ℕ → Ω → β}
{τ : Ω → ℕ}
[AddCommMonoid β]
{N : ℕ}
(hbdd : ∀ (ω : Ω), τ ω ≤ N)
:
MeasureTheory.stoppedValue u τ = fun (x : Ω) =>
(Finset.range (N + 1)).sum (fun (i : ℕ) => {ω : Ω | τ ω = i}.indicator (u i)) x
theorem
MeasureTheory.stoppedProcess_eq
{Ω : Type u_1}
{β : Type u_2}
{u : ℕ → Ω → β}
{τ : Ω → ℕ}
[AddCommMonoid β]
(n : ℕ)
:
MeasureTheory.stoppedProcess u τ n = {a : Ω | n ≤ τ a}.indicator (u n) + (Finset.range n).sum fun (i : ℕ) => {ω : Ω | τ ω = i}.indicator (u i)
theorem
MeasureTheory.stoppedProcess_eq'
{Ω : Type u_1}
{β : Type u_2}
{u : ℕ → Ω → β}
{τ : Ω → ℕ}
[AddCommMonoid β]
(n : ℕ)
:
MeasureTheory.stoppedProcess u τ n = {a : Ω | n + 1 ≤ τ a}.indicator (u n) + (Finset.range (n + 1)).sum fun (i : ℕ) => {a : Ω | τ a = i}.indicator (u i)
theorem
MeasureTheory.IsStoppingTime.piecewise_of_le
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[Preorder ι]
{𝒢 : MeasureTheory.Filtration ι m}
{τ : Ω → ι}
{η : Ω → ι}
{i : ι}
{s : Set Ω}
[DecidablePred fun (x : Ω) => x ∈ s]
(hτ_st : MeasureTheory.IsStoppingTime 𝒢 τ)
(hη_st : MeasureTheory.IsStoppingTime 𝒢 η)
(hτ : ∀ (ω : Ω), i ≤ τ ω)
(hη : ∀ (ω : Ω), i ≤ η ω)
(hs : MeasurableSet s)
:
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 : MeasurableSpace Ω}
[Preorder ι]
{𝒢 : MeasureTheory.Filtration ι m}
{i : ι}
{j : ι}
{s : Set Ω}
[DecidablePred fun (x : Ω) => x ∈ s]
(hij : i ≤ j)
(hs : MeasurableSet s)
:
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 : MeasurableSpace Ω}
[LinearOrder ι]
{μ : MeasureTheory.Measure Ω}
{ℱ : MeasureTheory.Filtration ι m}
{τ : Ω → ι}
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{f : Ω → E}
[MeasureTheory.SigmaFiniteFiltration μ ℱ]
(hτ : MeasureTheory.IsStoppingTime ℱ τ)
(h_countable : (Set.range τ).Countable)
[MeasureTheory.SigmaFinite (μ.trim ⋯)]
(i : ι)
:
(μ.restrict {x : Ω | τ x = i}).ae.EventuallyEq (MeasureTheory.condexp hτ.measurableSpace μ f)
(MeasureTheory.condexp (↑ℱ i) μ f)
theorem
MeasureTheory.condexp_stopping_time_ae_eq_restrict_eq_of_countable
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[LinearOrder ι]
{μ : MeasureTheory.Measure Ω}
{ℱ : MeasureTheory.Filtration ι m}
{τ : Ω → ι}
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{f : Ω → E}
[Countable ι]
[MeasureTheory.SigmaFiniteFiltration μ ℱ]
(hτ : MeasureTheory.IsStoppingTime ℱ τ)
[MeasureTheory.SigmaFinite (μ.trim ⋯)]
(i : ι)
:
(μ.restrict {x : Ω | τ x = i}).ae.EventuallyEq (MeasureTheory.condexp hτ.measurableSpace μ f)
(MeasureTheory.condexp (↑ℱ i) μ f)
theorem
MeasureTheory.condexp_min_stopping_time_ae_eq_restrict_le_const
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[LinearOrder ι]
{μ : MeasureTheory.Measure Ω}
{ℱ : MeasureTheory.Filtration ι m}
{τ : Ω → ι}
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{f : Ω → E}
[Filter.atTop.IsCountablyGenerated]
(hτ : MeasureTheory.IsStoppingTime ℱ τ)
(i : ι)
[MeasureTheory.SigmaFinite (μ.trim ⋯)]
:
(μ.restrict {x : Ω | τ x ≤ i}).ae.EventuallyEq (MeasureTheory.condexp ⋯.measurableSpace μ f)
(MeasureTheory.condexp hτ.measurableSpace μ f)
theorem
MeasureTheory.condexp_stopping_time_ae_eq_restrict_eq
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[LinearOrder ι]
{μ : MeasureTheory.Measure Ω}
{ℱ : MeasureTheory.Filtration ι m}
{τ : Ω → ι}
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{f : Ω → E}
[Filter.atTop.IsCountablyGenerated]
[TopologicalSpace ι]
[OrderTopology ι]
[FirstCountableTopology ι]
[MeasureTheory.SigmaFiniteFiltration μ ℱ]
(hτ : MeasureTheory.IsStoppingTime ℱ τ)
[MeasureTheory.SigmaFinite (μ.trim ⋯)]
(i : ι)
:
(μ.restrict {x : Ω | τ x = i}).ae.EventuallyEq (MeasureTheory.condexp hτ.measurableSpace μ f)
(MeasureTheory.condexp (↑ℱ i) μ f)
theorem
MeasureTheory.condexp_min_stopping_time_ae_eq_restrict_le
{Ω : Type u_1}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[LinearOrder ι]
{μ : MeasureTheory.Measure Ω}
{ℱ : MeasureTheory.Filtration ι m}
{τ : Ω → ι}
{σ : Ω → ι}
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{f : Ω → E}
[Filter.atTop.IsCountablyGenerated]
[TopologicalSpace ι]
[OrderTopology ι]
[MeasurableSpace ι]
[SecondCountableTopology ι]
[BorelSpace ι]
(hτ : MeasureTheory.IsStoppingTime ℱ τ)
(hσ : MeasureTheory.IsStoppingTime ℱ σ)
[MeasureTheory.SigmaFinite (μ.trim ⋯)]
:
(μ.restrict {x : Ω | τ x ≤ σ x}).ae.EventuallyEq (MeasureTheory.condexp ⋯.measurableSpace μ f)
(MeasureTheory.condexp hτ.measurableSpace μ f)