Locally integrable, class D, class DL #
def
ProbabilityTheory.HasLocallyIntegrableSup
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[NormedAddCommGroup E]
{mΩ : MeasurableSpace Ω}
[LinearOrder ι]
[OrderBot ι]
[TopologicalSpace ι]
[OrderTopology ι]
(X : ι → Ω → E)
(𝓕 : MeasureTheory.Filtration ι mΩ)
(P : MeasureTheory.Measure Ω := by volume_tac)
:
A stochastic process has locally integrable supremum if it satisfies locally the property that
for all t, the random variable ω ↦ sup_{s ≤ t} ‖X s ω‖ is integrable.
Equations
- One or more equations did not get rendered due to their size.
Instances For
structure
ProbabilityTheory.ClassD
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[NormedAddCommGroup E]
{mΩ : MeasurableSpace Ω}
[Preorder ι]
[Nonempty ι]
(X : ι → Ω → E)
(𝓕 : MeasureTheory.Filtration ι mΩ)
(P : MeasureTheory.Measure Ω)
:
A stochastic process $(X_t)$ is of class D (or in the Doob-Meyer class) if it is adapted and the set $\{X_\tau \mid \tau \text{ is a finite stopping time}\}$ is uniformly integrable.
- adapted : MeasureTheory.Adapted 𝓕 X
- uniformIntegrable : MeasureTheory.UniformIntegrable (fun (τ : ↑{T : Ω → WithTop ι | MeasureTheory.IsStoppingTime 𝓕 T ∧ ∀ (ω : Ω), T ω ≠ ⊤}) => MeasureTheory.stoppedValue X ↑τ) 1 P
Instances For
structure
ProbabilityTheory.ClassDL
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[NormedAddCommGroup E]
{mΩ : MeasurableSpace Ω}
[Preorder ι]
[Nonempty ι]
(X : ι → Ω → E)
(𝓕 : MeasureTheory.Filtration ι mΩ)
(P : MeasureTheory.Measure Ω)
:
A stochastic process $(X_t)$ is of class DL if it is adapted and for all $t$, the set $\{X_\tau \mid \tau \text{ is a stopping time with } \tau \le t\}$ is uniformly integrable.
- adapted : MeasureTheory.Adapted 𝓕 X
- uniformIntegrable (t : ι) : MeasureTheory.UniformIntegrable (fun (τ : ↑{T : Ω → WithTop ι | MeasureTheory.IsStoppingTime 𝓕 T ∧ ∀ (ω : Ω), T ω ≤ ↑t}) => MeasureTheory.stoppedValue X ↑τ) 1 P
Instances For
theorem
ProbabilityTheory.ClassD.classDL
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[NormedAddCommGroup E]
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[Preorder ι]
[Nonempty ι]
{𝓕 : MeasureTheory.Filtration ι mΩ}
{X : ι → Ω → E}
(hX : ClassD X 𝓕 P)
:
ClassDL X 𝓕 P
theorem
MeasureTheory.Submartingale.classDL
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[NormedAddCommGroup E]
{mΩ : MeasurableSpace Ω}
{P : Measure Ω}
{X : ι → Ω → E}
[NormedSpace ℝ E]
[CompleteSpace E]
[PartialOrder ι]
[Nonempty ι]
{𝓕 : Filtration ι mΩ}
[TopologicalSpace ι]
[PartialOrder E]
[OrderClosedTopology E]
[IsOrderedAddMonoid E]
[IsOrderedModule ℝ E]
(hX1 : Submartingale X 𝓕 P)
(hX2 : ∀ (ω : Ω), Function.RightContinuous fun (x : ι) => X x ω)
(hX3 : 0 ≤ X)
:
theorem
MeasureTheory.Submartingale.classD_iff_uniformIntegrable
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[NormedAddCommGroup E]
{mΩ : MeasurableSpace Ω}
{P : Measure Ω}
{X : ι → Ω → E}
[NormedSpace ℝ E]
[CompleteSpace E]
[PartialOrder ι]
[Nonempty ι]
{𝓕 : Filtration ι mΩ}
[TopologicalSpace ι]
[PartialOrder E]
[OrderClosedTopology E]
[IsOrderedAddMonoid E]
[IsOrderedModule ℝ E]
(hX1 : Submartingale X 𝓕 P)
(hX2 : ∀ (ω : Ω), Function.RightContinuous fun (x : ι) => X x ω)
(hX3 : 0 ≤ X)
:
theorem
MeasureTheory.Martingale.classDL
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[NormedAddCommGroup E]
{mΩ : MeasurableSpace Ω}
{P : Measure Ω}
{X : ι → Ω → E}
[NormedSpace ℝ E]
[CompleteSpace E]
[PartialOrder ι]
[Nonempty ι]
{𝓕 : Filtration ι mΩ}
[TopologicalSpace ι]
(hX1 : Martingale X 𝓕 P)
(hX2 : ∀ (ω : Ω), Function.RightContinuous fun (x : ι) => X x ω)
:
theorem
MeasureTheory.Martingale.classD_iff_uniformIntegrable
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[NormedAddCommGroup E]
{mΩ : MeasurableSpace Ω}
{P : Measure Ω}
{X : ι → Ω → E}
[NormedSpace ℝ E]
[CompleteSpace E]
[PartialOrder ι]
[Nonempty ι]
{𝓕 : Filtration ι mΩ}
[TopologicalSpace ι]
(hX1 : Martingale X 𝓕 P)
(hX2 : ∀ (ω : Ω), Function.RightContinuous fun (x : ι) => X x ω)
:
theorem
ProbabilityTheory.isStable_hasLocallyIntegrableSup
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[NormedAddCommGroup E]
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[LinearOrder ι]
{𝓕 : MeasureTheory.Filtration ι mΩ}
[OrderBot ι]
[TopologicalSpace ι]
[OrderTopology ι]
:
IsStable 𝓕 fun (x : ι → Ω → E) => HasLocallyIntegrableSup x 𝓕 P
theorem
ProbabilityTheory.isStable_classD
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[NormedAddCommGroup E]
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[LinearOrder ι]
{𝓕 : MeasureTheory.Filtration ι mΩ}
[OrderBot ι]
:
theorem
ProbabilityTheory.isStable_classDL
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[NormedAddCommGroup E]
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[LinearOrder ι]
{𝓕 : MeasureTheory.Filtration ι mΩ}
[OrderBot ι]
:
theorem
MeasureTheory.Integrable.classDL
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[NormedAddCommGroup E]
{mΩ : MeasurableSpace Ω}
{P : Measure Ω}
{X : ι → Ω → E}
[LinearOrder ι]
{𝓕 : Filtration ι mΩ}
[Nonempty ι]
(hX : ∀ (t : ι), Integrable (fun (ω : Ω) => ⨆ (s : ι), ⨆ (_ : s ≤ t), ‖X t ω‖ₑ) P)
:
theorem
ProbabilityTheory.HasLocallyIntegrableSup.locally_classDL
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[NormedAddCommGroup E]
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X : ι → Ω → E}
[LinearOrder ι]
{𝓕 : MeasureTheory.Filtration ι mΩ}
[OrderBot ι]
[TopologicalSpace ι]
[OrderTopology ι]
(hX1 : HasLocallyIntegrableSup X 𝓕 P)
(hX2 : MeasureTheory.Adapted 𝓕 X)
(h𝓕 : 𝓕.IsRightContinuous)
:
theorem
ProbabilityTheory.ClassDL.locally_classD
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[NormedAddCommGroup E]
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X : ι → Ω → E}
[LinearOrder ι]
{𝓕 : MeasureTheory.Filtration ι mΩ}
[OrderBot ι]
[TopologicalSpace ι]
[OrderTopology ι]
(hX : ClassDL X 𝓕 P)
:
theorem
ProbabilityTheory.locally_classD_of_locally_classDL
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[NormedAddCommGroup E]
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X : ι → Ω → E}
[LinearOrder ι]
{𝓕 : MeasureTheory.Filtration ι mΩ}
[OrderBot ι]
[TopologicalSpace ι]
[OrderTopology ι]
(hX : Locally (fun (x : ι → Ω → E) => ClassDL x 𝓕 P) 𝓕 X P)
(h𝓕 : 𝓕.IsRightContinuous)
:
theorem
ProbabilityTheory.isLocalizingSequence_hittingAfter_Ici
{Ω : Type u_2}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{ι : Type u_4}
[PartialOrder ι]
[TopologicalSpace ι]
[OrderTopology ι]
[FirstCountableTopology ι]
[InfSet ι]
[Bot ι]
[CompactIccSpace ι]
(𝓕 : MeasureTheory.Filtration ι mΩ)
(τ : ℕ → Ω → WithTop ι)
{X : ι → Ω → ℝ}
(hX1 : MeasureTheory.Adapted 𝓕 X)
(hX2 : ∀ (ω : Ω), Function.RightContinuous fun (x : ι) => X x ω)
(h𝓕 : 𝓕.IsRightContinuous)
:
IsLocalizingSequence 𝓕 (fun (n : ℕ) => MeasureTheory.hittingAfter X (Set.Ici ↑n) ⊥) P
theorem
ProbabilityTheory.sup_stoppedProcess_hittingAfter_Ici_le
{ι : Type u_1}
{Ω : Type u_2}
[LinearOrder ι]
{E : Type u_4}
[NormedAddCommGroup E]
[InfSet ι]
[Bot ι]
{X : ι → Ω → E}
(t : ι)
(K : ℝ)
(ω : Ω)
:
⨆ (s : ι),
⨆ (_ : s ≤ t),
‖MeasureTheory.stoppedProcess X (MeasureTheory.hittingAfter (fun (t : ι) (ω : Ω) => ‖X t ω‖) (Set.Ici K) ⊥) s ω‖ ≤ K + {ω : Ω | MeasureTheory.hittingAfter (fun (t : ι) (ω : Ω) => ‖X t ω‖) (Set.Ici K) ⊥ ω ≤ ↑t}.indicator
(fun (ω : Ω) =>
‖MeasureTheory.stoppedValue X (MeasureTheory.hittingAfter (fun (t : ι) (ω : Ω) => ‖X t ω‖) (Set.Ici K) ⊥) ω‖)
ω
theorem
ProbabilityTheory.ClassDL.hasLocallyIntegrableSup
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[NormedAddCommGroup E]
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X : ι → Ω → E}
[LinearOrder ι]
{𝓕 : MeasureTheory.Filtration ι mΩ}
[TopologicalSpace ι]
[OrderTopology ι]
[FirstCountableTopology ι]
[InfSet ι]
[CompactIccSpace ι]
[OrderBot ι]
(hX1 : ∀ (ω : Ω), IsCadlag fun (x : ι) => X x ω)
(hX2 : ClassDL X 𝓕 P)
(h𝓕 : 𝓕.IsRightContinuous)
:
HasLocallyIntegrableSup X 𝓕 P
theorem
ProbabilityTheory.hasLocallyIntegrableSup_of_locally_classDL
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[NormedAddCommGroup E]
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X : ι → Ω → E}
[LinearOrder ι]
{𝓕 : MeasureTheory.Filtration ι mΩ}
[TopologicalSpace ι]
[OrderTopology ι]
[FirstCountableTopology ι]
[InfSet ι]
[CompactIccSpace ι]
[OrderBot ι]
(hX1 : ∀ (ω : Ω), IsCadlag fun (x : ι) => X x ω)
(hX2 : Locally (fun (x : ι → Ω → E) => ClassDL x 𝓕 P) 𝓕 X P)
(h𝓕 : 𝓕.IsRightContinuous)
:
HasLocallyIntegrableSup X 𝓕 P