# Square integrable martingales #

source
structure ProbabilityTheory.IsSquareIntegrable {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [TopologicalSpace ι] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {mΩ : MeasurableSpace Ω} (X : ι → Ω → E) (𝓕 : MeasureTheory.Filtration ι mΩ) (P : MeasureTheory.Measure Ω) :
Prop

A square integrable martingale is a martingale with cadlag paths and uniformly bounded second moments.

- martingale : MeasureTheory.Martingale X 𝓕 P
- cadlag (ω : Ω) : IsCadlag fun (x : ι) => X x ω
- bounded : ⨆ (i : ι), MeasureTheory.eLpNorm (X i) 2 P < ⊤

Instances For

source
theorem ProbabilityTheory.IsSquareIntegrable.integrable_sq {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [TopologicalSpace ι] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : ι → Ω → E} {𝓕 : MeasureTheory.Filtration ι mΩ} (hX : IsSquareIntegrable X 𝓕 P) (i : ι) :
MeasureTheory.Integrable (fun (ω : Ω) => ‖X i ω‖ ^ 2) P
source
theorem ProbabilityTheory.IsSquareIntegrable.add {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [TopologicalSpace ι] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X Y : ι → Ω → E} {𝓕 : MeasureTheory.Filtration ι mΩ} (hX : IsSquareIntegrable X 𝓕 P) (hY : IsSquareIntegrable Y 𝓕 P) :
IsSquareIntegrable (fun (i : ι) (ω : Ω) => X i ω + Y i ω) 𝓕 P
source
theorem ProbabilityTheory.IsSquareIntegrable.submartingale_sq_norm {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [TopologicalSpace ι] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : ι → Ω → E} {𝓕 : MeasureTheory.Filtration ι mΩ} [MeasureTheory.SigmaFinite P] (hX : IsSquareIntegrable X 𝓕 P) :
MeasureTheory.Submartingale (fun (i : ι) (ω : Ω) => ‖X i ω‖ ^ 2) 𝓕 P
source
theorem ProbabilityTheory.IsSquareIntegrable.eLpNorm_mono {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [TopologicalSpace ι] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : ι → Ω → E} {𝓕 : MeasureTheory.Filtration ι mΩ} [MeasureTheory.SigmaFinite P] [MeasureTheory.SigmaFiniteFiltration P 𝓕] (hX : IsSquareIntegrable X 𝓕 P) {i j : ι} (hij : i ≤ j) :
MeasureTheory.eLpNorm (X i) 2 P ≤ MeasureTheory.eLpNorm (X j) 2 P