Local (sub)martingales #
def
ProbabilityTheory.IsLocalMartingale
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[LinearOrder ι]
[OrderBot ι]
[TopologicalSpace ι]
[OrderTopology ι]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{mΩ : MeasurableSpace Ω}
(X : ι → Ω → E)
(𝓕 : MeasureTheory.Filtration ι mΩ)
(P : MeasureTheory.Measure Ω := by volume_tac)
:
A stochastic process is a local martingale if it satisfies the martingale property locally.
Equations
- ProbabilityTheory.IsLocalMartingale X 𝓕 P = ProbabilityTheory.Locally (fun (X : ι → Ω → E) => MeasureTheory.Martingale X 𝓕 P ∧ ∀ (ω : Ω), IsCadlag fun (x : ι) => X x ω) 𝓕 X P
Instances For
def
ProbabilityTheory.IsLocalSubmartingale
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[LinearOrder ι]
[OrderBot ι]
[TopologicalSpace ι]
[OrderTopology ι]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{mΩ : MeasurableSpace Ω}
[LE E]
(X : ι → Ω → E)
(𝓕 : MeasureTheory.Filtration ι mΩ)
(P : MeasureTheory.Measure Ω := by volume_tac)
:
A stochastic process is a local submartingale if it satisfies the submartingale property locally.
Equations
- ProbabilityTheory.IsLocalSubmartingale X 𝓕 P = ProbabilityTheory.Locally (fun (X : ι → Ω → E) => MeasureTheory.Submartingale X 𝓕 P ∧ ∀ (ω : Ω), IsCadlag fun (x : ι) => X x ω) 𝓕 X P
Instances For
theorem
ProbabilityTheory.Martingale.IsLocalMartingale
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[LinearOrder ι]
[OrderBot ι]
[TopologicalSpace ι]
[OrderTopology ι]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X : ι → Ω → E}
{𝓕 : MeasureTheory.Filtration ι mΩ}
(hX : MeasureTheory.Martingale X 𝓕 P)
(hC : ∀ (ω : Ω), IsCadlag fun (x : ι) => X x ω)
:
theorem
ProbabilityTheory.Submartingale.IsLocalSubmartingale
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[LinearOrder ι]
[OrderBot ι]
[TopologicalSpace ι]
[OrderTopology ι]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X : ι → Ω → E}
{𝓕 : MeasureTheory.Filtration ι mΩ}
[LE E]
(hX : MeasureTheory.Submartingale X 𝓕 P)
(hC : ∀ (ω : Ω), IsCadlag fun (x : ι) => X x ω)
:
theorem
ProbabilityTheory.isStable_martingale
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[LinearOrder ι]
[OrderBot ι]
[TopologicalSpace ι]
[OrderTopology ι]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{𝓕 : MeasureTheory.Filtration ι mΩ}
:
IsStable 𝓕 fun (X : ι → Ω → E) => MeasureTheory.Martingale X 𝓕 P ∧ ∀ (ω : Ω), IsCadlag fun (x : ι) => X x ω
Martingales are a stable class.
theorem
ProbabilityTheory.isStable_submartingale
{ι : Type u_1}
{Ω : Type u_2}
[LinearOrder ι]
[OrderBot ι]
[TopologicalSpace ι]
[OrderTopology ι]
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{𝓕 : MeasureTheory.Filtration ι mΩ}
:
IsStable 𝓕 fun (X : ι → Ω → ℝ) => MeasureTheory.Submartingale X 𝓕 P ∧ ∀ (ω : Ω), IsCadlag fun (x : ι) => X x ω
Submartingales are a stable class.