Local (sub)martingales #
def
ProbabilityTheory.IsLocalMartingale
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{mΩ : MeasurableSpace Ω}
[LinearOrder ι]
[OrderBot ι]
(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) 𝓕 X P
Instances For
def
ProbabilityTheory.IsLocalSubmartingale
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{mΩ : MeasurableSpace Ω}
[LinearOrder ι]
[OrderBot ι]
[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) 𝓕 X P
Instances For
theorem
ProbabilityTheory.Martingale.IsLocalMartingale
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[LinearOrder ι]
[OrderBot ι]
{X : ι → Ω → E}
{𝓕 : MeasureTheory.Filtration ι mΩ}
(hX : MeasureTheory.Martingale X 𝓕 P)
:
theorem
ProbabilityTheory.Submartingale.IsLocalSubmartingale
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[LinearOrder ι]
[OrderBot ι]
{X : ι → Ω → E}
{𝓕 : MeasureTheory.Filtration ι mΩ}
[LE E]
(hX : MeasureTheory.Submartingale X 𝓕 P)
:
theorem
ProbabilityTheory.isStable_martingale
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[LinearOrder ι]
[OrderBot ι]
{𝓕 : MeasureTheory.Filtration ι mΩ}
:
IsStable (fun (X : ι → Ω → E) => MeasureTheory.Martingale X 𝓕 P) 𝓕
Martingales are a stable class.
theorem
ProbabilityTheory.isStable_submartingale
{ι : Type u_1}
{Ω : Type u_2}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[LinearOrder ι]
[OrderBot ι]
{𝓕 : MeasureTheory.Filtration ι mΩ}
:
IsStable (fun (X : ι → Ω → ℝ) => MeasureTheory.Submartingale X 𝓕 P) 𝓕
Submartingales are a stable class.