Locally integrable, class D, class DL #
def
ProbabilityTheory.HasStronglyMeasurableSupProcess
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[NormedAddCommGroup E]
{mΩ : MeasurableSpace Ω}
[LinearOrder ι]
[MeasurableSpace ι]
(X : ι → Ω → E)
:
The condition that the running supremum process (t, ω) ↦ sup_{s ≤ t} ‖X s ω‖ is strongly
measurable as a function on the product.
Equations
- ProbabilityTheory.HasStronglyMeasurableSupProcess X = MeasureTheory.StronglyMeasurable fun (tω : ι × Ω) => ⨆ (s : ι), ⨆ (_ : s ≤ tω.1), ‖X s tω.2‖ₑ
Instances For
def
ProbabilityTheory.HasIntegrableSup
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[NormedAddCommGroup E]
{mΩ : MeasurableSpace Ω}
[LinearOrder ι]
[MeasurableSpace ι]
(X : ι → Ω → E)
(P : MeasureTheory.Measure Ω := by volume_tac)
:
A stochastic process has integrable supremum if the function (t, ω) ↦ sup_{s ≤ t} ‖X s ω‖
is strongly measurable and if for all t, the random variable ω ↦ sup_{s ≤ t} ‖X s ω‖
is integrable.
Equations
- ProbabilityTheory.HasIntegrableSup X P = (ProbabilityTheory.HasStronglyMeasurableSupProcess X ∧ ∀ (t : ι), MeasureTheory.Integrable (fun (ω : Ω) => ⨆ (s : ι), ⨆ (_ : s ≤ t), ‖X s ω‖ₑ) P)
Instances For
def
ProbabilityTheory.HasLocallyIntegrableSup
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[NormedAddCommGroup E]
{mΩ : MeasurableSpace Ω}
[LinearOrder ι]
[OrderBot ι]
[TopologicalSpace ι]
[OrderTopology ι]
[MeasurableSpace ι]
(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
- ProbabilityTheory.HasLocallyIntegrableSup X 𝓕 P = ProbabilityTheory.Locally (fun (x : ι → Ω → E) => ProbabilityTheory.HasIntegrableSup x P) 𝓕 X P
Instances For
structure
ProbabilityTheory.ClassD
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[NormedAddCommGroup E]
{mΩ : MeasurableSpace Ω}
[Preorder ι]
[Nonempty ι]
[MeasurableSpace ι]
(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.
- progMeasurable : MeasureTheory.ProgMeasurable 𝓕 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 ι]
[MeasurableSpace ι]
(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.
- progMeasurable : MeasureTheory.ProgMeasurable 𝓕 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 ι]
[MeasurableSpace ι]
{𝓕 : MeasureTheory.Filtration ι mΩ}
{X : ι → Ω → E}
(hX : ClassD X 𝓕 P)
:
ClassDL X 𝓕 P
theorem
ProbabilityTheory.classD_of_uniformIntegrable_bounded_stoppingTime
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[NormedAddCommGroup E]
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[LinearOrder ι]
[TopologicalSpace ι]
[OrderTopology ι]
[OrderBot ι]
[MeasurableSpace ι]
[SecondCountableTopology ι]
{𝓕 : MeasureTheory.Filtration ι mΩ}
{X : ι → Ω → E}
(hX :
MeasureTheory.UniformIntegrable
(fun (T : ↑{T : Ω → WithTop ι | MeasureTheory.IsStoppingTime 𝓕 T ∧ ∃ (t : ι), ∀ (ω : Ω), T ω ≤ ↑t}) =>
MeasureTheory.stoppedValue X ↑T)
1 P)
(hm : MeasureTheory.ProgMeasurable 𝓕 X)
:
ClassD X 𝓕 P
If {stoppedValue X T : T is a bounded stopping time} is uniformly integrable, then X is
of class D.
theorem
MeasureTheory.Submartingale.classDL
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[NormedAddCommGroup E]
{mΩ : MeasurableSpace Ω}
{P : Measure Ω}
{X : ι → Ω → E}
[LinearOrder ι]
{𝓕 : Filtration ι mΩ}
[TopologicalSpace ι]
[OrderTopology ι]
[OrderBot ι]
[MeasurableSpace ι]
[SecondCountableTopology ι]
[NormedSpace ℝ E]
[CompleteSpace E]
[TopologicalSpace.PseudoMetrizableSpace ι]
[BorelSpace ι]
[Lattice E]
[HasSolidNorm E]
[IsOrderedAddMonoid E]
[IsOrderedModule ℝ E]
[IsFiniteMeasure P]
(hX1 : Submartingale X 𝓕 P)
(hX2 : ∀ (ω : Ω), Function.RightContinuous fun (x : ι) => X x ω)
(hX3 : 0 ≤ X)
:
theorem
MeasureTheory.Submartingale.uniformIntegrable_bounded_stoppingTime
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[NormedAddCommGroup E]
{mΩ : MeasurableSpace Ω}
{P : Measure Ω}
{X : ι → Ω → E}
[LinearOrder ι]
{𝓕 : Filtration ι mΩ}
[TopologicalSpace ι]
[OrderTopology ι]
[OrderBot ι]
[MeasurableSpace ι]
[SecondCountableTopology ι]
[NormedSpace ℝ E]
[CompleteSpace E]
[TopologicalSpace.PseudoMetrizableSpace ι]
[BorelSpace ι]
[Lattice E]
[HasSolidNorm E]
[IsOrderedAddMonoid E]
[IsOrderedModule ℝ E]
[IsFiniteMeasure P]
(hX1 : Submartingale X 𝓕 P)
(hX2 : ∀ (ω : Ω), Function.RightContinuous fun (x : ι) => X x ω)
(hX3 : 0 ≤ X)
(hX4 : UniformIntegrable X 1 P)
:
UniformIntegrable
(fun (T : ↑{T : Ω → WithTop ι | IsStoppingTime 𝓕 T ∧ ∃ (t : ι), ∀ (ω : Ω), T ω ≤ ↑t}) => stoppedValue X ↑T) 1 P
theorem
MeasureTheory.Submartingale.classD_iff_uniformIntegrable
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[NormedAddCommGroup E]
{mΩ : MeasurableSpace Ω}
{P : Measure Ω}
{X : ι → Ω → E}
[LinearOrder ι]
{𝓕 : Filtration ι mΩ}
[TopologicalSpace ι]
[OrderTopology ι]
[OrderBot ι]
[MeasurableSpace ι]
[SecondCountableTopology ι]
[NormedSpace ℝ E]
[CompleteSpace E]
[TopologicalSpace.PseudoMetrizableSpace ι]
[BorelSpace ι]
[Lattice E]
[HasSolidNorm E]
[IsOrderedAddMonoid E]
[IsOrderedModule ℝ E]
[IsFiniteMeasure P]
(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}
[LinearOrder ι]
{𝓕 : Filtration ι mΩ}
[TopologicalSpace ι]
[OrderTopology ι]
[OrderBot ι]
[MeasurableSpace ι]
[SecondCountableTopology ι]
[NormedSpace ℝ E]
[CompleteSpace E]
[IsFiniteMeasure P]
[TopologicalSpace.PseudoMetrizableSpace ι]
[BorelSpace ι]
(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}
[LinearOrder ι]
{𝓕 : Filtration ι mΩ}
[TopologicalSpace ι]
[OrderTopology ι]
[OrderBot ι]
[MeasurableSpace ι]
[SecondCountableTopology ι]
[NormedSpace ℝ E]
[CompleteSpace E]
(hX1 : Martingale X 𝓕 P)
(hX2 : ∀ (ω : Ω), Function.RightContinuous fun (x : ι) => X x ω)
:
theorem
ProbabilityTheory.isStable_stronglyMeasurable_uncurry
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[NormedAddCommGroup E]
{mΩ : MeasurableSpace Ω}
[LinearOrder ι]
{𝓕 : MeasureTheory.Filtration ι mΩ}
[OrderBot ι]
[TopologicalSpace ι]
[SecondCountableTopology ι]
[OrderTopology ι]
[MeasurableSpace ι]
[BorelSpace ι]
:
IsStable 𝓕 fun (X : ι → Ω → E) => MeasureTheory.StronglyMeasurable (Function.uncurry X)
theorem
ProbabilityTheory.isStable_progMeasurable
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[NormedAddCommGroup E]
{mΩ : MeasurableSpace Ω}
[LinearOrder ι]
{𝓕 : MeasureTheory.Filtration ι mΩ}
[OrderBot ι]
[MeasurableSpace ι]
[TopologicalSpace ι]
[TopologicalSpace.PseudoMetrizableSpace ι]
[BorelSpace ι]
[SecondCountableTopology ι]
[OrderTopology ι]
:
theorem
ProbabilityTheory.ProgMeasurable.stronglyMeasurable_uncurry_stoppedProcess_const
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[NormedAddCommGroup E]
{mΩ : MeasurableSpace Ω}
[LinearOrder ι]
[TopologicalSpace ι]
[OrderTopology ι]
[MeasurableSpace ι]
[BorelSpace ι]
[OrderBot ι]
{X : ι → Ω → E}
{𝓕 : MeasureTheory.Filtration ι mΩ}
(hX : MeasureTheory.ProgMeasurable 𝓕 X)
(t : ι)
:
MeasureTheory.StronglyMeasurable (Function.uncurry (MeasureTheory.stoppedProcess X fun (x : Ω) => ↑t))
theorem
ProbabilityTheory.ProgMeasurable.stronglyMeasurable_uncurry_of_isCountablyGenerated_atTop
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[NormedAddCommGroup E]
{mΩ : MeasurableSpace Ω}
[LinearOrder ι]
[OrderBot ι]
[TopologicalSpace ι]
[OrderTopology ι]
[MeasurableSpace ι]
[BorelSpace ι]
[Filter.atTop.IsCountablyGenerated]
{X : ι → Ω → E}
{𝓕 : MeasureTheory.Filtration ι mΩ}
(hX : MeasureTheory.ProgMeasurable 𝓕 X)
:
theorem
ProbabilityTheory.isStable_hasStronglyMeasurableSupProcess
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[NormedAddCommGroup E]
{mΩ : MeasurableSpace Ω}
[LinearOrder ι]
{𝓕 : MeasureTheory.Filtration ι mΩ}
[OrderBot ι]
[TopologicalSpace ι]
[SecondCountableTopology ι]
[OrderTopology ι]
[MeasurableSpace ι]
[BorelSpace ι]
:
IsStable 𝓕 fun (x : ι → Ω → E) => HasStronglyMeasurableSupProcess x
theorem
ProbabilityTheory.isStable_hasIntegrableSup
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[NormedAddCommGroup E]
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[LinearOrder ι]
{𝓕 : MeasureTheory.Filtration ι mΩ}
[OrderBot ι]
[TopologicalSpace ι]
[SecondCountableTopology ι]
[OrderTopology ι]
[MeasurableSpace ι]
[BorelSpace ι]
:
IsStable 𝓕 fun (x : ι → Ω → E) => HasIntegrableSup x P
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 ι]
[MeasurableSpace ι]
[SecondCountableTopology ι]
[BorelSpace ι]
:
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 ι]
[MeasurableSpace ι]
[TopologicalSpace ι]
[OrderTopology ι]
[TopologicalSpace.PseudoMetrizableSpace ι]
[BorelSpace ι]
[SecondCountableTopology ι]
[NoMaxOrder ι]
:
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 ι]
[TopologicalSpace ι]
[OrderTopology ι]
[MeasurableSpace ι]
[NoMaxOrder ι]
[BorelSpace ι]
[SecondCountableTopology ι]
[TopologicalSpace.PseudoMetrizableSpace ι]
:
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 ι]
[MeasurableSpace ι]
(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 ι]
[MeasurableSpace ι]
(hX1 : HasLocallyIntegrableSup X 𝓕 P)
(hX2 : MeasureTheory.Adapted 𝓕 X)
(h𝓕 : 𝓕.IsRightContinuous)
:
theorem
ProbabilityTheory.ClassDL.classD
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[NormedAddCommGroup E]
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X : ι → Ω → E}
[Preorder ι]
{𝓕 : MeasureTheory.Filtration ι mΩ}
[OrderTop ι]
[MeasurableSpace ι]
(hX : ClassDL X 𝓕 P)
:
ClassD X 𝓕 P
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 ι]
[SecondCountableTopology ι]
[MeasurableSpace ι]
[BorelSpace ι]
[TopologicalSpace.PseudoMetrizableSpace ι]
[OrderTopology ι]
(hX : ClassDL X 𝓕 P)
:
theorem
ProbabilityTheory.locally_classD_of_locally_classDL
{Ω : Type u_2}
{E : Type u_3}
[NormedAddCommGroup E]
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{ι : Type u_4}
[ConditionallyCompleteLinearOrderBot ι]
[TopologicalSpace ι]
[OrderTopology ι]
[DenselyOrdered ι]
[SecondCountableTopology ι]
[NoMaxOrder ι]
[MeasurableSpace ι]
[BorelSpace ι]
[TopologicalSpace.PseudoMetrizableSpace ι]
{𝓕 : MeasureTheory.Filtration ι mΩ}
{X : ι → Ω → E}
[MeasureTheory.IsFiniteMeasure P]
(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_2}
{E : Type u_4}
[NormedAddCommGroup E]
{ι : Type u_5}
[ConditionallyCompleteLinearOrderBot ι]
{X : ι → Ω → E}
(t : ι)
(K : ℝ)
(hK : 0 ≤ 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 ι]
[MeasurableSpace ι]
(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}
[ConditionallyCompleteLinearOrderBot ι]
[TopologicalSpace ι]
[OrderTopology ι]
[MeasurableSpace ι]
[SecondCountableTopology ι]
[DenselyOrdered ι]
[NoMaxOrder ι]
[BorelSpace ι]
[TopologicalSpace.PseudoMetrizableSpace ι]
[MeasureTheory.IsFiniteMeasure P]
{𝓕 : MeasureTheory.Filtration ι mΩ}
{h𝓕 : 𝓕.IsRightContinuous}
(hX1 : Locally (fun (X : ι → Ω → E) => ∀ (ω : Ω), IsCadlag fun (x : ι) => X x ω) 𝓕 X P)
(hX2 : Locally (fun (x : ι → Ω → E) => ClassDL x 𝓕 P) 𝓕 X P)
:
HasLocallyIntegrableSup X 𝓕 P