Local (sub)martingales

def ProbabilityTheory.IsLocalMartingale {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] [NormedAddCommGroup E] [NormedSpace ℝ 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

def ProbabilityTheory.IsLocalSubmartingale {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] [NormedAddCommGroup E] [NormedSpace ℝ 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

theorem ProbabilityTheory.Martingale.IsLocalMartingale {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] [NormedAddCommGroup E] [NormedSpace ℝ 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

theorem ProbabilityTheory.Submartingale.IsLocalSubmartingale {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] [NormedAddCommGroup E] [NormedSpace ℝ 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

theorem ProbabilityTheory.IsLocalMartingale.locally_isStronglyProgressive {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] [NormedAddCommGroup E] [NormedSpace ℝ E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : ι → Ω → E} {𝓕 : MeasureTheory.Filtration ι mΩ} [SecondCountableTopology ι] [MeasurableSpace ι] [BorelSpace ι] (hX : IsLocalMartingale X 𝓕 P) : Locally (MeasureTheory.IsStronglyProgressive 𝓕) 𝓕 X P

theorem ProbabilityTheory.IsLocalSubmartingale.locally_isStronglyProgressive {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] [NormedAddCommGroup E] [NormedSpace ℝ E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : ι → Ω → E} {𝓕 : MeasureTheory.Filtration ι mΩ} [SecondCountableTopology ι] [MeasurableSpace ι] [BorelSpace ι] [LE E] (hX : IsLocalSubmartingale X 𝓕 P) : Locally (MeasureTheory.IsStronglyProgressive 𝓕) 𝓕 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 ι] [TopologicalSpace.PseudoMetrizableSpace ι] (hX : StronglyAdapted 𝓕 X) (hC : ∀ (ω : Ω), IsRightContinuous 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] {mΩ : MeasurableSpace Ω} {P : Measure Ω} {X : ι → Ω → E} {𝓕 : Filtration ι mΩ} [SecondCountableTopology ι] [TopologicalSpace.PseudoMetrizableSpace ι] [IsFiniteMeasure P] [Approximable 𝓕 P] [CompleteSpace E] (hX : Martingale X 𝓕 P) (hC : ∀ (ω : Ω), IsRightContinuous fun (x : ι) => X x ω) {τ : Ω → WithTop ι} (hτ : IsStoppingTime 𝓕 τ) : Martingale (MeasureTheory.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] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} [SecondCountableTopology ι] [TopologicalSpace.PseudoMetrizableSpace ι] [MeasureTheory.IsFiniteMeasure P] [MeasureTheory.Approximable 𝓕 P] [CompleteSpace E] : 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] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} [SecondCountableTopology ι] [TopologicalSpace.PseudoMetrizableSpace ι] [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.