# Local (sub)martingales #

source
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) :
Prop

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

source
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) :
Prop

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

source
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 ω) :
ProbabilityTheory.IsLocalMartingale X 𝓕 P
source
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 ω) :
ProbabilityTheory.IsLocalSubmartingale X 𝓕 P
source
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Ω} [MeasurableSpace ι] [SecondCountableTopology ι] [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 ω

Martingales are a stable class.

source
theorem ProbabilityTheory.isStable_submartingale {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} [MeasurableSpace ι] [SecondCountableTopology ι] [BorelSpace ι] [TopologicalSpace.PseudoMetrizableSpace ι] [MeasureTheory.IsFiniteMeasure P] [MeasureTheory.Approximable 𝓕 P] :
IsStable 𝓕 fun (X : ι → Ω → ℝ) => MeasureTheory.Submartingale X 𝓕 P ∧ ∀ (ω : Ω), IsCadlag fun (x : ι) => X x ω

Submartingales are a stable class.