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.IsLocalMartingale.locally_progMeasurable
{ι : 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Ω}
[SecondCountableTopology ι]
[MeasurableSpace ι]
[BorelSpace ι]
(hX : IsLocalMartingale X 𝓕 P)
:
Locally (MeasureTheory.ProgMeasurable 𝓕) 𝓕 X P
theorem
ProbabilityTheory.IsLocalSubmartingale.locally_progMeasurable
{ι : 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Ω}
[SecondCountableTopology ι]
[MeasurableSpace ι]
[BorelSpace ι]
[LE E]
(hX : IsLocalSubmartingale X 𝓕 P)
:
Locally (MeasureTheory.ProgMeasurable 𝓕) 𝓕 X P
theorem
MeasureTheory.StronglyAdapted.stoppedProcess_indicator
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[LinearOrder ι]
[OrderBot ι]
[TopologicalSpace ι]
[OrderTopology ι]
[NormedAddCommGroup E]
{mΩ : MeasurableSpace Ω}
{X : ι → Ω → E}
{𝓕 : Filtration ι mΩ}
[SecondCountableTopology ι]
[MeasurableSpace ι]
[BorelSpace ι]
[TopologicalSpace.PseudoMetrizableSpace ι]
(hX : StronglyAdapted 𝓕 X)
(hC : ∀ (ω : Ω), Function.RightContinuous fun (x : ι) => X x ω)
{τ : Ω → WithTop ι}
(hτ : IsStoppingTime 𝓕 τ)
:
StronglyAdapted 𝓕 (MeasureTheory.stoppedProcess (fun (i : ι) => {ω : Ω | ⊥ < τ ω}.indicator (X i)) τ)
theorem
MeasureTheory.Martingale.stoppedProcess_indicator
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[LinearOrder ι]
[OrderBot ι]
[TopologicalSpace ι]
[OrderTopology ι]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{mΩ : MeasurableSpace Ω}
{P : Measure Ω}
{X : ι → Ω → E}
{𝓕 : Filtration ι mΩ}
[SecondCountableTopology ι]
[MeasurableSpace ι]
[BorelSpace ι]
[TopologicalSpace.PseudoMetrizableSpace ι]
[MeasurableSpace E]
[BorelSpace E]
[SecondCountableTopology E]
[IsFiniteMeasure P]
[Approximable 𝓕 P]
(hX : Martingale X 𝓕 P)
(hC : ∀ (ω : Ω), Function.RightContinuous fun (x : ι) => X x ω)
{τ : Ω → WithTop ι}
(hτ : IsStoppingTime 𝓕 τ)
:
Martingale (stoppedProcess (fun (i : ι) => {ω : Ω | ⊥ < τ ω}.indicator (X i)) τ) 𝓕 P
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Ω}
[SecondCountableTopology ι]
[MeasurableSpace ι]
[BorelSpace ι]
[TopologicalSpace.PseudoMetrizableSpace ι]
[MeasurableSpace E]
[BorelSpace E]
[SecondCountableTopology E]
[MeasureTheory.IsFiniteMeasure P]
[MeasureTheory.Approximable 𝓕 P]
:
IsStable 𝓕 fun (X : ι → Ω → E) => MeasureTheory.Martingale X 𝓕 P ∧ ∀ (ω : Ω), IsCadlag fun (x : ι) => X x ω
Càdlàg martingales are a stable class.
theorem
ProbabilityTheory.isStable_submartingale
{ι : 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Ω}
[SecondCountableTopology ι]
[MeasurableSpace ι]
[BorelSpace ι]
[TopologicalSpace.PseudoMetrizableSpace ι]
[MeasurableSpace E]
[BorelSpace E]
[SecondCountableTopology E]
[MeasureTheory.IsFiniteMeasure P]
[MeasureTheory.Approximable 𝓕 P]
[LE E]
:
IsStable 𝓕 fun (X : ι → Ω → E) => MeasureTheory.Submartingale X 𝓕 P ∧ ∀ (ω : Ω), IsCadlag fun (x : ι) => X x ω
Càdlàg submartingales are a stable class.