MeasureTheory.le_hitting
theorem MeasureTheory.le_hitting :
∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : ConditionallyCompleteLinearOrder ι] {u : ι → Ω → β}
{s : Set β} {n m : ι}, n ≤ m → ∀ (ω : Ω), n ≤ MeasureTheory.hitting u s n m ω
The theorem `MeasureTheory.le_hitting` states that for any types `Ω`, `β`, and `ι`, and given a conditionally complete linear order on `ι`, a function `u` from `ι` and `Ω` to `β`, a set `s` of elements of type `β`, and two elements `n` and `m` of type `ι` such that `n` is less than or equal to `m`, then for any element `ω` of type `Ω`, `n` is less than or equal to the hitting measure of `u`, `s`, `n`, `m`, and `ω`. In mathematical terms, this theorem asserts that the hitting measure of a function on a set is a non-decreasing function of its input parameters.
More concisely: For any conditionally complete linear order `ι`, function `u` from `ι × Ω` to `β`, set `s ⊆ β`, and elements `n ≤ m` of `ι`, if `ω` is an element of `Ω`, then `u(n, ω) ≤ u(m, ω)` holds in the hitting measure.
|
MeasureTheory.hitting_le
theorem MeasureTheory.hitting_le :
∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : ConditionallyCompleteLinearOrder ι] {u : ι → Ω → β}
{s : Set β} {n m : ι} (ω : Ω), MeasureTheory.hitting u s n m ω ≤ m
This theorem, known as `MeasureTheory.hitting_le`, states that for any given types `Ω`, `β`, and `ι`, where `ι` is a conditionally complete linear order, and for any function `u` mapping `ι` and `Ω` to `β`, any set `s` of type `β`, and any values `n` and `m` of type `ι`, and an element `ω` of type `Ω`, the "hitting" measure of `u`, `s`, `n`, `m`, and `ω` is less than or equal to `m`. Here, "hitting" is a concept from measure theory representing a certain kind of interaction between the function `u` and the set `s`.
More concisely: For any type `Ω`, conditionally complete linear order `ι`, function `u` from `ι × Ω` to `β`, set `s` of type `β`, and elements `n` and `m` of type `ι` and `ω` of type `Ω`, the measure of the set `{i ∈ i | u(i, ω) ∈ s}`, denoted by `# {i | u(i, ω) ∈ s}`, is less than or equal to `m`.
|
MeasureTheory.isStoppingTime_hitting_isStoppingTime
theorem MeasureTheory.isStoppingTime_hitting_isStoppingTime :
∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : ConditionallyCompleteLinearOrder ι]
[inst_1 : IsWellOrder ι fun x x_1 => x < x_1] [inst_2 : Countable ι] [inst_3 : TopologicalSpace ι]
[inst_4 : OrderTopology ι] [inst_5 : FirstCountableTopology ι] [inst_6 : TopologicalSpace β]
[inst_7 : TopologicalSpace.PseudoMetrizableSpace β] [inst_8 : MeasurableSpace β] [inst_9 : BorelSpace β]
{f : MeasureTheory.Filtration ι m} {u : ι → Ω → β} {τ : Ω → ι},
MeasureTheory.IsStoppingTime f τ →
∀ {N : ι},
(∀ (x : Ω), τ x ≤ N) →
∀ {s : Set β},
MeasurableSet s →
MeasureTheory.Adapted f u →
MeasureTheory.IsStoppingTime f fun x => MeasureTheory.hitting u s (τ x) N x
The theorem `MeasureTheory.isStoppingTime_hitting_isStoppingTime` states that for a measure space `Ω`, a type `β`, an indexing type `ι`, and under certain topological conditions on `β` and `ι`, given a filtration `f` on `ι`, a function `u` from `ι` to `Ω` to `β`, and a stopping time `τ`, if `τ` is a stopping time with respect to `f`, then for any index `N` such that `τ` of `x` is less than or equal to `N` for all `x` in `Ω`, and for any measurable set `s` of type `β`, if the function `u` is adapted to the filtration `f`, then the hitting time of the function `u` with respect to the set `s` starting at the stopping time `τ` is also a stopping time with respect to `f`, where the hitting time of the process `u` with respect to a set `s` and a starting time `τ` is the earliest time at which the process `u` enters the set `s` after time `τ`.
More concisely: Given a measure space, a filtration, a function from the space to another type, and a stopping time, if the function is adapted to the filtration and the hitting time of the function with respect to a measurable set starting at the stopping time is defined, then it is also a stopping time with respect to the filtration.
|
MeasureTheory.hitting_isStoppingTime
theorem MeasureTheory.hitting_isStoppingTime :
∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : ConditionallyCompleteLinearOrder ι]
[inst_1 : IsWellOrder ι fun x x_1 => x < x_1] [inst_2 : Countable ι] [inst_3 : TopologicalSpace β]
[inst_4 : TopologicalSpace.PseudoMetrizableSpace β] [inst_5 : MeasurableSpace β] [inst_6 : BorelSpace β]
{f : MeasureTheory.Filtration ι m} {u : ι → Ω → β} {s : Set β} {n n' : ι},
MeasureTheory.Adapted f u → MeasurableSet s → MeasureTheory.IsStoppingTime f (MeasureTheory.hitting u s n n')
The theorem `MeasureTheory.hitting_isStoppingTime` states that for any types `Ω`, `β`, and `ι`, with `Ω` being a measurable space, `β` being a topological, pseudometrizable, measurable and Borel space, and `ι` being a conditionally complete linear order which is well-ordered and countable, given a filtration `f` of type `MeasureTheory.Filtration ι m`, a sequence of functions `u` from `ι` to `Ω → β`, a set `s` of type `Set β`, and two elements `n` and `n'` of type `ι`, if the sequence of functions `u` is adapted to the filtration `f` and the set `s` is a measurable set, then the hitting time represented by `MeasureTheory.hitting u s n n'` is a stopping time with respect to the filtration `f`.
In more intuitive words, this theorem says that a certain kind of 'hitting time' - a time at which a certain event first occurs - is a 'stopping time' - a time at which a certain process can be stopped, given that the process observed is adapted to the filtration and the event set is measurable. This means we can determine whether to stop the process at time `i` using the information we have at time `i`, where `i` is a certain kind of linear order.
More concisely: Given a measurable space Ω, a topological, pseudometrizable, measurable and Borel space β, a countable, well-ordered and conditionally complete linear order ι, a filtration f, an adapted sequence of functions u from ι to Ω → β, and a measurable set s, the hitting time MeasureTheory.hitting u s n is a stopping time with respect to the filtration f.
|
MeasureTheory.hitting_of_lt
theorem MeasureTheory.hitting_of_lt :
∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : ConditionallyCompleteLinearOrder ι] {u : ι → Ω → β}
{s : Set β} {n : ι} {ω : Ω} {m : ι}, m < n → MeasureTheory.hitting u s n m ω = m
This theorem, `MeasureTheory.hitting_of_lt`, states that for any types `Ω`, `β`, and `ι`, where `ι` is a conditionally complete linear order, and for any function `u` mapping ordered pairs of `ι` and `Ω` to `β`, any set `s` of type `β`, any elements `n` and `m` of type `ι`, and any element `ω` of type `Ω`, if `m` is strictly less than `n`, then the hitting measure of `u`, `s`, `n`, `m`, and `ω` equals `m`. Here, "hitting measure" is a concept from measure theory, and `MeasureTheory.hitting` is a function or process related to this concept.
More concisely: For any type `Ω`, `β`, and conditionally complete linear order `ι`, if `u` is a function mapping ordered pairs of `ι` and `Ω` to `β`, `s` is a set of type `β`, `ω` is an element of type `Ω`, and `m` and `n` are elements of type `ι` with `m` strictly less than `n`, then the hitting measure of `u`, `s`, `n`, `m`, and `ω` equals `m`.
|
MeasureTheory.stoppedValue_hitting_mem
theorem MeasureTheory.stoppedValue_hitting_mem :
∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : ConditionallyCompleteLinearOrder ι]
[inst_1 : IsWellOrder ι fun x x_1 => x < x_1] {u : ι → Ω → β} {s : Set β} {n m : ι} {ω : Ω},
(∃ j ∈ Set.Icc n m, u j ω ∈ s) → MeasureTheory.stoppedValue u (MeasureTheory.hitting u s n m) ω ∈ s
This theorem states that for any types `Ω`, `β`, and `ι`, given a conditionally complete linear order on `ι`, a well-order on `ι` defined by a less-than relation, a mapping `u` from `ι` and `Ω` to `β`, a set `s` of type `β`, and elements `n`, `m` of `ι`, and `ω` of `Ω`, if there exists an element `j` in the closed interval from `n` to `m` such that `u j ω` belongs to the set `s`, then the stopped value of the mapping `u` with respect to the hitting time of `u`, `s`, `n`, and `m`, evaluated at `ω`, is also in the set `s`. In other words, if `u j ω` for some `j` in `[n, m]` is in `s`, then the stopped value of `u` at the time `u` first hits `s` between `n` and `m` is also in `s`.
More concisely: Given a conditionally complete linear order on `ι`, a well-order on `ι`, a mapping `u` from `ι` and `Ω` to `β`, a set `s` of type `β`, and elements `n`, `m` of `ι` and `ω` of `Ω`, if there exists `j` in `[n, m]` such that `u j ω` is in `s`, then the stopped value of `u` at the hitting time of `s` between `n` and `m` is also in `s`.
|