Stopping times, stopped processes and stopped values #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Definition and properties of stopping times.
Main definitions #
measure_theory.is_stopping_time: a stopping time with respect to some filtrationfis a functionτsuch that for alli, the preimage of{j | j ≤ i}alongτisf i-measurablemeasure_theory.is_stopping_time.measurable_space: the σ-algebra associated with a stopping time
Main results #
prog_measurable.stopped_process: the stopped process of a progressively measurable process is progressively measurable.mem_ℒp_stopped_process: if a process belongs toℒpat every time inℕ, then its stopped process belongs toℒpas well.
Tags #
stopping time, stochastic process
Stopping times #
def
measure_theory.is_stopping_time
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
[preorder ι]
(f : measure_theory.filtration ι m)
(τ : Ω → ι) :
Prop
A stopping time with respect to some filtration f is a function
τ such that for all i, the preimage of {j | j ≤ i} along τ is measurable
with respect to f i.
Intuitively, the stopping time τ describes some stopping rule such that at time
i, we may determine it with the information we have at time i.
Equations
- measure_theory.is_stopping_time f τ = ∀ (i : ι), measurable_set {ω : Ω | τ ω ≤ i}
theorem
measure_theory.is_stopping_time_const
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
[preorder ι]
(f : measure_theory.filtration ι m)
(i : ι) :
measure_theory.is_stopping_time f (λ (ω : Ω), i)
@[protected]
theorem
measure_theory.is_stopping_time.measurable_set_le
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
[preorder ι]
{f : measure_theory.filtration ι m}
{τ : Ω → ι}
(hτ : measure_theory.is_stopping_time f τ)
(i : ι) :
measurable_set {ω : Ω | τ ω ≤ i}
theorem
measure_theory.is_stopping_time.measurable_set_lt_of_pred
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
[preorder ι]
{f : measure_theory.filtration ι m}
{τ : Ω → ι}
[pred_order ι]
(hτ : measure_theory.is_stopping_time f τ)
(i : ι) :
measurable_set {ω : Ω | τ ω < i}
@[protected]
theorem
measure_theory.is_stopping_time.measurable_set_eq_of_countable_range
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
[partial_order ι]
{τ : Ω → ι}
{f : measure_theory.filtration ι m}
(hτ : measure_theory.is_stopping_time f τ)
(h_countable : (set.range τ).countable)
(i : ι) :
measurable_set {ω : Ω | τ ω = i}
@[protected]
theorem
measure_theory.is_stopping_time.measurable_set_eq_of_countable
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
[partial_order ι]
{τ : Ω → ι}
{f : measure_theory.filtration ι m}
[countable ι]
(hτ : measure_theory.is_stopping_time f τ)
(i : ι) :
measurable_set {ω : Ω | τ ω = i}
@[protected]
theorem
measure_theory.is_stopping_time.measurable_set_lt_of_countable_range
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
[partial_order ι]
{τ : Ω → ι}
{f : measure_theory.filtration ι m}
(hτ : measure_theory.is_stopping_time f τ)
(h_countable : (set.range τ).countable)
(i : ι) :
measurable_set {ω : Ω | τ ω < i}
@[protected]
theorem
measure_theory.is_stopping_time.measurable_set_lt_of_countable
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
[partial_order ι]
{τ : Ω → ι}
{f : measure_theory.filtration ι m}
[countable ι]
(hτ : measure_theory.is_stopping_time f τ)
(i : ι) :
measurable_set {ω : Ω | τ ω < i}
@[protected]
theorem
measure_theory.is_stopping_time.measurable_set_ge_of_countable_range
{Ω : Type u_1}
{m : measurable_space Ω}
{ι : Type u_2}
[linear_order ι]
{τ : Ω → ι}
{f : measure_theory.filtration ι m}
(hτ : measure_theory.is_stopping_time f τ)
(h_countable : (set.range τ).countable)
(i : ι) :
measurable_set {ω : Ω | i ≤ τ ω}
@[protected]
theorem
measure_theory.is_stopping_time.measurable_set_ge_of_countable
{Ω : Type u_1}
{m : measurable_space Ω}
{ι : Type u_2}
[linear_order ι]
{τ : Ω → ι}
{f : measure_theory.filtration ι m}
[countable ι]
(hτ : measure_theory.is_stopping_time f τ)
(i : ι) :
measurable_set {ω : Ω | i ≤ τ ω}
theorem
measure_theory.is_stopping_time.measurable_set_gt
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
[linear_order ι]
{f : measure_theory.filtration ι m}
{τ : Ω → ι}
(hτ : measure_theory.is_stopping_time f τ)
(i : ι) :
measurable_set {ω : Ω | i < τ ω}
theorem
measure_theory.is_stopping_time.measurable_set_lt_of_is_lub
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
[linear_order ι]
{f : measure_theory.filtration ι m}
{τ : Ω → ι}
[topological_space ι]
[order_topology ι]
[topological_space.first_countable_topology ι]
(hτ : measure_theory.is_stopping_time f τ)
(i : ι)
(h_lub : is_lub (set.Iio i) i) :
measurable_set {ω : Ω | τ ω < i}
Auxiliary lemma for is_stopping_time.measurable_set_lt.
theorem
measure_theory.is_stopping_time.measurable_set_lt
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
[linear_order ι]
{f : measure_theory.filtration ι m}
{τ : Ω → ι}
[topological_space ι]
[order_topology ι]
[topological_space.first_countable_topology ι]
(hτ : measure_theory.is_stopping_time f τ)
(i : ι) :
measurable_set {ω : Ω | τ ω < i}
theorem
measure_theory.is_stopping_time.measurable_set_ge
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
[linear_order ι]
{f : measure_theory.filtration ι m}
{τ : Ω → ι}
[topological_space ι]
[order_topology ι]
[topological_space.first_countable_topology ι]
(hτ : measure_theory.is_stopping_time f τ)
(i : ι) :
measurable_set {ω : Ω | i ≤ τ ω}
theorem
measure_theory.is_stopping_time.measurable_set_eq
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
[linear_order ι]
{f : measure_theory.filtration ι m}
{τ : Ω → ι}
[topological_space ι]
[order_topology ι]
[topological_space.first_countable_topology ι]
(hτ : measure_theory.is_stopping_time f τ)
(i : ι) :
measurable_set {ω : Ω | τ ω = i}
theorem
measure_theory.is_stopping_time.measurable_set_eq_le
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
[linear_order ι]
{f : measure_theory.filtration ι m}
{τ : Ω → ι}
[topological_space ι]
[order_topology ι]
[topological_space.first_countable_topology ι]
(hτ : measure_theory.is_stopping_time f τ)
{i j : ι}
(hle : i ≤ j) :
measurable_set {ω : Ω | τ ω = i}
theorem
measure_theory.is_stopping_time.measurable_set_lt_le
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
[linear_order ι]
{f : measure_theory.filtration ι m}
{τ : Ω → ι}
[topological_space ι]
[order_topology ι]
[topological_space.first_countable_topology ι]
(hτ : measure_theory.is_stopping_time f τ)
{i j : ι}
(hle : i ≤ j) :
measurable_set {ω : Ω | τ ω < i}
theorem
measure_theory.is_stopping_time_of_measurable_set_eq
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
[preorder ι]
[countable ι]
{f : measure_theory.filtration ι m}
{τ : Ω → ι}
(hτ : ∀ (i : ι), measurable_set {ω : Ω | τ ω = i}) :
@[protected]
theorem
measure_theory.is_stopping_time.max
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
[linear_order ι]
{f : measure_theory.filtration ι m}
{τ π : Ω → ι}
(hτ : measure_theory.is_stopping_time f τ)
(hπ : measure_theory.is_stopping_time f π) :
measure_theory.is_stopping_time f (λ (ω : Ω), linear_order.max (τ ω) (π ω))
@[protected]
theorem
measure_theory.is_stopping_time.max_const
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
[linear_order ι]
{f : measure_theory.filtration ι m}
{τ : Ω → ι}
(hτ : measure_theory.is_stopping_time f τ)
(i : ι) :
measure_theory.is_stopping_time f (λ (ω : Ω), linear_order.max (τ ω) i)
@[protected]
theorem
measure_theory.is_stopping_time.min
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
[linear_order ι]
{f : measure_theory.filtration ι m}
{τ π : Ω → ι}
(hτ : measure_theory.is_stopping_time f τ)
(hπ : measure_theory.is_stopping_time f π) :
measure_theory.is_stopping_time f (λ (ω : Ω), linear_order.min (τ ω) (π ω))
@[protected]
theorem
measure_theory.is_stopping_time.min_const
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
[linear_order ι]
{f : measure_theory.filtration ι m}
{τ : Ω → ι}
(hτ : measure_theory.is_stopping_time f τ)
(i : ι) :
measure_theory.is_stopping_time f (λ (ω : Ω), linear_order.min (τ ω) i)
theorem
measure_theory.is_stopping_time.add_const
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
[add_group ι]
[preorder ι]
[covariant_class ι ι (function.swap has_add.add) has_le.le]
[covariant_class ι ι has_add.add has_le.le]
{f : measure_theory.filtration ι m}
{τ : Ω → ι}
(hτ : measure_theory.is_stopping_time f τ)
{i : ι}
(hi : 0 ≤ i) :
measure_theory.is_stopping_time f (λ (ω : Ω), τ ω + i)
theorem
measure_theory.is_stopping_time.add_const_nat
{Ω : Type u_1}
{m : measurable_space Ω}
{f : measure_theory.filtration ℕ m}
{τ : Ω → ℕ}
(hτ : measure_theory.is_stopping_time f τ)
{i : ℕ} :
measure_theory.is_stopping_time f (λ (ω : Ω), τ ω + i)
theorem
measure_theory.is_stopping_time.add
{Ω : Type u_1}
{m : measurable_space Ω}
{f : measure_theory.filtration ℕ m}
{τ π : Ω → ℕ}
(hτ : measure_theory.is_stopping_time f τ)
(hπ : measure_theory.is_stopping_time f π) :
measure_theory.is_stopping_time f (τ + π)
@[protected]
def
measure_theory.is_stopping_time.measurable_space
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
[preorder ι]
{f : measure_theory.filtration ι m}
{τ : Ω → ι}
(hτ : measure_theory.is_stopping_time f τ) :
The associated σ-algebra with a stopping time.
Equations
- hτ.measurable_space = {measurable_set' := λ (s : set Ω), ∀ (i : ι), measurable_set (s ∩ {ω : Ω | τ ω ≤ i}), measurable_set_empty := _, measurable_set_compl := _, measurable_set_Union := _}
@[protected]
theorem
measure_theory.is_stopping_time.measurable_set
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
[preorder ι]
{f : measure_theory.filtration ι m}
{τ : Ω → ι}
(hτ : measure_theory.is_stopping_time f τ)
(s : set Ω) :
measurable_set s ↔ ∀ (i : ι), measurable_set (s ∩ {ω : Ω | τ ω ≤ i})
theorem
measure_theory.is_stopping_time.measurable_space_mono
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
[preorder ι]
{f : measure_theory.filtration ι m}
{τ π : Ω → ι}
(hτ : measure_theory.is_stopping_time f τ)
(hπ : measure_theory.is_stopping_time f π)
(hle : τ ≤ π) :
theorem
measure_theory.is_stopping_time.measurable_space_le_of_countable
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
[preorder ι]
{f : measure_theory.filtration ι m}
{τ : Ω → ι}
[countable ι]
(hτ : measure_theory.is_stopping_time f τ) :
hτ.measurable_space ≤ m
theorem
measure_theory.is_stopping_time.measurable_space_le'
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
[preorder ι]
{f : measure_theory.filtration ι m}
{τ : Ω → ι}
[filter.at_top.is_countably_generated]
[filter.at_top.ne_bot]
(hτ : measure_theory.is_stopping_time f τ) :
hτ.measurable_space ≤ m
theorem
measure_theory.is_stopping_time.measurable_space_le
{Ω : Type u_1}
{m : measurable_space Ω}
{ι : Type u_2}
[semilattice_sup ι]
{f : measure_theory.filtration ι m}
{τ : Ω → ι}
[filter.at_top.is_countably_generated]
(hτ : measure_theory.is_stopping_time f τ) :
hτ.measurable_space ≤ m
@[simp]
theorem
measure_theory.is_stopping_time.measurable_space_const
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
[preorder ι]
(f : measure_theory.filtration ι m)
(i : ι) :
_.measurable_space = ⇑f i
theorem
measure_theory.is_stopping_time.measurable_set_inter_eq_iff
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
[preorder ι]
{f : measure_theory.filtration ι m}
{τ : Ω → ι}
(hτ : measure_theory.is_stopping_time f τ)
(s : set Ω)
(i : ι) :
measurable_set (s ∩ {ω : Ω | τ ω = i}) ↔ measurable_set (s ∩ {ω : Ω | τ ω = i})
theorem
measure_theory.is_stopping_time.measurable_space_le_of_le_const
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
[preorder ι]
{f : measure_theory.filtration ι m}
{τ : Ω → ι}
(hτ : measure_theory.is_stopping_time f τ)
{i : ι}
(hτ_le : ∀ (ω : Ω), τ ω ≤ i) :
hτ.measurable_space ≤ ⇑f i
theorem
measure_theory.is_stopping_time.measurable_space_le_of_le
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
[preorder ι]
{f : measure_theory.filtration ι m}
{τ : Ω → ι}
(hτ : measure_theory.is_stopping_time f τ)
{n : ι}
(hτ_le : ∀ (ω : Ω), τ ω ≤ n) :
hτ.measurable_space ≤ m
theorem
measure_theory.is_stopping_time.le_measurable_space_of_const_le
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
[preorder ι]
{f : measure_theory.filtration ι m}
{τ : Ω → ι}
(hτ : measure_theory.is_stopping_time f τ)
{i : ι}
(hτ_le : ∀ (ω : Ω), i ≤ τ ω) :
⇑f i ≤ hτ.measurable_space
@[protected, instance]
def
measure_theory.is_stopping_time.sigma_finite_stopping_time
{Ω : Type u_1}
{m : measurable_space Ω}
{ι : Type u_2}
[semilattice_sup ι]
[order_bot ι]
[filter.at_top.is_countably_generated]
{μ : measure_theory.measure Ω}
{f : measure_theory.filtration ι m}
{τ : Ω → ι}
[measure_theory.sigma_finite_filtration μ f]
(hτ : measure_theory.is_stopping_time f τ) :
@[protected, instance]
def
measure_theory.is_stopping_time.sigma_finite_stopping_time_of_le
{Ω : Type u_1}
{m : measurable_space Ω}
{ι : Type u_2}
[semilattice_sup ι]
[order_bot ι]
{μ : measure_theory.measure Ω}
{f : measure_theory.filtration ι m}
{τ : Ω → ι}
[measure_theory.sigma_finite_filtration μ f]
(hτ : measure_theory.is_stopping_time f τ)
{n : ι}
(hτ_le : ∀ (ω : Ω), τ ω ≤ n) :
@[protected]
theorem
measure_theory.is_stopping_time.measurable_set_le'
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
[linear_order ι]
{f : measure_theory.filtration ι m}
{τ : Ω → ι}
(hτ : measure_theory.is_stopping_time f τ)
(i : ι) :
measurable_set {ω : Ω | τ ω ≤ i}
@[protected]
theorem
measure_theory.is_stopping_time.measurable_set_gt'
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
[linear_order ι]
{f : measure_theory.filtration ι m}
{τ : Ω → ι}
(hτ : measure_theory.is_stopping_time f τ)
(i : ι) :
measurable_set {ω : Ω | i < τ ω}
@[protected]
theorem
measure_theory.is_stopping_time.measurable_set_eq'
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
[linear_order ι]
{f : measure_theory.filtration ι m}
{τ : Ω → ι}
[topological_space ι]
[order_topology ι]
[topological_space.first_countable_topology ι]
(hτ : measure_theory.is_stopping_time f τ)
(i : ι) :
measurable_set {ω : Ω | τ ω = i}
@[protected]
theorem
measure_theory.is_stopping_time.measurable_set_ge'
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
[linear_order ι]
{f : measure_theory.filtration ι m}
{τ : Ω → ι}
[topological_space ι]
[order_topology ι]
[topological_space.first_countable_topology ι]
(hτ : measure_theory.is_stopping_time f τ)
(i : ι) :
measurable_set {ω : Ω | i ≤ τ ω}
@[protected]
theorem
measure_theory.is_stopping_time.measurable_set_lt'
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
[linear_order ι]
{f : measure_theory.filtration ι m}
{τ : Ω → ι}
[topological_space ι]
[order_topology ι]
[topological_space.first_countable_topology ι]
(hτ : measure_theory.is_stopping_time f τ)
(i : ι) :
measurable_set {ω : Ω | τ ω < i}
@[protected]
theorem
measure_theory.is_stopping_time.measurable_set_eq_of_countable_range'
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
[linear_order ι]
{f : measure_theory.filtration ι m}
{τ : Ω → ι}
(hτ : measure_theory.is_stopping_time f τ)
(h_countable : (set.range τ).countable)
(i : ι) :
measurable_set {ω : Ω | τ ω = i}
@[protected]
theorem
measure_theory.is_stopping_time.measurable_set_eq_of_countable'
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
[linear_order ι]
{f : measure_theory.filtration ι m}
{τ : Ω → ι}
[countable ι]
(hτ : measure_theory.is_stopping_time f τ)
(i : ι) :
measurable_set {ω : Ω | τ ω = i}
@[protected]
theorem
measure_theory.is_stopping_time.measurable_set_ge_of_countable_range'
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
[linear_order ι]
{f : measure_theory.filtration ι m}
{τ : Ω → ι}
(hτ : measure_theory.is_stopping_time f τ)
(h_countable : (set.range τ).countable)
(i : ι) :
measurable_set {ω : Ω | i ≤ τ ω}
@[protected]
theorem
measure_theory.is_stopping_time.measurable_set_ge_of_countable'
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
[linear_order ι]
{f : measure_theory.filtration ι m}
{τ : Ω → ι}
[countable ι]
(hτ : measure_theory.is_stopping_time f τ)
(i : ι) :
measurable_set {ω : Ω | i ≤ τ ω}
@[protected]
theorem
measure_theory.is_stopping_time.measurable_set_lt_of_countable_range'
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
[linear_order ι]
{f : measure_theory.filtration ι m}
{τ : Ω → ι}
(hτ : measure_theory.is_stopping_time f τ)
(h_countable : (set.range τ).countable)
(i : ι) :
measurable_set {ω : Ω | τ ω < i}
@[protected]
theorem
measure_theory.is_stopping_time.measurable_set_lt_of_countable'
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
[linear_order ι]
{f : measure_theory.filtration ι m}
{τ : Ω → ι}
[countable ι]
(hτ : measure_theory.is_stopping_time f τ)
(i : ι) :
measurable_set {ω : Ω | τ ω < i}
@[protected]
theorem
measure_theory.is_stopping_time.measurable_space_le_of_countable_range
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
[linear_order ι]
{f : measure_theory.filtration ι m}
{τ : Ω → ι}
(hτ : measure_theory.is_stopping_time f τ)
(h_countable : (set.range τ).countable) :
hτ.measurable_space ≤ m
@[protected]
theorem
measure_theory.is_stopping_time.measurable
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
[linear_order ι]
{f : measure_theory.filtration ι m}
{τ : Ω → ι}
[topological_space ι]
[measurable_space ι]
[borel_space ι]
[order_topology ι]
[topological_space.second_countable_topology ι]
(hτ : measure_theory.is_stopping_time f τ) :
@[protected]
theorem
measure_theory.is_stopping_time.measurable_of_le
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
[linear_order ι]
{f : measure_theory.filtration ι m}
{τ : Ω → ι}
[topological_space ι]
[measurable_space ι]
[borel_space ι]
[order_topology ι]
[topological_space.second_countable_topology ι]
(hτ : measure_theory.is_stopping_time f τ)
{i : ι}
(hτ_le : ∀ (ω : Ω), τ ω ≤ i) :
theorem
measure_theory.is_stopping_time.measurable_space_min
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
[linear_order ι]
{f : measure_theory.filtration ι m}
{τ π : Ω → ι}
(hτ : measure_theory.is_stopping_time f τ)
(hπ : measure_theory.is_stopping_time f π) :
theorem
measure_theory.is_stopping_time.measurable_set_min_iff
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
[linear_order ι]
{f : measure_theory.filtration ι m}
{τ π : Ω → ι}
(hτ : measure_theory.is_stopping_time f τ)
(hπ : measure_theory.is_stopping_time f π)
(s : set Ω) :
theorem
measure_theory.is_stopping_time.measurable_space_min_const
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
[linear_order ι]
{f : measure_theory.filtration ι m}
{τ : Ω → ι}
(hτ : measure_theory.is_stopping_time f τ)
{i : ι} :
_.measurable_space = hτ.measurable_space ⊓ ⇑f i
theorem
measure_theory.is_stopping_time.measurable_set_min_const_iff
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
[linear_order ι]
{f : measure_theory.filtration ι m}
{τ : Ω → ι}
(hτ : measure_theory.is_stopping_time f τ)
(s : set Ω)
{i : ι} :
theorem
measure_theory.is_stopping_time.measurable_set_inter_le
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
[linear_order ι]
{f : measure_theory.filtration ι m}
{τ π : Ω → ι}
[topological_space ι]
[topological_space.second_countable_topology ι]
[order_topology ι]
[measurable_space ι]
[borel_space ι]
(hτ : measure_theory.is_stopping_time f τ)
(hπ : measure_theory.is_stopping_time f π)
(s : set Ω)
(hs : measurable_set s) :
measurable_set (s ∩ {ω : Ω | τ ω ≤ π ω})
theorem
measure_theory.is_stopping_time.measurable_set_inter_le_iff
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
[linear_order ι]
{f : measure_theory.filtration ι m}
{τ π : Ω → ι}
[topological_space ι]
[topological_space.second_countable_topology ι]
[order_topology ι]
[measurable_space ι]
[borel_space ι]
(hτ : measure_theory.is_stopping_time f τ)
(hπ : measure_theory.is_stopping_time f π)
(s : set Ω) :
measurable_set (s ∩ {ω : Ω | τ ω ≤ π ω}) ↔ measurable_set (s ∩ {ω : Ω | τ ω ≤ π ω})
theorem
measure_theory.is_stopping_time.measurable_set_inter_le_const_iff
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
[linear_order ι]
{f : measure_theory.filtration ι m}
{τ : Ω → ι}
(hτ : measure_theory.is_stopping_time f τ)
(s : set Ω)
(i : ι) :
measurable_set (s ∩ {ω : Ω | τ ω ≤ i}) ↔ measurable_set (s ∩ {ω : Ω | τ ω ≤ i})
theorem
measure_theory.is_stopping_time.measurable_set_le_stopping_time
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
[linear_order ι]
{f : measure_theory.filtration ι m}
{τ π : Ω → ι}
[topological_space ι]
[topological_space.second_countable_topology ι]
[order_topology ι]
[measurable_space ι]
[borel_space ι]
(hτ : measure_theory.is_stopping_time f τ)
(hπ : measure_theory.is_stopping_time f π) :
measurable_set {ω : Ω | τ ω ≤ π ω}
theorem
measure_theory.is_stopping_time.measurable_set_stopping_time_le
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
[linear_order ι]
{f : measure_theory.filtration ι m}
{τ π : Ω → ι}
[topological_space ι]
[topological_space.second_countable_topology ι]
[order_topology ι]
[measurable_space ι]
[borel_space ι]
(hτ : measure_theory.is_stopping_time f τ)
(hπ : measure_theory.is_stopping_time f π) :
measurable_set {ω : Ω | τ ω ≤ π ω}
theorem
measure_theory.is_stopping_time.measurable_set_eq_stopping_time
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
[linear_order ι]
{f : measure_theory.filtration ι m}
{τ π : Ω → ι}
[add_group ι]
[topological_space ι]
[measurable_space ι]
[borel_space ι]
[order_topology ι]
[measurable_singleton_class ι]
[topological_space.second_countable_topology ι]
[has_measurable_sub₂ ι]
(hτ : measure_theory.is_stopping_time f τ)
(hπ : measure_theory.is_stopping_time f π) :
measurable_set {ω : Ω | τ ω = π ω}
theorem
measure_theory.is_stopping_time.measurable_set_eq_stopping_time_of_countable
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
[linear_order ι]
{f : measure_theory.filtration ι m}
{τ π : Ω → ι}
[countable ι]
[topological_space ι]
[measurable_space ι]
[borel_space ι]
[order_topology ι]
[measurable_singleton_class ι]
[topological_space.second_countable_topology ι]
(hτ : measure_theory.is_stopping_time f τ)
(hπ : measure_theory.is_stopping_time f π) :
measurable_set {ω : Ω | τ ω = π ω}
Stopped value and stopped process #
theorem
measure_theory.stopped_value_const
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
(u : ι → Ω → β)
(i : ι) :
measure_theory.stopped_value u (λ (ω : Ω), i) = u i
def
measure_theory.stopped_process
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[linear_order ι]
(u : ι → Ω → β)
(τ : Ω → ι) :
Given a map u : ι → Ω → E, the stopped process with respect to τ is u i ω if
i ≤ τ ω, and u (τ ω) ω otherwise.
Intuitively, the stopped process stops evolving once the stopping time has occured.
Equations
- measure_theory.stopped_process u τ = λ (i : ι) (ω : Ω), u (linear_order.min i (τ ω)) ω
theorem
measure_theory.stopped_process_eq_stopped_value
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[linear_order ι]
{u : ι → Ω → β}
{τ : Ω → ι} :
measure_theory.stopped_process u τ = λ (i : ι), measure_theory.stopped_value u (λ (ω : Ω), linear_order.min i (τ ω))
theorem
measure_theory.stopped_value_stopped_process
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[linear_order ι]
{u : ι → Ω → β}
{τ σ : Ω → ι} :
measure_theory.stopped_value (measure_theory.stopped_process u τ) σ = measure_theory.stopped_value u (λ (ω : Ω), linear_order.min (σ ω) (τ ω))
theorem
measure_theory.stopped_process_eq_of_le
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[linear_order ι]
{u : ι → Ω → β}
{τ : Ω → ι}
{i : ι}
{ω : Ω}
(h : i ≤ τ ω) :
measure_theory.stopped_process u τ i ω = u i ω
theorem
measure_theory.stopped_process_eq_of_ge
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[linear_order ι]
{u : ι → Ω → β}
{τ : Ω → ι}
{i : ι}
{ω : Ω}
(h : τ ω ≤ i) :
measure_theory.stopped_process u τ i ω = u (τ ω) ω
theorem
measure_theory.prog_measurable_min_stopping_time
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
[linear_order ι]
[measurable_space ι]
[topological_space ι]
[order_topology ι]
[topological_space.second_countable_topology ι]
[borel_space ι]
{τ : Ω → ι}
{f : measure_theory.filtration ι m}
[topological_space.metrizable_space ι]
(hτ : measure_theory.is_stopping_time f τ) :
measure_theory.prog_measurable f (λ (i : ι) (ω : Ω), linear_order.min i (τ ω))
theorem
measure_theory.prog_measurable.stopped_process
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : measurable_space Ω}
[linear_order ι]
[measurable_space ι]
[topological_space ι]
[order_topology ι]
[topological_space.second_countable_topology ι]
[borel_space ι]
[topological_space β]
{u : ι → Ω → β}
{τ : Ω → ι}
{f : measure_theory.filtration ι m}
[topological_space.metrizable_space ι]
(h : measure_theory.prog_measurable f u)
(hτ : measure_theory.is_stopping_time f τ) :
theorem
measure_theory.prog_measurable.adapted_stopped_process
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : measurable_space Ω}
[linear_order ι]
[measurable_space ι]
[topological_space ι]
[order_topology ι]
[topological_space.second_countable_topology ι]
[borel_space ι]
[topological_space β]
{u : ι → Ω → β}
{τ : Ω → ι}
{f : measure_theory.filtration ι m}
[topological_space.metrizable_space ι]
(h : measure_theory.prog_measurable f u)
(hτ : measure_theory.is_stopping_time f τ) :
theorem
measure_theory.prog_measurable.strongly_measurable_stopped_process
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : measurable_space Ω}
[linear_order ι]
[measurable_space ι]
[topological_space ι]
[order_topology ι]
[topological_space.second_countable_topology ι]
[borel_space ι]
[topological_space β]
{u : ι → Ω → β}
{τ : Ω → ι}
{f : measure_theory.filtration ι m}
[topological_space.metrizable_space ι]
(hu : measure_theory.prog_measurable f u)
(hτ : measure_theory.is_stopping_time f τ)
(i : ι) :
theorem
measure_theory.strongly_measurable_stopped_value_of_le
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : measurable_space Ω}
[linear_order ι]
[measurable_space ι]
[topological_space ι]
[order_topology ι]
[topological_space.second_countable_topology ι]
[borel_space ι]
[topological_space β]
{u : ι → Ω → β}
{τ : Ω → ι}
{f : measure_theory.filtration ι m}
(h : measure_theory.prog_measurable f u)
(hτ : measure_theory.is_stopping_time f τ)
{n : ι}
(hτ_le : ∀ (ω : Ω), τ ω ≤ n) :
theorem
measure_theory.measurable_stopped_value
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : measurable_space Ω}
[linear_order ι]
[measurable_space ι]
[topological_space ι]
[order_topology ι]
[topological_space.second_countable_topology ι]
[borel_space ι]
[topological_space β]
{u : ι → Ω → β}
{τ : Ω → ι}
{f : measure_theory.filtration ι m}
[topological_space.metrizable_space β]
[measurable_space β]
[borel_space β]
(hf_prog : measure_theory.prog_measurable f u)
(hτ : measure_theory.is_stopping_time f τ) :
theorem
measure_theory.stopped_value_eq'
{Ω : Type u_1}
{ι : Type u_3}
{τ : Ω → ι}
{E : Type u_4}
{u : ι → Ω → E}
[preorder ι]
[locally_finite_order_bot ι]
[add_comm_monoid E]
{N : ι}
(hbdd : ∀ (ω : Ω), τ ω ≤ N) :
measure_theory.stopped_value u τ = (finset.Iic N).sum (λ (i : ι), {ω : Ω | τ ω = i}.indicator (u i))
theorem
measure_theory.stopped_process_eq_of_mem_finset
{Ω : Type u_1}
{ι : Type u_3}
{τ : Ω → ι}
{E : Type u_4}
{u : ι → Ω → E}
[linear_order ι]
[add_comm_monoid E]
{s : finset ι}
(n : ι)
(hbdd : ∀ (ω : Ω), τ ω < n → τ ω ∈ s) :
measure_theory.stopped_process u τ n = {a : Ω | n ≤ τ a}.indicator (u n) + (finset.filter (λ (_x : ι), _x < n) s).sum (λ (i : ι), {ω : Ω | τ ω = i}.indicator (u i))
theorem
measure_theory.stopped_process_eq''
{Ω : Type u_1}
{ι : Type u_3}
{τ : Ω → ι}
{E : Type u_4}
{u : ι → Ω → E}
[linear_order ι]
[locally_finite_order_bot ι]
[add_comm_monoid E]
(n : ι) :
measure_theory.stopped_process u τ n = {a : Ω | n ≤ τ a}.indicator (u n) + (finset.Iio n).sum (λ (i : ι), {ω : Ω | τ ω = i}.indicator (u i))
theorem
measure_theory.mem_ℒp_stopped_value_of_mem_finset
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
{μ : measure_theory.measure Ω}
{τ : Ω → ι}
{E : Type u_4}
{p : ennreal}
{u : ι → Ω → E}
[partial_order ι]
{ℱ : measure_theory.filtration ι m}
[normed_add_comm_group E]
(hτ : measure_theory.is_stopping_time ℱ τ)
(hu : ∀ (n : ι), measure_theory.mem_ℒp (u n) p μ)
{s : finset ι}
(hbdd : ∀ (ω : Ω), τ ω ∈ s) :
theorem
measure_theory.mem_ℒp_stopped_value
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
{μ : measure_theory.measure Ω}
{τ : Ω → ι}
{E : Type u_4}
{p : ennreal}
{u : ι → Ω → E}
[partial_order ι]
{ℱ : measure_theory.filtration ι m}
[normed_add_comm_group E]
[locally_finite_order_bot ι]
(hτ : measure_theory.is_stopping_time ℱ τ)
(hu : ∀ (n : ι), measure_theory.mem_ℒp (u n) p μ)
{N : ι}
(hbdd : ∀ (ω : Ω), τ ω ≤ N) :
theorem
measure_theory.integrable_stopped_value_of_mem_finset
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
{μ : measure_theory.measure Ω}
{τ : Ω → ι}
{E : Type u_4}
{u : ι → Ω → E}
[partial_order ι]
{ℱ : measure_theory.filtration ι m}
[normed_add_comm_group E]
(hτ : measure_theory.is_stopping_time ℱ τ)
(hu : ∀ (n : ι), measure_theory.integrable (u n) μ)
{s : finset ι}
(hbdd : ∀ (ω : Ω), τ ω ∈ s) :
theorem
measure_theory.integrable_stopped_value
{Ω : Type u_1}
(ι : Type u_3)
{m : measurable_space Ω}
{μ : measure_theory.measure Ω}
{τ : Ω → ι}
{E : Type u_4}
{u : ι → Ω → E}
[partial_order ι]
{ℱ : measure_theory.filtration ι m}
[normed_add_comm_group E]
[locally_finite_order_bot ι]
(hτ : measure_theory.is_stopping_time ℱ τ)
(hu : ∀ (n : ι), measure_theory.integrable (u n) μ)
{N : ι}
(hbdd : ∀ (ω : Ω), τ ω ≤ N) :
theorem
measure_theory.mem_ℒp_stopped_process_of_mem_finset
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
{μ : measure_theory.measure Ω}
{τ : Ω → ι}
{E : Type u_4}
{p : ennreal}
{u : ι → Ω → E}
[linear_order ι]
[topological_space ι]
[order_topology ι]
[topological_space.first_countable_topology ι]
{ℱ : measure_theory.filtration ι m}
[normed_add_comm_group E]
(hτ : measure_theory.is_stopping_time ℱ τ)
(hu : ∀ (n : ι), measure_theory.mem_ℒp (u n) p μ)
(n : ι)
{s : finset ι}
(hbdd : ∀ (ω : Ω), τ ω < n → τ ω ∈ s) :
measure_theory.mem_ℒp (measure_theory.stopped_process u τ n) p μ
theorem
measure_theory.mem_ℒp_stopped_process
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
{μ : measure_theory.measure Ω}
{τ : Ω → ι}
{E : Type u_4}
{p : ennreal}
{u : ι → Ω → E}
[linear_order ι]
[topological_space ι]
[order_topology ι]
[topological_space.first_countable_topology ι]
{ℱ : measure_theory.filtration ι m}
[normed_add_comm_group E]
[locally_finite_order_bot ι]
(hτ : measure_theory.is_stopping_time ℱ τ)
(hu : ∀ (n : ι), measure_theory.mem_ℒp (u n) p μ)
(n : ι) :
measure_theory.mem_ℒp (measure_theory.stopped_process u τ n) p μ
theorem
measure_theory.integrable_stopped_process_of_mem_finset
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
{μ : measure_theory.measure Ω}
{τ : Ω → ι}
{E : Type u_4}
{u : ι → Ω → E}
[linear_order ι]
[topological_space ι]
[order_topology ι]
[topological_space.first_countable_topology ι]
{ℱ : measure_theory.filtration ι m}
[normed_add_comm_group E]
(hτ : measure_theory.is_stopping_time ℱ τ)
(hu : ∀ (n : ι), measure_theory.integrable (u n) μ)
(n : ι)
{s : finset ι}
(hbdd : ∀ (ω : Ω), τ ω < n → τ ω ∈ s) :
theorem
measure_theory.integrable_stopped_process
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
{μ : measure_theory.measure Ω}
{τ : Ω → ι}
{E : Type u_4}
{u : ι → Ω → E}
[linear_order ι]
[topological_space ι]
[order_topology ι]
[topological_space.first_countable_topology ι]
{ℱ : measure_theory.filtration ι m}
[normed_add_comm_group E]
[locally_finite_order_bot ι]
(hτ : measure_theory.is_stopping_time ℱ τ)
(hu : ∀ (n : ι), measure_theory.integrable (u n) μ)
(n : ι) :
theorem
measure_theory.adapted.stopped_process
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : measurable_space Ω}
[topological_space β]
[topological_space.pseudo_metrizable_space β]
[linear_order ι]
[topological_space ι]
[topological_space.second_countable_topology ι]
[order_topology ι]
[measurable_space ι]
[borel_space ι]
{f : measure_theory.filtration ι m}
{u : ι → Ω → β}
{τ : Ω → ι}
[topological_space.metrizable_space ι]
(hu : measure_theory.adapted f u)
(hu_cont : ∀ (ω : Ω), continuous (λ (i : ι), u i ω))
(hτ : measure_theory.is_stopping_time f τ) :
The stopped process of an adapted process with continuous paths is adapted.
theorem
measure_theory.adapted.stopped_process_of_discrete
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : measurable_space Ω}
[topological_space β]
[topological_space.pseudo_metrizable_space β]
[linear_order ι]
[topological_space ι]
[topological_space.second_countable_topology ι]
[order_topology ι]
[measurable_space ι]
[borel_space ι]
{f : measure_theory.filtration ι m}
{u : ι → Ω → β}
{τ : Ω → ι}
[discrete_topology ι]
(hu : measure_theory.adapted f u)
(hτ : measure_theory.is_stopping_time f τ) :
If the indexing order has the discrete topology, then the stopped process of an adapted process is adapted.
theorem
measure_theory.adapted.strongly_measurable_stopped_process
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : measurable_space Ω}
[topological_space β]
[topological_space.pseudo_metrizable_space β]
[linear_order ι]
[topological_space ι]
[topological_space.second_countable_topology ι]
[order_topology ι]
[measurable_space ι]
[borel_space ι]
{f : measure_theory.filtration ι m}
{u : ι → Ω → β}
{τ : Ω → ι}
[topological_space.metrizable_space ι]
(hu : measure_theory.adapted f u)
(hu_cont : ∀ (ω : Ω), continuous (λ (i : ι), u i ω))
(hτ : measure_theory.is_stopping_time f τ)
(n : ι) :
theorem
measure_theory.adapted.strongly_measurable_stopped_process_of_discrete
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : measurable_space Ω}
[topological_space β]
[topological_space.pseudo_metrizable_space β]
[linear_order ι]
[topological_space ι]
[topological_space.second_countable_topology ι]
[order_topology ι]
[measurable_space ι]
[borel_space ι]
{f : measure_theory.filtration ι m}
{u : ι → Ω → β}
{τ : Ω → ι}
[discrete_topology ι]
(hu : measure_theory.adapted f u)
(hτ : measure_theory.is_stopping_time f τ)
(n : ι) :
Filtrations indexed by ℕ #
theorem
measure_theory.stopped_value_sub_eq_sum
{Ω : Type u_1}
{β : Type u_2}
{u : ℕ → Ω → β}
{τ π : Ω → ℕ}
[add_comm_group β]
(hle : τ ≤ π) :
measure_theory.stopped_value u π - measure_theory.stopped_value u τ = λ (ω : Ω), (finset.Ico (τ ω) (π ω)).sum (λ (i : ℕ), u (i + 1) - u i) ω
theorem
measure_theory.stopped_value_sub_eq_sum'
{Ω : Type u_1}
{β : Type u_2}
{u : ℕ → Ω → β}
{τ π : Ω → ℕ}
[add_comm_group β]
(hle : τ ≤ π)
{N : ℕ}
(hbdd : ∀ (ω : Ω), π ω ≤ N) :
measure_theory.stopped_value u π - measure_theory.stopped_value u τ = λ (ω : Ω), (finset.range (N + 1)).sum (λ (i : ℕ), {ω : Ω | τ ω ≤ i ∧ i < π ω}.indicator (u (i + 1) - u i)) ω
theorem
measure_theory.is_stopping_time.piecewise_of_le
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
[preorder ι]
{𝒢 : measure_theory.filtration ι m}
{τ η : Ω → ι}
{i : ι}
{s : set Ω}
[decidable_pred (λ (_x : Ω), _x ∈ s)]
(hτ_st : measure_theory.is_stopping_time 𝒢 τ)
(hη_st : measure_theory.is_stopping_time 𝒢 η)
(hτ : ∀ (ω : Ω), i ≤ τ ω)
(hη : ∀ (ω : Ω), i ≤ η ω)
(hs : measurable_set s) :
measure_theory.is_stopping_time 𝒢 (s.piecewise τ η)
Given stopping times τ and η which are bounded below, set.piecewise s τ η is also
a stopping time with respect to the same filtration.
theorem
measure_theory.is_stopping_time_piecewise_const
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
[preorder ι]
{𝒢 : measure_theory.filtration ι m}
{i j : ι}
{s : set Ω}
[decidable_pred (λ (_x : Ω), _x ∈ s)]
(hij : i ≤ j)
(hs : measurable_set s) :
measure_theory.is_stopping_time 𝒢 (s.piecewise (λ (_x : Ω), i) (λ (_x : Ω), j))
theorem
measure_theory.stopped_value_piecewise_const
{Ω : Type u_1}
{s : set Ω}
[decidable_pred (λ (_x : Ω), _x ∈ s)]
{ι' : Type u_2}
{i j : ι'}
{f : ι' → Ω → ℝ} :
measure_theory.stopped_value f (s.piecewise (λ (_x : Ω), i) (λ (_x : Ω), j)) = s.piecewise (f i) (f j)
Conditional expectation with respect to the σ-algebra generated by a stopping time #
theorem
measure_theory.condexp_stopping_time_ae_eq_restrict_eq_of_countable_range
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
[linear_order ι]
{μ : measure_theory.measure Ω}
{ℱ : measure_theory.filtration ι m}
{τ : Ω → ι}
{E : Type u_4}
[normed_add_comm_group E]
[normed_space ℝ E]
[complete_space E]
{f : Ω → E}
[measure_theory.sigma_finite_filtration μ ℱ]
(hτ : measure_theory.is_stopping_time ℱ τ)
(h_countable : (set.range τ).countable)
[measure_theory.sigma_finite (μ.trim _)]
(i : ι) :
measure_theory.condexp hτ.measurable_space μ f =ᵐ[μ.restrict {x : Ω | τ x = i}] measure_theory.condexp (⇑ℱ i) μ f
theorem
measure_theory.condexp_stopping_time_ae_eq_restrict_eq_of_countable
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
[linear_order ι]
{μ : measure_theory.measure Ω}
{ℱ : measure_theory.filtration ι m}
{τ : Ω → ι}
{E : Type u_4}
[normed_add_comm_group E]
[normed_space ℝ E]
[complete_space E]
{f : Ω → E}
[countable ι]
[measure_theory.sigma_finite_filtration μ ℱ]
(hτ : measure_theory.is_stopping_time ℱ τ)
[measure_theory.sigma_finite (μ.trim _)]
(i : ι) :
measure_theory.condexp hτ.measurable_space μ f =ᵐ[μ.restrict {x : Ω | τ x = i}] measure_theory.condexp (⇑ℱ i) μ f
theorem
measure_theory.condexp_min_stopping_time_ae_eq_restrict_le_const
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
[linear_order ι]
{μ : measure_theory.measure Ω}
{ℱ : measure_theory.filtration ι m}
{τ : Ω → ι}
{E : Type u_4}
[normed_add_comm_group E]
[normed_space ℝ E]
[complete_space E]
{f : Ω → E}
[filter.at_top.is_countably_generated]
(hτ : measure_theory.is_stopping_time ℱ τ)
(i : ι)
[measure_theory.sigma_finite (μ.trim _)] :
measure_theory.condexp _.measurable_space μ f =ᵐ[μ.restrict {x : Ω | τ x ≤ i}] measure_theory.condexp hτ.measurable_space μ f
theorem
measure_theory.condexp_stopping_time_ae_eq_restrict_eq
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
[linear_order ι]
{μ : measure_theory.measure Ω}
{ℱ : measure_theory.filtration ι m}
{τ : Ω → ι}
{E : Type u_4}
[normed_add_comm_group E]
[normed_space ℝ E]
[complete_space E]
{f : Ω → E}
[filter.at_top.is_countably_generated]
[topological_space ι]
[order_topology ι]
[topological_space.first_countable_topology ι]
[measure_theory.sigma_finite_filtration μ ℱ]
(hτ : measure_theory.is_stopping_time ℱ τ)
[measure_theory.sigma_finite (μ.trim _)]
(i : ι) :
measure_theory.condexp hτ.measurable_space μ f =ᵐ[μ.restrict {x : Ω | τ x = i}] measure_theory.condexp (⇑ℱ i) μ f
theorem
measure_theory.condexp_min_stopping_time_ae_eq_restrict_le
{Ω : Type u_1}
{ι : Type u_3}
{m : measurable_space Ω}
[linear_order ι]
{μ : measure_theory.measure Ω}
{ℱ : measure_theory.filtration ι m}
{τ σ : Ω → ι}
{E : Type u_4}
[normed_add_comm_group E]
[normed_space ℝ E]
[complete_space E]
{f : Ω → E}
[filter.at_top.is_countably_generated]
[topological_space ι]
[order_topology ι]
[measurable_space ι]
[topological_space.second_countable_topology ι]
[borel_space ι]
(hτ : measure_theory.is_stopping_time ℱ τ)
(hσ : measure_theory.is_stopping_time ℱ σ)
[measure_theory.sigma_finite (μ.trim _)] :
measure_theory.condexp _.measurable_space μ f =ᵐ[μ.restrict {x : Ω | τ x ≤ σ x}] measure_theory.condexp hτ.measurable_space μ f