Continuous square integrable martingales

Continuous square integrable martingales

def ProbabilityTheory.continuousSquareIntegrable {ι : Type u_1} {Ω : Type u_2} (E : Type u_3) [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} (P : MeasureTheory.Measure Ω) [LinearOrder ι] [TopologicalSpace ι] (𝓕 : MeasureTheory.Filtration ι mΩ) [CompleteSpace E] [MeasureTheory.IsFiniteMeasure P] [NormedSpace ℝ E] : Submodule ℝ (SquareIntegrable E P 𝓕)

The set of continuous square integrable martingales, as a submodule of the type of square-integrable martingales, see SquareIntegrable.

Equations

• One or more equations did not get rendered due to their size.

theorem ProbabilityTheory.continuous_coe {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [TopologicalSpace ι] {𝓕 : MeasureTheory.Filtration ι mΩ} [CompleteSpace E] [MeasureTheory.IsFiniteMeasure P] [NormedSpace ℝ E] {X : SquareIntegrable E P 𝓕} (hX : X ∈ continuousSquareIntegrable E P 𝓕) (ω : Ω) : Continuous fun (x : ι) => ↑X x ω

theorem ProbabilityTheory.IsAESquareIntegrable.isSquareIntegrable_toContinuous {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [TopologicalSpace ι] {X : ι → Ω → E} {𝓕 : MeasureTheory.Filtration ι mΩ} [CompleteSpace E] [NormedSpace ℝ E] [h𝓕 : 𝓕.IsComplete P] (hX1 : ∀ᵐ (ω : Ω) ∂P, Continuous fun (x : ι) => X x ω) (hX2 : IsAESquareIntegrable X 𝓕 P) : IsSquareIntegrable (toContinuous X hX2) 𝓕 P

theorem ProbabilityTheory.mem_continuousSquareIntegrable {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [TopologicalSpace ι] {𝓕 : MeasureTheory.Filtration ι mΩ} [CompleteSpace E] [MeasureTheory.IsFiniteMeasure P] [NormedSpace ℝ E] [𝓕.IsComplete P] {X : SquareIntegrable E P 𝓕} (hX : ∀ᵐ (ω : Ω) ∂P, Continuous fun (x : ι) => ↑X x ω) : X ∈ continuousSquareIntegrable E P 𝓕

A square integrable martingale that is almost surely continuous is indistinguishable from a square integrable martingale that is continuous everywhere.

theorem ProbabilityTheory.IsAESquareIntegrable.mk_mem_continuousSquareIntegrable {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [TopologicalSpace ι] {X : ι → Ω → E} {𝓕 : MeasureTheory.Filtration ι mΩ} [CompleteSpace E] [MeasureTheory.IsFiniteMeasure P] [NormedSpace ℝ E] [𝓕.IsComplete P] (hX1 : IsAESquareIntegrable X 𝓕 P) (hX2 : ∀ᵐ (ω : Ω) ∂P, Continuous fun (x : ι) => X x ω) : SquareIntegrable.mk X hX1 ∈ continuousSquareIntegrable E P 𝓕

A square integrable martingale that is almost surely continuous is indistinguishable from a square integrable martingale that is continuous everywhere.

theorem ProbabilityTheory.exists_subsequence_ae_tendsto_uniformly {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [TopologicalSpace ι] {𝓕 : MeasureTheory.Filtration ι mΩ} [CompleteSpace E] [MeasureTheory.IsFiniteMeasure P] [NormedSpace ℝ E] {M : ℕ → ι → Ω → E} {N : ι → Ω → E} [OrderTopology ι] [SecondCountableTopology ι] (hM : ∀ (n : ℕ), IsAESquareIntegrable (M n) 𝓕 P) (hN : IsAESquareIntegrable N 𝓕 P) (h : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (MeasureTheory.Filtration.limitProcess (M n) 𝓕 P - MeasureTheory.Filtration.limitProcess N 𝓕 P) 2 P) Filter.atTop (nhds 0)) : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ᵐ (ω : Ω) ∂P, TendstoUniformly (fun (n : ℕ) (t : ι) => M (φ n) t ω) (fun (x : ι) => N x ω) Filter.atTop

If M is a sequence of square integrable martingales that converges to N in SquareIntegrable E P 𝓕, then there exists φ : ℕ → ℕ increasing such that almost surely, M n converges to N uniformly. This is needed to show that the space of continuous square integrable martingales is closed.

instance ProbabilityTheory.instIsClosedSquareIntegrableCoeSubmoduleRealContinuousSquareIntegrableOfIsCompleteOfOrderTopology {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [TopologicalSpace ι] {𝓕 : MeasureTheory.Filtration ι mΩ} [CompleteSpace E] [MeasureTheory.IsFiniteMeasure P] [NormedSpace ℝ E] [𝓕.IsComplete P] [Nonempty ι] [OrderTopology ι] [SecondCountableTopology ι] : IsClosed ↑(continuousSquareIntegrable E P 𝓕)

The submodule of continuous square integrable martingales is closed in the Hilbert space of square integrable martingales.

noncomputable def ProbabilityTheory.continuousPart {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} [LinearOrder ι] [TopologicalSpace ι] [CompleteSpace E] [InnerProductSpace ℝ E] [OrderBot ι] [OrderTopology ι] [SecondCountableTopology ι] (X : ι → Ω → E) (𝓕 : MeasureTheory.Filtration ι mΩ) (P : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure P] [𝓕.IsComplete P] [𝓕.IsRightContinuous] : ι → Ω → E

The continuous martingale part of a square-integrable martingale X. This is defined as the projection of X onto the closed subspace of continuous square-integrable martingales.

Equations

• One or more equations did not get rendered due to their size.

theorem ProbabilityTheory.continuousPart_congr {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [TopologicalSpace ι] {X Y : ι → Ω → E} {𝓕 : MeasureTheory.Filtration ι mΩ} [CompleteSpace E] [MeasureTheory.IsFiniteMeasure P] [InnerProductSpace ℝ E] [OrderBot ι] [OrderTopology ι] [SecondCountableTopology ι] [𝓕.IsRightContinuous] [𝓕.IsComplete P] (hXY : X ≡ᵐ[P] Y) : continuousPart X 𝓕 P = continuousPart Y 𝓕 P

theorem ProbabilityTheory.continuous_continuousPart {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [TopologicalSpace ι] {𝓕 : MeasureTheory.Filtration ι mΩ} [CompleteSpace E] [MeasureTheory.IsFiniteMeasure P] [InnerProductSpace ℝ E] [OrderBot ι] [OrderTopology ι] [SecondCountableTopology ι] [𝓕.IsRightContinuous] [𝓕.IsComplete P] (X : ι → Ω → E) (ω : Ω) : Continuous fun (x : ι) => continuousPart X 𝓕 P x ω

theorem ProbabilityTheory.isSquareIntegrable_continuousPart {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [TopologicalSpace ι] {X : ι → Ω → E} {𝓕 : MeasureTheory.Filtration ι mΩ} [CompleteSpace E] [MeasureTheory.IsFiniteMeasure P] [InnerProductSpace ℝ E] [OrderBot ι] [OrderTopology ι] [SecondCountableTopology ι] [𝓕.IsRightContinuous] [𝓕.IsComplete P] : IsSquareIntegrable (continuousPart X 𝓕 P) 𝓕 P

theorem ProbabilityTheory.IsAESquareIntegrable.mk_continuousPart {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [TopologicalSpace ι] {X : ι → Ω → E} {𝓕 : MeasureTheory.Filtration ι mΩ} [CompleteSpace E] [MeasureTheory.IsFiniteMeasure P] [InnerProductSpace ℝ E] [OrderBot ι] [OrderTopology ι] [SecondCountableTopology ι] [𝓕.IsRightContinuous] [𝓕.IsComplete P] (hX : IsAESquareIntegrable X 𝓕 P) : SquareIntegrable.mk (continuousPart X 𝓕 P) ⋯ = (continuousSquareIntegrable E P 𝓕).starProjection (SquareIntegrable.mk X hX)

noncomputable def ProbabilityTheory.discontinuousPart {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} [LinearOrder ι] [TopologicalSpace ι] [CompleteSpace E] [InnerProductSpace ℝ E] [OrderBot ι] [OrderTopology ι] [SecondCountableTopology ι] (X : ι → Ω → E) (𝓕 : MeasureTheory.Filtration ι mΩ) (P : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure P] [𝓕.IsComplete P] [𝓕.IsRightContinuous] : ι → Ω → E

The purely discontinuous martingale part of a square integrable martingale. Purely discontinuous martingales are the orthogonal submodule of continuous square integrable martingales in the Hilbert space of square integrable martingales.

Equations

• ProbabilityTheory.discontinuousPart X 𝓕 P = X - ProbabilityTheory.continuousPart X 𝓕 P

theorem ProbabilityTheory.discontinuousPart_def {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [TopologicalSpace ι] {𝓕 : MeasureTheory.Filtration ι mΩ} [CompleteSpace E] [MeasureTheory.IsFiniteMeasure P] [InnerProductSpace ℝ E] [OrderBot ι] [OrderTopology ι] [SecondCountableTopology ι] [𝓕.IsRightContinuous] [𝓕.IsComplete P] (X : ι → Ω → E) : discontinuousPart X 𝓕 P = X - continuousPart X 𝓕 P

theorem ProbabilityTheory.continuousPart_add_discontinuousPart {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [TopologicalSpace ι] {X : ι → Ω → E} {𝓕 : MeasureTheory.Filtration ι mΩ} [CompleteSpace E] [MeasureTheory.IsFiniteMeasure P] [InnerProductSpace ℝ E] [OrderBot ι] [OrderTopology ι] [SecondCountableTopology ι] [𝓕.IsRightContinuous] [𝓕.IsComplete P] : continuousPart X 𝓕 P + discontinuousPart X 𝓕 P = X

theorem ProbabilityTheory.IsAESquareIntegrable.discontinuousPart {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [TopologicalSpace ι] {X : ι → Ω → E} {𝓕 : MeasureTheory.Filtration ι mΩ} [CompleteSpace E] [MeasureTheory.IsFiniteMeasure P] [InnerProductSpace ℝ E] [OrderBot ι] [OrderTopology ι] [SecondCountableTopology ι] [𝓕.IsRightContinuous] [𝓕.IsComplete P] (hX : IsAESquareIntegrable X 𝓕 P) : IsAESquareIntegrable (ProbabilityTheory.discontinuousPart X 𝓕 P) 𝓕 P

noncomputable def ProbabilityTheory.discontinuousSquareIntegrable {ι : Type u_1} {Ω : Type u_2} (E : Type u_3) [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} (P : MeasureTheory.Measure Ω) [LinearOrder ι] [TopologicalSpace ι] (𝓕 : MeasureTheory.Filtration ι mΩ) [CompleteSpace E] [MeasureTheory.IsFiniteMeasure P] [InnerProductSpace ℝ E] [OrderBot ι] [SecondCountableTopology ι] : Submodule ℝ (SquareIntegrable E P 𝓕)

The submodule of purely discontinuous square integrable martingales. Purely discontinuous martingales are the orthogonal submodule of continuous square integrable martingales in the Hilbert space of square integrable martingales.

Equations

• ProbabilityTheory.discontinuousSquareIntegrable E P 𝓕 = (ProbabilityTheory.continuousSquareIntegrable E P 𝓕)ᗮ

theorem ProbabilityTheory.mem_discontinuousSquareIntegrable {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [TopologicalSpace ι] {𝓕 : MeasureTheory.Filtration ι mΩ} [CompleteSpace E] [MeasureTheory.IsFiniteMeasure P] [InnerProductSpace ℝ E] [OrderBot ι] [SecondCountableTopology ι] {Y : SquareIntegrable E P 𝓕} (hY : IsPurelyDiscontinuous (↑Y) 𝓕 P) : Y ∈ discontinuousSquareIntegrable E P 𝓕

A purely discontinuous square integrable martingale is in the submodule of purely discontinuous square integrable martingales. This statements links the predicate IsPurelyDiscontinuous with the submodule discontinuousSquareIntegrable.

theorem ProbabilityTheory.IsPurelyDiscontinuous.mk_mem_discontinuousSquareIntegrable {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [TopologicalSpace ι] {Y : ι → Ω → E} {𝓕 : MeasureTheory.Filtration ι mΩ} [CompleteSpace E] [MeasureTheory.IsFiniteMeasure P] [InnerProductSpace ℝ E] [OrderBot ι] [SecondCountableTopology ι] (hY : IsPurelyDiscontinuous Y 𝓕 P) : SquareIntegrable.mk Y ⋯ ∈ discontinuousSquareIntegrable E P 𝓕

A purely discontinuous square integrable martingale is in the submodule of purely discontinuous square integrable martingales. This statements links the predicate IsPurelyDiscontinuous with the submodule discontinuousSquareIntegrable.

theorem ProbabilityTheory.isPurelyDiscontinuous_discontinuousPart {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [TopologicalSpace ι] {X : ι → Ω → E} {𝓕 : MeasureTheory.Filtration ι mΩ} [CompleteSpace E] [MeasureTheory.IsFiniteMeasure P] [InnerProductSpace ℝ E] [OrderBot ι] [OrderTopology ι] [SecondCountableTopology ι] [𝓕.IsRightContinuous] [𝓕.IsComplete P] (hX : IsAESquareIntegrable X 𝓕 P) : IsPurelyDiscontinuous (discontinuousPart X 𝓕 P) 𝓕 P

The discontinuous part of square integrable martingale is purely discontinuous.

theorem ProbabilityTheory.indist_continuousPart {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [TopologicalSpace ι] {X Y Z : ι → Ω → E} {𝓕 : MeasureTheory.Filtration ι mΩ} [CompleteSpace E] [MeasureTheory.IsFiniteMeasure P] [InnerProductSpace ℝ E] [OrderBot ι] [OrderTopology ι] [SecondCountableTopology ι] [𝓕.IsRightContinuous] [𝓕.IsComplete P] (hX1 : IsAESquareIntegrable X 𝓕 P) (hX2 : ∀ᵐ (ω : Ω) ∂P, Continuous fun (x : ι) => X x ω) (hY : IsPurelyDiscontinuous Y 𝓕 P) (hZ1 : IsAESquareIntegrable Z 𝓕 P) (hZ2 : Z ≡ᵐ[P] X + Y) : X ≡ᵐ[P] continuousPart Z 𝓕 P

Uniqueness of the decomposition of a square integrable martingale into a continuous part and a discontinuous part: If a square integrable martingale Z is indistinguishable from X + Y where X is continuous and Y is discontinuous, then X is indistinguishable from the continuous part of Z.

theorem ProbabilityTheory.indist_discontinuousPart {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [TopologicalSpace ι] {𝓕 : MeasureTheory.Filtration ι mΩ} [CompleteSpace E] [MeasureTheory.IsFiniteMeasure P] [InnerProductSpace ℝ E] [OrderBot ι] [OrderTopology ι] [SecondCountableTopology ι] [𝓕.IsRightContinuous] [𝓕.IsComplete P] {X Y Z : ι → Ω → E} (hX1 : IsAESquareIntegrable X 𝓕 P) (hX2 : ∀ᵐ (ω : Ω) ∂P, Continuous fun (x : ι) => X x ω) (hY2 : IsPurelyDiscontinuous Y 𝓕 P) (hZ1 : IsAESquareIntegrable Z 𝓕 P) (hZ2 : Z ≡ᵐ[P] X + Y) : Y ≡ᵐ[P] discontinuousPart Z 𝓕 P

Uniqueness of the decomposition of a square integrable martingale into a continuous part and a discontinuous part: If a square integrable martingale Z is indistinguishable from X + Y where X is continuous and Y is discontinuous, then Y is indistinguishable from the discontinuous part of Z.

theorem ProbabilityTheory.IsPurelyDiscontinuous.stoppedProcess {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [TopologicalSpace ι] {X : ι → Ω → E} {𝓕 : MeasureTheory.Filtration ι mΩ} {τ : Ω → WithTop ι} [CompleteSpace E] [MeasureTheory.IsFiniteMeasure P] [InnerProductSpace ℝ E] [OrderBot ι] [OrderTopology ι] [SecondCountableTopology ι] [MeasureTheory.Approximable 𝓕 P] (hX : IsPurelyDiscontinuous X 𝓕 P) (hτ : MeasureTheory.IsStoppingTime 𝓕 τ) : IsPurelyDiscontinuous (MeasureTheory.stoppedProcess X τ) 𝓕 P

The stopped process of a purely discontinuous square integrable martingale is again a purely discontinuous square integrable martingale.

theorem ProbabilityTheory.continuousPart_stoppedProcess {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [TopologicalSpace ι] {𝓕 : MeasureTheory.Filtration ι mΩ} {τ : Ω → WithTop ι} [CompleteSpace E] [MeasureTheory.IsFiniteMeasure P] [InnerProductSpace ℝ E] [OrderBot ι] [OrderTopology ι] [SecondCountableTopology ι] [𝓕.IsRightContinuous] [𝓕.IsComplete P] [MeasureTheory.Approximable 𝓕 P] {X : ι → Ω → E} (hX : IsAESquareIntegrable X 𝓕 P) (hτ : MeasureTheory.IsStoppingTime 𝓕 τ) : continuousPart (MeasureTheory.stoppedProcess X τ) 𝓕 P ≡ᵐ[P] MeasureTheory.stoppedProcess (continuousPart X 𝓕 P) τ

The continuous part of the stopped process is the stopped process of the continuous part.

theorem MeasureTheory.fun_stoppedProcess_sub {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [Nonempty ι] {u v : ι → Ω → β} {τ : Ω → WithTop ι} [LinearOrder ι] [Sub β] : stoppedProcess (fun (i : ι) (i_1 : Ω) => u i i_1 - v i i_1) τ = fun (i : ι) (i_1 : Ω) => stoppedProcess u τ i i_1 - stoppedProcess v τ i i_1

Eta-expanded form of MeasureTheory.stoppedProcess_sub

theorem ProbabilityTheory.discontinuousPart_stoppedProcess {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [TopologicalSpace ι] {𝓕 : MeasureTheory.Filtration ι mΩ} {τ : Ω → WithTop ι} [CompleteSpace E] [MeasureTheory.IsFiniteMeasure P] [InnerProductSpace ℝ E] [OrderBot ι] [OrderTopology ι] [SecondCountableTopology ι] [𝓕.IsRightContinuous] [𝓕.IsComplete P] [MeasureTheory.Approximable 𝓕 P] {X : ι → Ω → E} (hX : IsAESquareIntegrable X 𝓕 P) (hτ : MeasureTheory.IsStoppingTime 𝓕 τ) : discontinuousPart (MeasureTheory.stoppedProcess X τ) 𝓕 P ≡ᵐ[P] MeasureTheory.stoppedProcess (discontinuousPart X 𝓕 P) τ

The discontinuous part of the stopped process is the stopped process of the discontinuous part.