MeasureTheory.IsStoppingTime.measurableSet_eq_of_countable_range'
theorem MeasureTheory.IsStoppingTime.measurableSet_eq_of_countable_range' :
∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : LinearOrder ι] {f : MeasureTheory.Filtration ι m}
{τ : Ω → ι} (hτ : MeasureTheory.IsStoppingTime f τ),
(Set.range τ).Countable → ∀ (i : ι), MeasurableSet {ω | τ ω = i}
The theorem `MeasureTheory.IsStoppingTime.measurableSet_eq_of_countable_range'` states that for any types `Ω` and `ι`, any measurable space `m` over `Ω`, any linear order over `ι`, any filtration `f` over the measurable space `m` indexed by `ι`, and any function `τ` from `Ω` to `ι` which respects the stopping time property with respect to `f`, if the range of the function `τ` is countable, then for any `i` in `ι`, the set of elements of `Ω` such that `τ` of the element equals `i` is a measurable set.
In simpler terms, given a stopping time rule `τ` whose possible outcomes are countable, the set of all outcomes that stop at a specific time `i` can be measured using the given measure theory.
More concisely: If `τ: Ω → ι` is a measurable, countably-valued stopping time with respect to filtration `f` on measurable space `(Ω, m)`, then for all `i` in `ι`, the set `{ω in Ω | τ(ω) = i}` is measurable.
|
Mathlib.Probability.Process.Stopping._auxLemma.23
theorem Mathlib.Probability.Process.Stopping._auxLemma.23 :
∀ {α : Type u} (x : α) (a b : Set α), (x ∈ a ∩ b) = (x ∈ a ∧ x ∈ b)
This theorem states that for any type `α`, any element `x` of that type, and any two sets `a` and `b` of that type, the statement "x is in the intersection of a and b" is equivalent to the statement "x is in a and x is in b". In other words, an element belongs to the intersection of two sets if and only if it belongs to both of these sets.
More concisely: For any type `α` and sets `a` and `b` of type `α`, `x ∈ a ∧ x ∈ b` if and only if `x ∈ a ∩ b`.
|
MeasureTheory.IsStoppingTime.measurableSpace_le
theorem MeasureTheory.IsStoppingTime.measurableSpace_le :
∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {ι : Type u_4} [inst : SemilatticeSup ι] {f : MeasureTheory.Filtration ι m}
{τ : Ω → ι} [inst_1 : Filter.atTop.IsCountablyGenerated] (hτ : MeasureTheory.IsStoppingTime f τ),
hτ.measurableSpace ≤ m
The theorem `MeasureTheory.IsStoppingTime.measurableSpace_le` states that for any type `Ω` with a measurable space structure `m`, any type `ι` with a semilattice sup structure, any filtration `f` of `m` indexed by `ι`, and any function `τ` from `Ω` to `ι`, if `τ` is a stopping time with respect to `f` and the filter `atTop` is countably generated, then the measurable space associated with the stopping time `τ` is a sub-measurable space of `m`. In other words, every set that is measurable in the σ-algebra associated with the stopping time `τ` is also measurable in the original measurable space `m`.
More concisely: For any measurable space `(Ω, m)`, semilattice `ι` with sup structure, filtration `f: ι -> Set Ω.Measurable` indexed by `ι`, and stopping time `τ: Ω -> ι` with respect to `f` on a countably generated filter `atTop`, the associated measurable space of `τ` is a sub-measurable space of `m`. That is, every set measurable in `τ`'s σ-algebra is measurable in `m`.
|
Mathlib.Probability.Process.Stopping._auxLemma.17
theorem Mathlib.Probability.Process.Stopping._auxLemma.17 :
∀ {α : Type u} [inst : PartialOrder α] {a b : α}, (a < b) = (a ≤ b ∧ a ≠ b)
This theorem states that for any two elements `a` and `b` of a certain type `α` that forms a partial order, the statement "`a` is less than `b`" is equivalent to the conjunction of "`a` is less than or equal to `b`" and "`a` is not equal to `b`". This is a fundamental property of partial orders, reflecting that "less than" means "less than or equal to" but not "equal to".
More concisely: In a partial order, `a` is less than `b` if and only if `a` is strictly less than or equal to `b`.
|
MeasureTheory.isStoppingTime_const
theorem MeasureTheory.isStoppingTime_const :
∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : Preorder ι] (f : MeasureTheory.Filtration ι m)
(i : ι), MeasureTheory.IsStoppingTime f fun x => i
The theorem `MeasureTheory.isStoppingTime_const` asserts that for any measurable space `Ω`, any type `ι` equipped with a preorder, any filtration `f` on the measurable space indexed by `ι`, and any element `i` of `ι`, the function which assigns `i` to every element of `Ω` is a stopping time with respect to `f`. In other words, a function that maps every event in a measurable space to a fixed point in time is deemed a stopping time according to the given filtration, since the occurrence of the event can be determined at the fixed point in time.
More concisely: For any measurable space Ω, preorder ι, filtration f on Ω indexed by ι, and i in ι, the constant function mapping every element of Ω to i is a stopping time with respect to f.
|
MeasureTheory.IsStoppingTime.measurableSet_eq
theorem MeasureTheory.IsStoppingTime.measurableSet_eq :
∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : LinearOrder ι] {f : MeasureTheory.Filtration ι m}
{τ : Ω → ι} [inst_1 : TopologicalSpace ι] [inst_2 : OrderTopology ι] [inst_3 : FirstCountableTopology ι],
MeasureTheory.IsStoppingTime f τ → ∀ (i : ι), MeasurableSet {ω | τ ω = i}
The theorem `MeasureTheory.IsStoppingTime.measurableSet_eq` states that for any types `Ω` and `ι`, any measurable space `m` on `Ω`, any linear order on `ι`, any filtration `f` of `m` over `ι`, any function `τ` from `Ω` to `ι`, and assuming that `ι` is a topological space with an order topology and a first countable topology, if `τ` is a stopping time with respect to the filtration `f`, then for every `i` in `ι`, the set of all `ω` in `Ω` such that `τ(ω)` equals `i` is a measurable set.
In more intuitive terms, this theorem asserts that under the given conditions, if `τ` describes a rule that determines when to stop a given process at any given time using the information we have at that time, then for every possible stopping time, the set of all outcomes that would cause us to stop at that time is a measurable set, i.e., a set to which we can meaningfully assign a probability.
More concisely: If `τ: Ω -> ι` is a stopping time with respect to filtration `f` on measurable space `(Ω, m)` over linear order `ι`, with `ι` being a topological space with an order topology and first countable topology, then for every `i` in `ι`, the set `{ω | τ(ω) = i}` is measurable.
|
Mathlib.Probability.Process.Stopping._auxLemma.5
theorem Mathlib.Probability.Process.Stopping._auxLemma.5 :
∀ {α : Type u} {s t : Set α} (x : α), (x ∈ s \ t) = (x ∈ s ∧ x ∉ t)
This theorem, referred to as `Mathlib.Probability.Process.Stopping._auxLemma.5`, states that for every type `α` and sets `s` and `t` of type `α`, an element `x` of type `α` is in the set difference `s \ t` if and only if `x` is in set `s` and `x` is not in set `t`. In simpler terms, it formalizes the basic set theory property where an element is in the difference of two sets if it belongs to the first set and does not belong to the second.
More concisely: For any type `α` and sets `s` and `t` of type `α`, an element `x` lies in the set difference `s \ t` if and only if it is in `s` but not in `t`.
|
MeasureTheory.IsStoppingTime.measurableSet_inter_eq_iff
theorem MeasureTheory.IsStoppingTime.measurableSet_inter_eq_iff :
∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
{τ : Ω → ι} (hτ : MeasureTheory.IsStoppingTime f τ) (s : Set Ω) (i : ι),
MeasurableSet (s ∩ {ω | τ ω = i}) ↔ MeasurableSet (s ∩ {ω | τ ω = i})
This theorem states that for any measure space `Ω`, any preordered index set `ι`, any filtration `f` on `Ω` indexed by `ι`, and any stopping time `τ` with respect to this filtration, the set `s` of elements in `Ω`, and an index `i` from `ι`, the intersection of `s` with the set of elements `ω` in `Ω` where `τ ω` equals `i` is measurable if and only if this intersection is measurable. Intuitively, this means that the measurability of the set of outcomes where the stopping time equals a specific time `i` and belong to a certain set `s` is not affected by the specifics of the stopping rule `τ`.
More concisely: For any measure space `Ω`, preordered index set `ι`, filtration `f` on `Ω` indexed by `ι`, and stopping time `τ` with respect to `f`, the set `{ω ∈ Ω | τ ω = i ∧ ω ∈ s}` is measurable if andωaso is, for all `i` in `ι` and set `s` in `Ω`.
|
MeasureTheory.Adapted.stoppedProcess
theorem MeasureTheory.Adapted.stoppedProcess :
∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : TopologicalSpace β]
[inst_1 : TopologicalSpace.PseudoMetrizableSpace β] [inst_2 : LinearOrder ι] [inst_3 : TopologicalSpace ι]
[inst_4 : SecondCountableTopology ι] [inst_5 : OrderTopology ι] [inst_6 : MeasurableSpace ι]
[inst_7 : BorelSpace ι] {f : MeasureTheory.Filtration ι m} {u : ι → Ω → β} {τ : Ω → ι}
[inst_8 : TopologicalSpace.MetrizableSpace ι],
MeasureTheory.Adapted f u →
(∀ (ω : Ω), Continuous fun i => u i ω) →
MeasureTheory.IsStoppingTime f τ → MeasureTheory.Adapted f (MeasureTheory.stoppedProcess u τ)
The theorem states that for a given set `Ω`, a topological space `β`, an order type `ι`, a measurable space `m`, a filtration `f` on `m`, a sequence of functions `u`, and a stopping time `τ`, if `u` is adapted to `f` and for every `ω` in `Ω`, the function `u` is continuous in `i`, then the stopped process of `u` with respect to `τ` is also adapted to `f`. In other words, if we have a process that is adapted to a filtration and has continuous paths, even when we stop this process at a certain stopping time, the resulting process is still adapted to the original filtration.
More concisely: If `u` is an adapted and continuously pathwise function on a measurable space `(Ω, m)` with respect to a filtration `f`, then the stopped process `u bekan τ` is also adapted to `f` for any stopping time `τ`.
|
MeasureTheory.IsStoppingTime.measurableSet_eq_of_countable_range
theorem MeasureTheory.IsStoppingTime.measurableSet_eq_of_countable_range :
∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : PartialOrder ι] {τ : Ω → ι}
{f : MeasureTheory.Filtration ι m},
MeasureTheory.IsStoppingTime f τ → (Set.range τ).Countable → ∀ (i : ι), MeasurableSet {ω | τ ω = i}
The theorem `MeasureTheory.IsStoppingTime.measurableSet_eq_of_countable_range` states that for any types `Ω` and `ι`, a measurable space `m` on `Ω`, a partial order on `ι`, a function `τ` from `Ω` to `ι`, and a filtration `f` on `m`, if `τ` is a stopping time with respect to the filtration `f` and if the range of `τ` is countable, then for every `i` in `ι`, the set of all `ω` in `Ω` such that `τ(ω) = i` is a measurable set with respect to the measurable space `m`.
In other words, if we have a stopping rule `τ` that can be decided using the information available at a given time, and this stopping rule only takes on countably many values, then the set of points in our space that stop at a given time `i` is a measurable set, which means it can be meaningfully assigned a measure (or "size") in our measure space.
More concisely: If `τ: Ω → ι` is a measurable stopping time with a countable range in a measurable space `(Ω, m)` and filtration `f`, then for all `i ∈ ι`, the set `{ω ∈ Ω | τ(ω) = i}` is measurable.
|
Mathlib.Probability.Process.Stopping._auxLemma.12
theorem Mathlib.Probability.Process.Stopping._auxLemma.12 :
∀ {α : Type u} [inst : Preorder α] (a : α), (a ≤ a) = True
This theorem, named `Mathlib.Probability.Process.Stopping._auxLemma.12`, states that for any type `α` in a Preorder (a mathematical structure where the relation is reflexive and transitive), any instance `a` of this type is less than or equal to itself. In other words, in any preorder, every element is less than or equal to itself, which is a property of reflexivity in preorders. The equality `(a ≤ a) = True` reflects this property.
More concisely: In any preorder, every element is less than or equal to itself (reflexivity property).
|
MeasureTheory.IsStoppingTime.measurableSpace_const
theorem MeasureTheory.IsStoppingTime.measurableSpace_const :
∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : Preorder ι] (f : MeasureTheory.Filtration ι m)
(i : ι), ⋯.measurableSpace = ↑f i
The theorem `MeasureTheory.IsStoppingTime.measurableSpace_const` states that for any measurable space `Ω`, type `ι` with a preorder instance, filtration `f` of `ι` on `Ω`, and any `ι` instance `i`, the associated σ-algebra or measurable space with a constant stopping time (where the stopping time is always the same value `i` for all elements of the underlying set `Ω`) is equal to the `i`-th space in the filtration `f`.
More concisely: For any measurable space `Ω` with a preorder instance, filtration `f` on `ι`, and `ι` instance `i`, the σ-algebra of the constant stopping time `i` equals the `i`-th space in `f`.
|
MeasureTheory.IsStoppingTime.measurableSet_lt_of_isLUB
theorem MeasureTheory.IsStoppingTime.measurableSet_lt_of_isLUB :
∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : LinearOrder ι] {f : MeasureTheory.Filtration ι m}
{τ : Ω → ι} [inst_1 : TopologicalSpace ι] [inst_2 : OrderTopology ι] [inst_3 : FirstCountableTopology ι],
MeasureTheory.IsStoppingTime f τ → ∀ (i : ι), IsLUB (Set.Iio i) i → MeasurableSet {ω | τ ω < i}
The theorem `MeasureTheory.IsStoppingTime.measurableSet_lt_of_isLUB` states that for every measurable space `Ω`, type `ι`, and a filtration `f` of a measure theory, if `τ` is a stopping time with respect to the filtration `f`, then for every type `ι` value `i` that is a least upper bound of the left-infinite right-open interval less than `i`, the set of all `ω` in `Ω` such that `τ ω` is less than `i` is a measurable set. This is under the assumptions that `ι` is an instance of a linear order, topological space, order topology, and first countable topology.
In simpler terms, if we have a stopping rule that can be determined with the information we have at a certain time point, then for any time point that is the smallest upper bound of all previous time points, the set of all outcomes where the stopping rule suggests we stop before this time point is a measurable set - a set that can be meaningfully utilized in the context of measure theory.
More concisely: If `τ` is a stopping time with respect to a filtration `f` in a measurable space `Ω` with a linear order `ι` having the properties of a topology and being first countable, then for each `i` in `ι` that is a least upper bound of the left-open intervals less than `i`, the set of all `ω` in `Ω` such that `τ ω` is less than `i` is measurable.
|
MeasureTheory.IsStoppingTime.measurableSet_le'
theorem MeasureTheory.IsStoppingTime.measurableSet_le' :
∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : LinearOrder ι] {f : MeasureTheory.Filtration ι m}
{τ : Ω → ι} (hτ : MeasureTheory.IsStoppingTime f τ) (i : ι), MeasurableSet {ω | τ ω ≤ i}
The theorem `MeasureTheory.IsStoppingTime.measurableSet_le'` states that for any types Ω and ι, a measurable space `m` on Ω, a linear order on ι, a filtration `f` of the measurable space, and a function `τ` from Ω to ι that is a stopping time with respect to the filtration `f`, for every `ι` instance `i`, the set of all `ω` in Ω such that `τ(ω)` is less than or equal to `i` is a measurable set in the measurable space. In other words, the set of outcomes where the stopping time is no later than a given time is a measurable set.
More concisely: For any measurable space $(Ω, m)$, linear order $(ι, ≤)$, filtration $(f\_t : t ∈ ι)$ on $Ω$, and stopping time $τ : Ω → ι$, the set $\{ω ∈ Ω : τ(ω) ≤ i\}$ is measurable for all $i ∈ ι$.
|
MeasureTheory.ProgMeasurable.stoppedProcess
theorem MeasureTheory.ProgMeasurable.stoppedProcess :
∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : LinearOrder ι]
[inst_1 : MeasurableSpace ι] [inst_2 : TopologicalSpace ι] [inst_3 : OrderTopology ι]
[inst_4 : SecondCountableTopology ι] [inst_5 : BorelSpace ι] [inst_6 : TopologicalSpace β] {u : ι → Ω → β}
{τ : Ω → ι} {f : MeasureTheory.Filtration ι m} [inst_7 : TopologicalSpace.MetrizableSpace ι],
MeasureTheory.ProgMeasurable f u →
MeasureTheory.IsStoppingTime f τ → MeasureTheory.ProgMeasurable f (MeasureTheory.stoppedProcess u τ)
The theorem `MeasureTheory.ProgMeasurable.stoppedProcess` states that for any types `Ω`, `β`, and `ι`, for a given measurable space `m` on `Ω`, a linear order on `ι`, measurable space on `ι`, topological space on `ι`, order topology on `ι`, second countable topology on `ι`, Borel space on `ι`, topological space on `β`, a function `u` mapping `ι` and `Ω` to `β`, a function `τ` mapping `Ω` to `ι`, and a filtration `f` on `m` with `ι` as the index set, and assuming `ι` is a metrizable space, if the function `u` is progressively measurable with respect to the filtration `f`, and if the function `τ` is a stopping time with respect to the same filtration `f`, then the stopped process of `u` with respect to `τ` is also progressively measurable with respect to the filtration `f`. In other words, stopping a progressively measurable process at a stopping time yields another progressively measurable process.
More concisely: Given a measurable space, a linear order on a metrizable index set, a filtration, a progressively measurable function, and a stopping time, the stopped process of the function at the stopping time is also progressively measurable with respect to the filtration.
|
MeasureTheory.IsStoppingTime.measurableSet_le
theorem MeasureTheory.IsStoppingTime.measurableSet_le :
∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
{τ : Ω → ι}, MeasureTheory.IsStoppingTime f τ → ∀ (i : ι), MeasurableSet {ω | τ ω ≤ i}
This theorem states that for any types `Ω` and `ι`, any measurable space `m` over `Ω`, any preorder on `ι`, any filtration `f` of `m` over `ι`, and any function `τ` from `Ω` to `ι`, if `τ` is a stopping time with respect to `f`, then for every `ι`, the set of all `ω` in `Ω` such that `τ ω` is less than or equal to `i` is a measurable set in the ambient measure space. In other words, the preimage of any set `{j | j ≤ i}` along `τ` is measurable with respect to the filtration `f` at time `i`, underscoring the intuitive understanding of a stopping time as a rule that can be determined with the information available at time `i`.
More concisely: For any measurable space `(Ω, m)`, preorder `≤` on `ι`, filtration `f` of `m` over `ι`, and function `τ: Ω → ι`, if `τ` is a stopping time with respect to `f`, then for every `i ∈ ι`, the set `{ω ∈ Ω | τ(ω) ≤ i}` is measurable in `(Ω, m)` with respect to `f` at time `i`.
|
MeasureTheory.IsStoppingTime.measurableSet_min_iff
theorem MeasureTheory.IsStoppingTime.measurableSet_min_iff :
∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : LinearOrder ι] {f : MeasureTheory.Filtration ι m}
{τ π : Ω → ι} (hτ : MeasureTheory.IsStoppingTime f τ) (hπ : MeasureTheory.IsStoppingTime f π) (s : Set Ω),
MeasurableSet s ↔ MeasurableSet s ∧ MeasurableSet s
The theorem `MeasureTheory.IsStoppingTime.measurableSet_min_iff` states that for any types `Ω` and `ι`, a `MeasurableSpace Ω` named `m`, a `LinearOrder` on `ι`, a filtration `f` of type `MeasureTheory.Filtration ι m`, and two functions `τ` and `π` from `Ω` to `ι` such that both `τ` and `π` are stopping times with respect to the filtration `f`, and any set `s` of type `Set Ω`, `s` is a measurable set if and only if both `s` and `s` are measurable sets. Clearly, this statement is a tautology as it states that `s` is measurable if and only if `s` is measurable.
More concisely: For any measurable space `(Ω, m)`, filtration `f`, and stopping times `τ` and `π` on `Ω` with respect to `f`, if two sets `s` are measurable with respect to `(Ω, m)` and `f`, then `s` and `τ^{-1}[min τ(s)] = π^{-1}[min π(s)]` have the same measurability.
|
MeasureTheory.IsStoppingTime.measurableSpace_mono
theorem MeasureTheory.IsStoppingTime.measurableSpace_mono :
∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
{τ π : Ω → ι} (hτ : MeasureTheory.IsStoppingTime f τ) (hπ : MeasureTheory.IsStoppingTime f π),
τ ≤ π → hτ.measurableSpace ≤ hπ.measurableSpace
The theorem `MeasureTheory.IsStoppingTime.measurableSpace_mono` states that for any types `Ω` and `ι`, a measurable space `m` over `Ω`, a preorder on `ι`, a filtration `f` of `m`, and two stopping times `τ` and `π` with respect to `f`, if `τ` is less than or equal to `π`, then the σ-algebra associated with stopping time `τ` is a sub-σ-algebra of the σ-algebra associated with stopping time `π`. Intuitively, this means that if one stopping rule `τ` stops no later than another stopping rule `π`, then any event measurable with respect to the earlier stopping rule `τ` is also measurable with respect to the later stopping rule `π`.
More concisely: If `(Ω, m)` is a measurable space, `f` is a filtration on `m`, `τ` and `π` are stopping times with respect to `f` such that `τ ≤ π`, then the σ-algebra generated by `τ` is a sub-σ-algebra of the σ-algebra generated by `π`.
|
MeasureTheory.Adapted.stoppedProcess_of_discrete
theorem MeasureTheory.Adapted.stoppedProcess_of_discrete :
∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : TopologicalSpace β]
[inst_1 : TopologicalSpace.PseudoMetrizableSpace β] [inst_2 : LinearOrder ι] [inst_3 : TopologicalSpace ι]
[inst_4 : SecondCountableTopology ι] [inst_5 : OrderTopology ι] [inst_6 : MeasurableSpace ι]
[inst_7 : BorelSpace ι] {f : MeasureTheory.Filtration ι m} {u : ι → Ω → β} {τ : Ω → ι}
[inst_8 : DiscreteTopology ι],
MeasureTheory.Adapted f u →
MeasureTheory.IsStoppingTime f τ → MeasureTheory.Adapted f (MeasureTheory.stoppedProcess u τ)
This theorem states that if the index order has a discrete topology, then the stopped process of an adapted process is also adapted. Here, an adapted process is a sequence of functions `u` that is measurable with respect to a given filtration `f` at each time `i`. The stopped process of `u` with respect to a stopping time `τ` is defined as `u i ω` if `i ≤ τ ω`, and `u (τ ω) ω` otherwise. The stopping time `τ` is a rule that, at each time `i`, determines whether to stop based on the information available at that time. The theorem asserts that if `u` is adapted and `τ` is a stopping time with respect to `f`, then the stopped process of `u` with respect to `τ` is also adapted to `f`, provided that the index order is equipped with a discrete topology.
More concisely: If `u` is an adapted process with respect to filtration `f` and `τ` is a stopping time with respect to `f`, then the stopped process of `u` with respect to `τ` is also an adapted process with respect to `f`, given that the index order has a discrete topology.
|
Mathlib.Probability.Process.Stopping._auxLemma.18
theorem Mathlib.Probability.Process.Stopping._auxLemma.18 : ∀ {α : Type u} (s : Set α) (x : α), (x ∈ sᶜ) = (x ∉ s) := by
sorry
This theorem, named `Mathlib.Probability.Process.Stopping._auxLemma.18`, states that for any type `α`, any set `s` of type `α`, and any element `x` of type `α`, the statement that `x` is in the complement of `s` (denoted as `sᶜ`) is equivalent to the statement that `x` is not in `s` (denoted as `x ∉ s`). In other words, an element belongs to the complement of a set if and only if it does not belong to the original set.
More concisely: The complement of a set is the set of all elements not in the original set.
|
MeasureTheory.IsStoppingTime.piecewise_of_le
theorem MeasureTheory.IsStoppingTime.piecewise_of_le :
∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : Preorder ι] {𝒢 : MeasureTheory.Filtration ι m}
{τ η : Ω → ι} {i : ι} {s : Set Ω} [inst_1 : DecidablePred fun x => x ∈ s],
MeasureTheory.IsStoppingTime 𝒢 τ →
MeasureTheory.IsStoppingTime 𝒢 η →
(∀ (ω : Ω), i ≤ τ ω) →
(∀ (ω : Ω), i ≤ η ω) → MeasurableSet s → MeasureTheory.IsStoppingTime 𝒢 (s.piecewise τ η)
This theorem states that given two stopping times `τ` and `η`, which are both bounded below, the piecewise function (`Set.piecewise s τ η`) created from them is also a stopping time with respect to the same filtration. Here, a stopping time describes a rule for stopping an experiment or observation based on the information available at a given time. The theorem requires the set `s` to be measurable, and it uses `DecidablePred` to ensure that whether an element is in the set `s` can be decided. The piecewise function takes the value of `τ` for elements that are in the set `s` and `η` otherwise.
More concisely: Given two bounded-below stopping times `τ` and `η` and a measurable set `s` with `DecidablePred s`, the piecewise function created from `τ` and `η` on `s` is also a stopping time.
|
MeasureTheory.IsStoppingTime.measurableSet
theorem MeasureTheory.IsStoppingTime.measurableSet :
∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
{τ : Ω → ι} (hτ : MeasureTheory.IsStoppingTime f τ) (s : Set Ω),
MeasurableSet s ↔ ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ i})
This theorem states that for any given types `Ω` and `ι`, and any given measurable space `m` on `Ω`, that is, a structure that allows us to treat subsets of `Ω` as "measurable" or not, and for any preorder (a relation that is reflexive and transitive) on `ι`, and any filtration `f` of `m` (a family of sigma algebras indexed by `ι`), and any function `τ` from `Ω` to `ι`, if `τ` is a stopping time with respect to `f`, and `s` is a set of `Ω`, then `s` is a measurable set if and only if the intersection of `s` with the set of all `ω` such that `τ ω` is less than or equal to `i` is a measurable set for all `i` in `ι`. In other words, a set is measurable if and only if its intersection with all sets defined by the stopping time being less than or equal to a certain time is measurable.
More concisely: A set is measurable with respect to a filtration and a stopping time if and only if the intersection of the set with each level set defined by the stopping time is measurable.
|
MeasureTheory.IsStoppingTime.measurableSet_eq'
theorem MeasureTheory.IsStoppingTime.measurableSet_eq' :
∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : LinearOrder ι] {f : MeasureTheory.Filtration ι m}
{τ : Ω → ι} [inst_1 : TopologicalSpace ι] [inst_2 : OrderTopology ι] [inst_3 : FirstCountableTopology ι]
(hτ : MeasureTheory.IsStoppingTime f τ) (i : ι), MeasurableSet {ω | τ ω = i}
The theorem `MeasureTheory.IsStoppingTime.measurableSet_eq'` asserts that for any types `Ω` and `ι`, given a measurable space `m` over `Ω`, a linear order on `ι`, a filtration `f` over the measurable space indexed by `ι`, a function `τ` mapping `Ω` to `ι`, and provided that `ι` has a topological space structure, an order topology, and is first countable, if `τ` is a stopping time with respect to the filtration `f`, then for any `i` in `ι`, the set of `ω` in `Ω` such that `τ(ω)` equals `i` is a measurable set.
This means that, intuitively, if `τ` is a stopping time (a rule that determines when to stop a process, which can be determined with the information available at any given time), then the set of points in the space where the stopping time equals a specific time `i` is a measurable set - it can be assigned a 'size' or 'measure' in a meaningful way.
More concisely: For any measurable space `(Ω, m)`, linear order `ι`, filtration `f` over `(Ω, m)` indexed by `ι`, and a stopping time `τ : Ω → ι`, if `ι` is a first countable topological space with an order topology, then for every `i` in `ι`, the set `{ ω : Ω | τ(ω) = i }` is measurable.
|
MeasureTheory.IsStoppingTime.min
theorem MeasureTheory.IsStoppingTime.min :
∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : LinearOrder ι] {f : MeasureTheory.Filtration ι m}
{τ π : Ω → ι},
MeasureTheory.IsStoppingTime f τ →
MeasureTheory.IsStoppingTime f π → MeasureTheory.IsStoppingTime f fun ω => min (τ ω) (π ω)
This theorem states that for any two stopping times `τ` and `π` with respect to a given filtration `f`, the stopping time function that takes the minimum of `τ ω` and `π ω` for each ω is also a stopping time. In more intuitive terms, given two stopping rules described by `τ` and `π`, the rule that stops at the earlier of the two times is also a valid stopping rule. This result applies in any measurable space `Ω` with a linear order on the index set `ι`.
More concisely: Given stopping times `τ` and `π` in a measurable space with a linear order, the minimum `τ ∧π` is also a stopping time.
|
MeasureTheory.stoppedValue_eq_of_mem_finset
theorem MeasureTheory.stoppedValue_eq_of_mem_finset :
∀ {Ω : Type u_1} {ι : Type u_3} {τ : Ω → ι} {E : Type u_4} {u : ι → Ω → E} [inst : AddCommMonoid E] {s : Finset ι},
(∀ (ω : Ω), τ ω ∈ s) → MeasureTheory.stoppedValue u τ = s.sum fun i => {ω | τ ω = i}.indicator (u i)
This theorem states that for all types `Ω`, `ι`, and `E`, a function `τ` from `Ω` to `ι`, and a map `u` from `ι` and `Ω` to `E`, given an additive commutative monoid structure on `E`, and a finite set `s` of `ι`, if for every element `ω` in `Ω`, `τ ω` is in `s`, then the stopped value of the map `u` with respect to the stopping time `τ` is equal to the sum over `s` of the set indicator function applied to the set of elements `ω` for which `τ ω` equals `i`, and the function `u i`. In mathematical terms, $\text{stoppedValue}\ u\ \tau = \sum_{i \in s} \text{Set.indicator}\ \{w | \tau w = i\}\ (u\ i)$.
More concisely: For a commutative additive monoid `E`, given a function `τ:` `Ω` → `ι`, a map `u:` `ι` × `Ω` → `E`, and a finite set `s` ⊆ `ι`, if `τω` ∈ `s` for all `ω` ∈ `Ω`, then `stoppedValue` `u` `τ` = ∑(``i`:` `s`) Set.indicator {`ω` | `τ`(`ω`) = `i`} `u` `i`.
|