MeasureTheory.Adapted.progMeasurable_of_continuous
theorem MeasureTheory.Adapted.progMeasurable_of_continuous :
∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : TopologicalSpace β]
[inst_1 : Preorder ι] {u : ι → Ω → β} {f : MeasureTheory.Filtration ι m} [inst_2 : TopologicalSpace ι]
[inst_3 : TopologicalSpace.MetrizableSpace ι] [inst_4 : SecondCountableTopology ι] [inst_5 : MeasurableSpace ι]
[inst_6 : OpensMeasurableSpace ι] [inst_7 : TopologicalSpace.PseudoMetrizableSpace β],
MeasureTheory.Adapted f u → (∀ (ω : Ω), Continuous fun i => u i ω) → MeasureTheory.ProgMeasurable f u
The theorem `MeasureTheory.Adapted.progMeasurable_of_continuous` states that for any types `Ω`, `β`, `ι`; a measurable space `m` over `Ω`; a topological space over `β`; a preorder on `ι`; a sequence of functions `u` from `ι` to `Ω → β`; a filtration `f` on `m`; provided that the space `ι` is topological, metrizable, has a second countable topology, is measurable, has an open measurable space, and `β` is pseudo-metrizable: if the sequence `u` is adapted to the filtration `f` (i.e., for all `i`, `u i` is `f i`-measurable), and for every `ω` in `Ω`, the function `u i ω` is continuous, then `u` is progressively measurable with respect to the filtration `f` (i.e., for every `i` in `ι`, the function `u` up to time `i` is measurable). This theorem connects the concepts of adapted processes, continuity, and progressive measurability in the framework of measure theory.
More concisely: If `Ω`, `β`, `ι` are suitable types, `m` is a measurable space over `Ω`, `β` is pseudo-metrizable, `ι` is a second countable, measurable topological space, `u: ι → Ω → β` is a sequence of continuous, `f` is a filtration on `m`, and `u` is adapted to `f`, then `u` is progressively measurable with respect to `f`.
|
MeasureTheory.ProgMeasurable.adapted
theorem MeasureTheory.ProgMeasurable.adapted :
∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : TopologicalSpace β]
[inst_1 : Preorder ι] {u : ι → Ω → β} {f : MeasureTheory.Filtration ι m} [inst_2 : MeasurableSpace ι],
MeasureTheory.ProgMeasurable f u → MeasureTheory.Adapted f u
The theorem `MeasureTheory.ProgMeasurable.adapted` states that for any types `Ω`, `β`, and `ι`, given a measurable space `Ω`, a topological space `β`, and a preorder `ι`, if `u` is a function from `ι` to a function from `Ω` to `β` and `f` is a filtration on `m`, then if `u` is progressively measurable with respect to `f`, it follows that `u` is adapted to `f`. Here, being progressively measurable means `u` is measurable with respect to the increasing sequence of sigma-algebras defined by `f`, and being adapted to `f` means each function `u i` in the sequence is strongly measurable with respect to `f i`.
More concisely: Given a measurable space `(Ω, Σ)`, a topological space `(β, τ)`, a preorder `(ι, ⋈)`, a filtration `(f : Filtration Σ ι)`, and a progressively measurable function `u : ι → Ω → β`, then `u` is adapted to `f`.
|
MeasureTheory.Adapted.progMeasurable_of_discrete
theorem MeasureTheory.Adapted.progMeasurable_of_discrete :
∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : TopologicalSpace β]
[inst_1 : Preorder ι] {u : ι → Ω → β} {f : MeasureTheory.Filtration ι m} [inst_2 : TopologicalSpace ι]
[inst_3 : DiscreteTopology ι] [inst_4 : SecondCountableTopology ι] [inst_5 : MeasurableSpace ι]
[inst_6 : OpensMeasurableSpace ι] [inst_7 : TopologicalSpace.PseudoMetrizableSpace β],
MeasureTheory.Adapted f u → MeasureTheory.ProgMeasurable f u
This theorem states that for filtrations indexed by a discrete order, the properties of being `Adapted` and `ProgMeasurable` are equivalent, in the direction that if a sequence of functions `u` is `Adapted` to a filtration `f`, then it is `ProgMeasurable` with respect to `f`. Here, a sequence of functions `u` is said to be `Adapted` to a filtration `f` if for all `i`, `u i` is `f i`-measurable. The term `ProgMeasurable` refers to a stronger property than `Adapted`. The reverse direction, that `ProgMeasurable` implies `Adapted`, is true more generally and is provided by the lemma `ProgMeasurable.adapted`. This theorem requires a number of conditions on the types, including that the index set has a topology that is both discrete and second countable, and the target space of the functions is a pseudo-metrizable topological space.
More concisely: For filtrations indexed by a discrete and second countable index set, a sequence of functions is Adapted if and only if it is Progressively Measurable.
|
MeasureTheory.Adapted.neg
theorem MeasureTheory.Adapted.neg :
∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : TopologicalSpace β]
[inst_1 : Preorder ι] {u : ι → Ω → β} {f : MeasureTheory.Filtration ι m} [inst_2 : AddGroup β]
[inst_3 : TopologicalAddGroup β], MeasureTheory.Adapted f u → MeasureTheory.Adapted f (-u)
The theorem `MeasureTheory.Adapted.neg` states that for any type `Ω`, any topological space `β`, any preorder `ι`, and any measurable space `m`, if a sequence of functions `u` (from `ι` to `β`) is adapted to a filtration `f` (from `ι` to `m`), then the negative of that sequence of functions `-u` is also adapted to the same filtration `f`. Here, `β` is assumed to be an additive group and a topological additive group.
More concisely: If `u: ι → β` is an adapted sequence of functions to filtration `f: ι → m` over measurable space `(Ω, m)`, then the sequence `-u` is also adapted to filtration `f`.
|