Square integrable martingales

Predicates IsSquareIntegrable and IsAESquareIntegrable

structure ProbabilityTheory.IsSquareIntegrable {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} [LinearOrder ι] [TopologicalSpace ι] [NormedSpace ℝ E] (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 < ⊤

theorem ProbabilityTheory.IsSquareIntegrable.isRightContinuous {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [TopologicalSpace ι] {X : ι → Ω → E} {𝓕 : MeasureTheory.Filtration ι mΩ} [NormedSpace ℝ E] (hX : IsSquareIntegrable X 𝓕 P) (ω : Ω) : IsRightContinuous fun (x : ι) => X x ω

theorem ProbabilityTheory.IsSquareIntegrable.const {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [TopologicalSpace ι] {𝓕 : MeasureTheory.Filtration ι mΩ} [NormedSpace ℝ E] [MeasureTheory.IsFiniteMeasure P] {c : E} : IsSquareIntegrable (fun (x : ι) (x_1 : Ω) => c) 𝓕 P

theorem ProbabilityTheory.IsSquareIntegrable.uniformIntegrable {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [TopologicalSpace ι] {X : ι → Ω → E} {𝓕 : MeasureTheory.Filtration ι mΩ} [NormedSpace ℝ E] [MeasureTheory.IsFiniteMeasure P] (hX : IsSquareIntegrable X 𝓕 P) : MeasureTheory.UniformIntegrable X 1 P

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

An a.e.-square integrable martingale is a process that is indistinguishable from a square integrable martingale, see IsSquareIntegrable.

Equations

• ProbabilityTheory.IsAESquareIntegrable X 𝓕 P = ∃ (Y : ι → Ω → E), ProbabilityTheory.IsSquareIntegrable Y 𝓕 P ∧ X ≡ᵐ[P] Y

theorem ProbabilityTheory.IsSquareIntegrable.stronglyMeasurable_stoppedValue' {ι : 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 ι} [NormedSpace ℝ E] [OrderTopology ι] [OrderBot ι] [SecondCountableTopology ι] (hX : IsSquareIntegrable X 𝓕 P) (hτ : MeasureTheory.IsStoppingTime 𝓕 τ) : MeasureTheory.StronglyMeasurable (MeasureTheory.Filtration.stoppedValue' X τ 𝓕 P)

theorem ProbabilityTheory.IsAESquareIntegrable.aestronglyMeasurable_stoppedValue' {ι : 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 ι} [NormedSpace ℝ E] [OrderTopology ι] [OrderBot ι] [SecondCountableTopology ι] (hX : IsAESquareIntegrable X 𝓕 P) (hτ : MeasureTheory.IsStoppingTime 𝓕 τ) : MeasureTheory.AEStronglyMeasurable (MeasureTheory.Filtration.stoppedValue' X τ 𝓕 P) P

theorem ProbabilityTheory.IsAESquareIntegrable.uniformIntegrable {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [TopologicalSpace ι] {X : ι → Ω → E} {𝓕 : MeasureTheory.Filtration ι mΩ} [NormedSpace ℝ E] [MeasureTheory.IsFiniteMeasure P] (hX : IsAESquareIntegrable X 𝓕 P) : MeasureTheory.UniformIntegrable X 1 P

theorem ProbabilityTheory.IsAESquareIntegrable.aestronglyAdapted {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [TopologicalSpace ι] {X : ι → Ω → E} {𝓕 : MeasureTheory.Filtration ι mΩ} [NormedSpace ℝ E] (hX : IsAESquareIntegrable X 𝓕 P) : MeasureTheory.AEStronglyAdapted X 𝓕 P

theorem ProbabilityTheory.IsSquareIntegrable.isAESquareIntegrable {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [TopologicalSpace ι] {X : ι → Ω → E} {𝓕 : MeasureTheory.Filtration ι mΩ} [NormedSpace ℝ E] (hX : IsSquareIntegrable X 𝓕 P) : IsAESquareIntegrable X 𝓕 P

theorem ProbabilityTheory.IsAESquareIntegrable.const {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [TopologicalSpace ι] {𝓕 : MeasureTheory.Filtration ι mΩ} [NormedSpace ℝ E] [MeasureTheory.IsFiniteMeasure P] {c : E} : IsAESquareIntegrable (fun (x : ι) (x_1 : Ω) => c) 𝓕 P

theorem ProbabilityTheory.IsAESquareIntegrable.congr {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [TopologicalSpace ι] {𝓕 : MeasureTheory.Filtration ι mΩ} [NormedSpace ℝ E] {X Y : ι → Ω → E} (hX : IsAESquareIntegrable X 𝓕 P) (hXY : X ≡ᵐ[P] Y) : IsAESquareIntegrable Y 𝓕 P

theorem ProbabilityTheory.isAESquareIntegrable_congr {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [TopologicalSpace ι] {𝓕 : MeasureTheory.Filtration ι mΩ} [NormedSpace ℝ E] {X Y : ι → Ω → E} (hXY : X ≡ᵐ[P] Y) : IsAESquareIntegrable X 𝓕 P ↔ IsAESquareIntegrable Y 𝓕 P

theorem ProbabilityTheory.IsSquareIntegrable.memLp_two {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [TopologicalSpace ι] {X : ι → Ω → E} {𝓕 : MeasureTheory.Filtration ι mΩ} [NormedSpace ℝ E] (hX : IsSquareIntegrable X 𝓕 P) (i : ι) : MeasureTheory.MemLp (X i) 2 P

@[simp]

theorem ProbabilityTheory.stronglyAdapted_of_subsingleton_dom {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} [LinearOrder ι] [Subsingleton Ω] (X : ι → Ω → E) (𝓕 : MeasureTheory.Filtration ι mΩ) : MeasureTheory.StronglyAdapted 𝓕 X

@[simp]

theorem ProbabilityTheory.stronglyAdapted_of_subsingleton_cod {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} [LinearOrder ι] [Subsingleton E] (X : ι → Ω → E) (𝓕 : MeasureTheory.Filtration ι mΩ) : MeasureTheory.StronglyAdapted 𝓕 X

@[simp]

theorem ProbabilityTheory.martingale_of_isEmpty {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} [LinearOrder ι] [NormedSpace ℝ E] [IsEmpty Ω] (X : ι → Ω → E) (𝓕 : MeasureTheory.Filtration ι mΩ) (P : MeasureTheory.Measure Ω) : MeasureTheory.Martingale X 𝓕 P

@[simp]

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

theorem ProbabilityTheory.isSquareIntegrable_of_le_const {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [TopologicalSpace ι] {X : ι → Ω → E} {𝓕 : MeasureTheory.Filtration ι mΩ} [NormedSpace ℝ E] (h_mart : MeasureTheory.Martingale X 𝓕 P) (h_cadlag : ∀ (ω : Ω), IsCadlag fun (x : ι) => X x ω) {C : NNReal} (h_bound : ∀ (i : ι), MeasureTheory.eLpNorm (X i) 2 P ≤ ↑C) : IsSquareIntegrable X 𝓕 P

theorem ProbabilityTheory.IsSquareIntegrable.integrable_sq {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [TopologicalSpace ι] {X : ι → Ω → E} {𝓕 : MeasureTheory.Filtration ι mΩ} [NormedSpace ℝ E] (hX : IsSquareIntegrable X 𝓕 P) (i : ι) : MeasureTheory.Integrable (fun (ω : Ω) => ‖X i ω‖ ^ 2) P

theorem ProbabilityTheory.IsSquareIntegrable.add {ι : 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Ω} [NormedSpace ℝ E] [CompleteSpace E] (hX : IsSquareIntegrable X 𝓕 P) (hY : IsSquareIntegrable Y 𝓕 P) : IsSquareIntegrable (X + Y) 𝓕 P

theorem ProbabilityTheory.IsSquareIntegrable.fun_add {ι : 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Ω} [NormedSpace ℝ E] [CompleteSpace E] (hX : IsSquareIntegrable X 𝓕 P) (hY : IsSquareIntegrable Y 𝓕 P) : IsSquareIntegrable (fun (i : ι) (i_1 : Ω) => X i i_1 + Y i i_1) 𝓕 P

Eta-expanded form of ProbabilityTheory.IsSquareIntegrable.add

theorem ProbabilityTheory.IsAESquareIntegrable.add {ι : 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Ω} [NormedSpace ℝ E] [CompleteSpace E] (hX : IsAESquareIntegrable X 𝓕 P) (hY : IsAESquareIntegrable Y 𝓕 P) : IsAESquareIntegrable (X + Y) 𝓕 P

theorem ProbabilityTheory.IsAESquareIntegrable.fun_add {ι : 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Ω} [NormedSpace ℝ E] [CompleteSpace E] (hX : IsAESquareIntegrable X 𝓕 P) (hY : IsAESquareIntegrable Y 𝓕 P) : IsAESquareIntegrable (fun (i : ι) (i_1 : Ω) => X i i_1 + Y i i_1) 𝓕 P

Eta-expanded form of ProbabilityTheory.IsAESquareIntegrable.add

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

theorem ProbabilityTheory.IsSquareIntegrable.fun_smul {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [TopologicalSpace ι] {X : ι → Ω → E} {𝓕 : MeasureTheory.Filtration ι mΩ} [NormedSpace ℝ E] [CompleteSpace E] (hX : IsSquareIntegrable X 𝓕 P) (r : ℝ) : IsSquareIntegrable (fun (i : ι) (i_1 : Ω) => r • X i i_1) 𝓕 P

Eta-expanded form of ProbabilityTheory.IsSquareIntegrable.smul

theorem ProbabilityTheory.IsAESquareIntegrable.smul {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [TopologicalSpace ι] {X : ι → Ω → E} {𝓕 : MeasureTheory.Filtration ι mΩ} [NormedSpace ℝ E] [CompleteSpace E] (hX : IsAESquareIntegrable X 𝓕 P) (r : ℝ) : IsAESquareIntegrable (r • X) 𝓕 P

theorem ProbabilityTheory.IsAESquareIntegrable.fun_smul {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [TopologicalSpace ι] {X : ι → Ω → E} {𝓕 : MeasureTheory.Filtration ι mΩ} [NormedSpace ℝ E] [CompleteSpace E] (hX : IsAESquareIntegrable X 𝓕 P) (r : ℝ) : IsAESquareIntegrable (fun (i : ι) (i_1 : Ω) => r • X i i_1) 𝓕 P

Eta-expanded form of ProbabilityTheory.IsAESquareIntegrable.smul

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

theorem ProbabilityTheory.IsSquareIntegrable.fun_neg {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [TopologicalSpace ι] {X : ι → Ω → E} {𝓕 : MeasureTheory.Filtration ι mΩ} [NormedSpace ℝ E] [CompleteSpace E] (hX : IsSquareIntegrable X 𝓕 P) : IsSquareIntegrable (fun (i : ι) (i_1 : Ω) => -X i i_1) 𝓕 P

Eta-expanded form of ProbabilityTheory.IsSquareIntegrable.neg

theorem ProbabilityTheory.IsAESquareIntegrable.neg {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [TopologicalSpace ι] {X : ι → Ω → E} {𝓕 : MeasureTheory.Filtration ι mΩ} [NormedSpace ℝ E] [CompleteSpace E] (hX : IsAESquareIntegrable X 𝓕 P) : IsAESquareIntegrable (-X) 𝓕 P

theorem ProbabilityTheory.IsAESquareIntegrable.fun_neg {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [TopologicalSpace ι] {X : ι → Ω → E} {𝓕 : MeasureTheory.Filtration ι mΩ} [NormedSpace ℝ E] [CompleteSpace E] (hX : IsAESquareIntegrable X 𝓕 P) : IsAESquareIntegrable (fun (i : ι) (i_1 : Ω) => -X i i_1) 𝓕 P

Eta-expanded form of ProbabilityTheory.IsAESquareIntegrable.neg

theorem ProbabilityTheory.IsSquareIntegrable.sub {ι : 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Ω} [NormedSpace ℝ E] [CompleteSpace E] (hX : IsSquareIntegrable X 𝓕 P) (hY : IsSquareIntegrable Y 𝓕 P) : IsSquareIntegrable (X - Y) 𝓕 P

theorem ProbabilityTheory.IsSquareIntegrable.fun_sub {ι : 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Ω} [NormedSpace ℝ E] [CompleteSpace E] (hX : IsSquareIntegrable X 𝓕 P) (hY : IsSquareIntegrable Y 𝓕 P) : IsSquareIntegrable (fun (i : ι) (i_1 : Ω) => X i i_1 - Y i i_1) 𝓕 P

Eta-expanded form of ProbabilityTheory.IsSquareIntegrable.sub

theorem ProbabilityTheory.IsAESquareIntegrable.sub {ι : 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Ω} [NormedSpace ℝ E] [CompleteSpace E] (hX : IsAESquareIntegrable X 𝓕 P) (hY : IsAESquareIntegrable Y 𝓕 P) : IsAESquareIntegrable (X - Y) 𝓕 P

theorem ProbabilityTheory.IsAESquareIntegrable.fun_sub {ι : 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Ω} [NormedSpace ℝ E] [CompleteSpace E] (hX : IsAESquareIntegrable X 𝓕 P) (hY : IsAESquareIntegrable Y 𝓕 P) : IsAESquareIntegrable (fun (i : ι) (i_1 : Ω) => X i i_1 - Y i i_1) 𝓕 P

Eta-expanded form of ProbabilityTheory.IsAESquareIntegrable.sub

noncomputable def ProbabilityTheory.IsAESquareIntegrable.toContinuous {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [TopologicalSpace ι] {𝓕 : MeasureTheory.Filtration ι mΩ} [NormedSpace ℝ E] (X : ι → Ω → E) (hX : IsAESquareIntegrable X 𝓕 P) (t : ι) (ω : Ω) : E

If hX : IsAESquareIntegrable X 𝓕 P and ∀ᵐ ω ∂P, Continuous (X · ω), then hX.toContinuous X is continuous everywhere, satisfies IsSquareIntegrable and is indistinguishable from X.

Equations

• ProbabilityTheory.IsAESquareIntegrable.toContinuous X hX t ω = if Continuous fun (x : ι) => Exists.choose hX x ω then Exists.choose hX t ω else 0

theorem ProbabilityTheory.IsAESquareIntegrable.continuous_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Ω} [NormedSpace ℝ E] (hX : IsAESquareIntegrable X 𝓕 P) (ω : Ω) : Continuous fun (x : ι) => toContinuous X hX x ω

theorem ProbabilityTheory.IsAESquareIntegrable.indist_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Ω} [NormedSpace ℝ E] (hX1 : ∀ᵐ (ω : Ω) ∂P, Continuous fun (x : ι) => X x ω) (hX2 : IsAESquareIntegrable X 𝓕 P) : X ≡ᵐ[P] toContinuous X hX2

theorem ProbabilityTheory.IsSquareIntegrable.submartingale_sq_norm {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [TopologicalSpace ι] {X : ι → Ω → E} {𝓕 : MeasureTheory.Filtration ι mΩ} [NormedSpace ℝ E] [MeasureTheory.SigmaFiniteFiltration P 𝓕] [CompleteSpace E] (hX : IsSquareIntegrable X 𝓕 P) : MeasureTheory.Submartingale (fun (i : ι) (ω : Ω) => ‖X i ω‖ ^ 2) 𝓕 P

theorem ProbabilityTheory.IsSquareIntegrable.eLpNorm_mono {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [TopologicalSpace ι] {X : ι → Ω → E} {𝓕 : MeasureTheory.Filtration ι mΩ} [NormedSpace ℝ E] [MeasureTheory.SigmaFiniteFiltration P 𝓕] [CompleteSpace E] (hX : IsSquareIntegrable X 𝓕 P) {i j : ι} (hij : i ≤ j) : MeasureTheory.eLpNorm (X i) 2 P ≤ MeasureTheory.eLpNorm (X j) 2 P

theorem ProbabilityTheory.IsSquareIntegrable.ae_tendsto_limitProcess {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [TopologicalSpace ι] {X : ι → Ω → E} {𝓕 : MeasureTheory.Filtration ι mΩ} [NormedSpace ℝ E] [MeasureTheory.IsFiniteMeasure P] (hX : IsSquareIntegrable X 𝓕 P) : ∀ᵐ (ω : Ω) ∂P, Filter.Tendsto (fun (x : ι) => X x ω) Filter.atTop (nhds (MeasureTheory.Filtration.limitProcess X 𝓕 P ω))

theorem ProbabilityTheory.IsAESquareIntegrable.ae_tendsto_limitProcess {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [TopologicalSpace ι] {X : ι → Ω → E} {𝓕 : MeasureTheory.Filtration ι mΩ} [NormedSpace ℝ E] [MeasureTheory.IsFiniteMeasure P] (hX : IsAESquareIntegrable X 𝓕 P) : ∀ᵐ (ω : Ω) ∂P, Filter.Tendsto (fun (x : ι) => X x ω) Filter.atTop (nhds (MeasureTheory.Filtration.limitProcess X 𝓕 P ω))

theorem ProbabilityTheory.IsSquareIntegrable.limitProcess_add {ι : 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Ω} [NormedSpace ℝ E] [Nonempty ι] [MeasureTheory.IsFiniteMeasure P] (hX : IsSquareIntegrable X 𝓕 P) (hY : IsSquareIntegrable Y 𝓕 P) : MeasureTheory.Filtration.limitProcess (X + Y) 𝓕 P =ᵐ[P] MeasureTheory.Filtration.limitProcess X 𝓕 P + MeasureTheory.Filtration.limitProcess Y 𝓕 P

theorem ProbabilityTheory.IsSquareIntegrable.limitProcess_fun_add {ι : 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Ω} [NormedSpace ℝ E] [Nonempty ι] [MeasureTheory.IsFiniteMeasure P] (hX : IsSquareIntegrable X 𝓕 P) (hY : IsSquareIntegrable Y 𝓕 P) : MeasureTheory.Filtration.limitProcess (fun (i : ι) (i_1 : Ω) => X i i_1 + Y i i_1) 𝓕 P =ᵐ[P] fun (i : Ω) => MeasureTheory.Filtration.limitProcess X 𝓕 P i + MeasureTheory.Filtration.limitProcess Y 𝓕 P i

Eta-expanded form of ProbabilityTheory.IsSquareIntegrable.limitProcess_add

theorem ProbabilityTheory.IsSquareIntegrable.limitProcess_sub {ι : 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Ω} [NormedSpace ℝ E] [Nonempty ι] [MeasureTheory.IsFiniteMeasure P] (hX : IsSquareIntegrable X 𝓕 P) (hY : IsSquareIntegrable Y 𝓕 P) : MeasureTheory.Filtration.limitProcess (X - Y) 𝓕 P =ᵐ[P] MeasureTheory.Filtration.limitProcess X 𝓕 P - MeasureTheory.Filtration.limitProcess Y 𝓕 P

theorem ProbabilityTheory.IsSquareIntegrable.limitProcess_fun_sub {ι : 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Ω} [NormedSpace ℝ E] [Nonempty ι] [MeasureTheory.IsFiniteMeasure P] (hX : IsSquareIntegrable X 𝓕 P) (hY : IsSquareIntegrable Y 𝓕 P) : MeasureTheory.Filtration.limitProcess (fun (i : ι) (i_1 : Ω) => X i i_1 - Y i i_1) 𝓕 P =ᵐ[P] fun (i : Ω) => MeasureTheory.Filtration.limitProcess X 𝓕 P i - MeasureTheory.Filtration.limitProcess Y 𝓕 P i

Eta-expanded form of ProbabilityTheory.IsSquareIntegrable.limitProcess_sub

theorem ProbabilityTheory.IsAESquareIntegrable.limitProcess_add {ι : 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Ω} [NormedSpace ℝ E] [Nonempty ι] [MeasureTheory.IsFiniteMeasure P] (hX : IsAESquareIntegrable X 𝓕 P) (hY : IsAESquareIntegrable Y 𝓕 P) : MeasureTheory.Filtration.limitProcess (X + Y) 𝓕 P =ᵐ[P] MeasureTheory.Filtration.limitProcess X 𝓕 P + MeasureTheory.Filtration.limitProcess Y 𝓕 P

theorem ProbabilityTheory.IsAESquareIntegrable.limitProcess_fun_add {ι : 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Ω} [NormedSpace ℝ E] [Nonempty ι] [MeasureTheory.IsFiniteMeasure P] (hX : IsAESquareIntegrable X 𝓕 P) (hY : IsAESquareIntegrable Y 𝓕 P) : MeasureTheory.Filtration.limitProcess (fun (i : ι) (i_1 : Ω) => X i i_1 + Y i i_1) 𝓕 P =ᵐ[P] fun (i : Ω) => MeasureTheory.Filtration.limitProcess X 𝓕 P i + MeasureTheory.Filtration.limitProcess Y 𝓕 P i

Eta-expanded form of ProbabilityTheory.IsAESquareIntegrable.limitProcess_add

theorem ProbabilityTheory.IsAESquareIntegrable.limitProcess_sub {ι : 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Ω} [NormedSpace ℝ E] [Nonempty ι] [MeasureTheory.IsFiniteMeasure P] (hX : IsAESquareIntegrable X 𝓕 P) (hY : IsAESquareIntegrable Y 𝓕 P) : MeasureTheory.Filtration.limitProcess (X - Y) 𝓕 P =ᵐ[P] MeasureTheory.Filtration.limitProcess X 𝓕 P - MeasureTheory.Filtration.limitProcess Y 𝓕 P

theorem ProbabilityTheory.IsAESquareIntegrable.limitProcess_fun_sub {ι : 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Ω} [NormedSpace ℝ E] [Nonempty ι] [MeasureTheory.IsFiniteMeasure P] (hX : IsAESquareIntegrable X 𝓕 P) (hY : IsAESquareIntegrable Y 𝓕 P) : MeasureTheory.Filtration.limitProcess (fun (i : ι) (i_1 : Ω) => X i i_1 - Y i i_1) 𝓕 P =ᵐ[P] fun (i : Ω) => MeasureTheory.Filtration.limitProcess X 𝓕 P i - MeasureTheory.Filtration.limitProcess Y 𝓕 P i

Eta-expanded form of ProbabilityTheory.IsAESquareIntegrable.limitProcess_sub

theorem ProbabilityTheory.tendsto_ae_condExp' {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [TopologicalSpace ι] (𝓕 : MeasureTheory.Filtration ι mΩ) [NormedSpace ℝ E] (X : Ω → E) : ∀ᵐ (ω : Ω) ∂P, Filter.Tendsto (fun (x : ι) => P[X | ↑𝓕 x] ω) Filter.atTop (nhds (P[X | ⨆ (t : ι), ↑𝓕 t] ω))

theorem ProbabilityTheory.IsSquareIntegrable.condExp_limitProcess_ae_eq {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [TopologicalSpace ι] {X : ι → Ω → E} {𝓕 : MeasureTheory.Filtration ι mΩ} [NormedSpace ℝ E] [MeasureTheory.IsFiniteMeasure P] (hX : IsSquareIntegrable X 𝓕 P) (t : ι) : P[MeasureTheory.Filtration.limitProcess X 𝓕 P | ↑𝓕 t] =ᵐ[P] X t

theorem ProbabilityTheory.IsSquareIntegrable.condExp_limitProcess_ae_eq' {ι : 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 ι} [NormedSpace ℝ E] [MeasureTheory.IsFiniteMeasure P] (hX : IsSquareIntegrable X 𝓕 P) (hτ : MeasureTheory.IsStoppingTime 𝓕 τ) : P[MeasureTheory.Filtration.limitProcess X 𝓕 P | hτ.measurableSpace] =ᵐ[P] MeasureTheory.Filtration.stoppedValue' X τ 𝓕 P

theorem ProbabilityTheory.IsAESquareIntegrable.condExp_limitProcess_ae_eq {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [TopologicalSpace ι] {X : ι → Ω → E} {𝓕 : MeasureTheory.Filtration ι mΩ} [NormedSpace ℝ E] [MeasureTheory.IsFiniteMeasure P] [CompleteSpace E] (hX : IsAESquareIntegrable X 𝓕 P) (t : ι) : P[MeasureTheory.Filtration.limitProcess X 𝓕 P | ↑𝓕 t] =ᵐ[P] X t

theorem ProbabilityTheory.IsAESquareIntegrable.condExp_limitProcess_ae_eq' {ι : 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 ι} [NormedSpace ℝ E] [MeasureTheory.IsFiniteMeasure P] [CompleteSpace E] (hX : IsAESquareIntegrable X 𝓕 P) (hτ : MeasureTheory.IsStoppingTime 𝓕 τ) : P[MeasureTheory.Filtration.limitProcess X 𝓕 P | hτ.measurableSpace] =ᵐ[P] MeasureTheory.Filtration.stoppedValue' X τ 𝓕 P

theorem ProbabilityTheory.IsSquareIntegrable.tendsto_eLpNorm_two_limitProcess {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [TopologicalSpace ι] {X : ι → Ω → E} {𝓕 : MeasureTheory.Filtration ι mΩ} [NormedSpace ℝ E] (hX : IsSquareIntegrable X 𝓕 P) : Filter.Tendsto (fun (i : ι) => MeasureTheory.eLpNorm (X i - MeasureTheory.Filtration.limitProcess X 𝓕 P) 2 P) Filter.atTop (nhds 0)

theorem ProbabilityTheory.isSquareIntegrable_of_limitProcess {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [TopologicalSpace ι] {X : ι → Ω → E} {𝓕 : MeasureTheory.Filtration ι mΩ} [NormedSpace ℝ E] [CompleteSpace E] (hX1 : MeasureTheory.Martingale X 𝓕 P) (hX2 : MeasureTheory.UniformIntegrable X 1 P) (hX3 : ∀ (ω : Ω), IsCadlag fun (x : ι) => X x ω) (hX4 : MeasureTheory.MemLp (MeasureTheory.Filtration.limitProcess X 𝓕 P) 2 P) : IsSquareIntegrable X 𝓕 P

theorem ProbabilityTheory.IsSquareIntegrable.iSup_eLpNorm_eq_eLpNorm_limitProcess {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [TopologicalSpace ι] {X : ι → Ω → E} {𝓕 : MeasureTheory.Filtration ι mΩ} [NormedSpace ℝ E] (hX : IsSquareIntegrable X 𝓕 P) : ⨆ (i : ι), MeasureTheory.eLpNorm (X i) 2 P = MeasureTheory.eLpNorm (MeasureTheory.Filtration.limitProcess X 𝓕 P) 2 P

theorem ProbabilityTheory.IsSquareIntegrable.iSup_lintegral_pow_two_eq {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [TopologicalSpace ι] {X : ι → Ω → E} {𝓕 : MeasureTheory.Filtration ι mΩ} [NormedSpace ℝ E] (hX : IsSquareIntegrable X 𝓕 P) : ⨆ (t : ι), ∫⁻ (ω : Ω), ‖X t ω‖ₑ ^ 2 ∂P = ∫⁻ (ω : Ω), ‖MeasureTheory.Filtration.limitProcess X 𝓕 P ω‖ₑ ^ 2 ∂P

theorem ProbabilityTheory.IsAESquareIntegrable.iSup_eLpNorm_eq_eLpNorm_limitProcess {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [TopologicalSpace ι] {X : ι → Ω → E} {𝓕 : MeasureTheory.Filtration ι mΩ} [NormedSpace ℝ E] (hX : IsAESquareIntegrable X 𝓕 P) : ⨆ (i : ι), MeasureTheory.eLpNorm (X i) 2 P = MeasureTheory.eLpNorm (MeasureTheory.Filtration.limitProcess X 𝓕 P) 2 P

theorem ProbabilityTheory.IsSquareIntegrable.memLp_limitProcess {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [TopologicalSpace ι] {X : ι → Ω → E} {𝓕 : MeasureTheory.Filtration ι mΩ} [NormedSpace ℝ E] (hX : IsSquareIntegrable X 𝓕 P) : MeasureTheory.MemLp (MeasureTheory.Filtration.limitProcess X 𝓕 P) 2 P

theorem ProbabilityTheory.IsAESquareIntegrable.memLp_limitProcess {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [TopologicalSpace ι] {X : ι → Ω → E} {𝓕 : MeasureTheory.Filtration ι mΩ} [NormedSpace ℝ E] (hX : IsAESquareIntegrable X 𝓕 P) : MeasureTheory.MemLp (MeasureTheory.Filtration.limitProcess X 𝓕 P) 2 P

theorem ProbabilityTheory.IsSquareIntegrable.integral_iSup_norm_rpow_rpow_inv_le_limitProcess {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [TopologicalSpace ι] {X : ι → Ω → E} {𝓕 : MeasureTheory.Filtration ι mΩ} [NormedSpace ℝ E] [OrderTopology ι] [SecondCountableTopology ι] [CompleteSpace E] [MeasureTheory.IsFiniteMeasure P] (hX : IsSquareIntegrable X 𝓕 P) : (∫⁻ (ω : Ω), (⨆ (t : ι), ‖X t ω‖ₑ) ^ 2 ∂P) ^ (1 / 2) ≤ 2 * MeasureTheory.eLpNorm (MeasureTheory.Filtration.limitProcess X 𝓕 P) 2 P

theorem ProbabilityTheory.IsAESquareIntegrable.integral_iSup_norm_rpow_rpow_inv_le_limitProcess {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [TopologicalSpace ι] {X : ι → Ω → E} {𝓕 : MeasureTheory.Filtration ι mΩ} [NormedSpace ℝ E] [OrderTopology ι] [SecondCountableTopology ι] [CompleteSpace E] [MeasureTheory.IsFiniteMeasure P] (hX : IsAESquareIntegrable X 𝓕 P) : (∫⁻ (ω : Ω), (⨆ (t : ι), ‖X t ω‖ₑ) ^ 2 ∂P) ^ (1 / 2) ≤ 2 * MeasureTheory.eLpNorm (MeasureTheory.Filtration.limitProcess X 𝓕 P) 2 P

theorem ProbabilityTheory.IsSquareIntegrable.limitProcess_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 ι} [NormedSpace ℝ E] [OrderTopology ι] [SecondCountableTopology ι] [OrderBot ι] [MeasureTheory.IsFiniteMeasure P] (hX : IsSquareIntegrable X 𝓕 P) (hτ : MeasureTheory.IsStoppingTime 𝓕 τ) : MeasureTheory.Filtration.limitProcess (MeasureTheory.stoppedProcess X τ) 𝓕 P =ᵐ[P] MeasureTheory.Filtration.stoppedValue' X τ 𝓕 P

theorem ProbabilityTheory.IsAESquareIntegrable.limitProcess_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 ι} [NormedSpace ℝ E] [OrderTopology ι] [SecondCountableTopology ι] [OrderBot ι] [MeasureTheory.IsFiniteMeasure P] (hX : IsAESquareIntegrable X 𝓕 P) (hτ : MeasureTheory.IsStoppingTime 𝓕 τ) : MeasureTheory.Filtration.limitProcess (MeasureTheory.stoppedProcess X τ) 𝓕 P =ᵐ[P] MeasureTheory.Filtration.stoppedValue' X τ 𝓕 P

theorem ProbabilityTheory.IsSquareIntegrable.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 ι} [NormedSpace ℝ E] [OrderTopology ι] [SecondCountableTopology ι] [OrderBot ι] [MeasureTheory.IsFiniteMeasure P] [CompleteSpace E] [MeasureTheory.Approximable 𝓕 P] (hX : IsSquareIntegrable X 𝓕 P) (hτ : MeasureTheory.IsStoppingTime 𝓕 τ) : IsSquareIntegrable (MeasureTheory.stoppedProcess X τ) 𝓕 P

theorem ProbabilityTheory.IsAESquareIntegrable.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 ι} [NormedSpace ℝ E] [OrderTopology ι] [SecondCountableTopology ι] [OrderBot ι] [MeasureTheory.IsFiniteMeasure P] [CompleteSpace E] [MeasureTheory.Approximable 𝓕 P] (hX : IsAESquareIntegrable X 𝓕 P) (hτ : MeasureTheory.IsStoppingTime 𝓕 τ) : IsAESquareIntegrable (MeasureTheory.stoppedProcess X τ) 𝓕 P

theorem ProbabilityTheory.IsAESquareIntegrable.memLp_two_stoppedValue' {ι : 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 ι} [NormedSpace ℝ E] [OrderTopology ι] [SecondCountableTopology ι] [OrderBot ι] [MeasureTheory.IsFiniteMeasure P] [CompleteSpace E] [MeasureTheory.Approximable 𝓕 P] (hX : IsAESquareIntegrable X 𝓕 P) (hτ : MeasureTheory.IsStoppingTime 𝓕 τ) : MeasureTheory.MemLp (MeasureTheory.Filtration.stoppedValue' X τ 𝓕 P) 2 P

The Hilbert space of square integrable martingales

def ProbabilityTheory.IsPurelyDiscontinuous {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} [LinearOrder ι] [TopologicalSpace ι] [InnerProductSpace ℝ E] (X : ι → Ω → E) (𝓕 : MeasureTheory.Filtration ι mΩ) (P : MeasureTheory.Measure Ω) : Prop

A process is a purely discontinuous square integrable martingale if it is square integrable and orthogonal to every continuous square integrable martingale in the Hilbert space of square integrable martingales.

Equations

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

theorem ProbabilityTheory.IsPurelyDiscontinuous.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Ω} [InnerProductSpace ℝ E] (hX : IsPurelyDiscontinuous X 𝓕 P) (h : X ≡ᵐ[P] Y) : IsPurelyDiscontinuous Y 𝓕 P

def ProbabilityTheory.squareIntegrableSubmodule {ι : 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 ℝ (Ω →ₚ[P, 𝓕] E)

The type of square integrable martingales, as a submodule of equivalence classes of indistinguishable processes.

Equations

• ProbabilityTheory.squareIntegrableSubmodule E P 𝓕 = { carrier := {X : Ω →ₚ[P, 𝓕] E | ProbabilityTheory.IsAESquareIntegrable (↑X) 𝓕 P}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

def ProbabilityTheory.SquareIntegrable {ι : 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] : Type (max (max u_1 u_2) u_3)

The type of square integrable martingales up to indistinguishability.

Equations

• ProbabilityTheory.SquareIntegrable E P 𝓕 = ↥(ProbabilityTheory.squareIntegrableSubmodule E P 𝓕)

@[instance_reducible]

instance ProbabilityTheory.instAddCommGroupSquareIntegrable {ι : 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] : AddCommGroup (SquareIntegrable E P 𝓕)

Equations

• ProbabilityTheory.instAddCommGroupSquareIntegrable = AddSubgroupClass.toAddCommGroup (ProbabilityTheory.squareIntegrableSubmodule E P 𝓕)

@[instance_reducible]

instance ProbabilityTheory.instModuleRealSquareIntegrable {ι : 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] : Module ℝ (SquareIntegrable E P 𝓕)

Equations

• ProbabilityTheory.instModuleRealSquareIntegrable = (ProbabilityTheory.squareIntegrableSubmodule E P 𝓕).module

noncomputable def ProbabilityTheory.SquareIntegrable.mk {ι : 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 : ι → Ω → E) (hX : IsAESquareIntegrable X 𝓕 P) : SquareIntegrable E P 𝓕

The equivalence class of a process that is indistinguishable from a square integrable martingale.

Equations

• ProbabilityTheory.SquareIntegrable.mk X hX = ⟨MeasureTheory.AEEqProcess.mk X ⋯, ⋯⟩

noncomputable def ProbabilityTheory.SquareIntegrable.out {ι : 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 𝓕) : ι → Ω → E

Given an equivalence class of square integrable martingales, this is a version that satisfies IsSquareIntegrable. Don't use this directly, use the coercion system instead.

Equations

• ↑X = if h : ∃ (Y : ι → Ω → E), (∀ (ω : Ω), Continuous fun (x : ι) => Y x ω) ∧ ProbabilityTheory.IsSquareIntegrable Y 𝓕 P ∧ ↑↑X ≡ᵐ[P] Y then h.choose else Exists.choose ⋯

@[instance_reducible]

noncomputable instance ProbabilityTheory.instCoeFunSquareIntegrableForallForall {ι : 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] : CoeFun (SquareIntegrable E P 𝓕) fun (x : SquareIntegrable E P 𝓕) => ι → Ω → E

Equations

• ProbabilityTheory.instCoeFunSquareIntegrableForallForall = { coe := ProbabilityTheory.SquareIntegrable.out }

theorem ProbabilityTheory.SquareIntegrable.isSquareIntegrable_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 𝓕) : IsSquareIntegrable (↑X) 𝓕 P

theorem ProbabilityTheory.SquareIntegrable.isAESquareIntegrable_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 𝓕) : IsAESquareIntegrable (↑X) 𝓕 P

theorem ProbabilityTheory.SquareIntegrable.val_indist_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 𝓕) : ↑↑X ≡ᵐ[P] ↑X

theorem ProbabilityTheory.SquareIntegrable.ext {ι : 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 Y : SquareIntegrable E P 𝓕} (h : ↑X ≡ᵐ[P] ↑Y) : X = Y

theorem ProbabilityTheory.SquareIntegrable.ext_iff {ι : 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 Y : SquareIntegrable E P 𝓕} : X = Y ↔ ↑X ≡ᵐ[P] ↑Y

theorem ProbabilityTheory.SquareIntegrable.coe_add {ι : 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 Y : SquareIntegrable E P 𝓕) : ↑(X + Y) ≡ᵐ[P] ↑X + ↑Y

theorem ProbabilityTheory.SquareIntegrable.coe_sub {ι : 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 Y : SquareIntegrable E P 𝓕) : ↑(X - Y) ≡ᵐ[P] ↑X - ↑Y

theorem ProbabilityTheory.SquareIntegrable.coe_smul {ι : 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 𝓕) (c : ℝ) : ↑(c • X) ≡ᵐ[P] c • ↑X

theorem ProbabilityTheory.SquareIntegrable.coe_neg {ι : 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 𝓕) : ↑(-X) ≡ᵐ[P] -↑X

theorem ProbabilityTheory.SquareIntegrable.mk_indist {ι : 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] (hX : IsAESquareIntegrable X 𝓕 P) : ↑(mk X hX) ≡ᵐ[P] X

theorem ProbabilityTheory.SquareIntegrable.mk_eq_mk {ι : 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] [NormedSpace ℝ E] {hX : IsAESquareIntegrable X 𝓕 P} {hY : IsAESquareIntegrable Y 𝓕 P} : mk X hX = mk Y hY ↔ X ≡ᵐ[P] Y

theorem ProbabilityTheory.SquareIntegrable.mk_add {ι : 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] [NormedSpace ℝ E] {hX : IsAESquareIntegrable X 𝓕 P} {hY : IsAESquareIntegrable Y 𝓕 P} : mk (X + Y) ⋯ = mk X hX + mk Y hY

theorem ProbabilityTheory.SquareIntegrable.mk_sub {ι : 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] [NormedSpace ℝ E] {hX : IsAESquareIntegrable X 𝓕 P} {hY : IsAESquareIntegrable Y 𝓕 P} : mk (X - Y) ⋯ = mk X hX - mk Y hY

theorem ProbabilityTheory.SquareIntegrable.coe_const {ι : 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] (c : E) : ↑(mk (fun (x : ι) (x_1 : Ω) => c) ⋯) ≡ᵐ[P] fun (x : ι) (x_1 : Ω) => c

theorem ProbabilityTheory.SquareIntegrable.coe_zero {ι : 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] : ↑0 ≡ᵐ[P] 0

theorem ProbabilityTheory.indistinguishable_of_modification' {T : Type u_4} {Ω : Type u_5} {E : Type u_6} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X Y : T → Ω → E} [TopologicalSpace E] [TopologicalSpace T] [TopologicalSpace.SeparableSpace T] [T2Space E] [Preorder T] (hX : ∀ᵐ (ω : Ω) ∂P, IsRightContinuous fun (x : T) => X x ω) (hY : ∀ᵐ (ω : Ω) ∂P, IsRightContinuous fun (x : T) => Y x ω) (h : ∀ (t : T), X t =ᵐ[P] Y t) : X ≡ᵐ[P] Y

Two modifications that are right-continuous are indistinguishable.

noncomputable def ProbabilityTheory.SquareIntegrable.toL2 {ι : 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] [Nonempty ι] : SquareIntegrable E P 𝓕 →ₗ[ℝ] ↥(MeasureTheory.Lp E 2 P)

The injection of square integrable martingales into the L^2 space given by X ↦ X ∞. This is a LinearIsometryEquiv onto the subspace of functions that are strongly measurable with respect to ⨆ t, 𝓕 t, see SquareIntegrable.toL2Isom.

Equations

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

theorem ProbabilityTheory.SquareIntegrable.toL2_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] [NormedSpace ℝ E] [Nonempty ι] (X : SquareIntegrable E P 𝓕) : (toL2 E P 𝓕) X = MeasureTheory.MemLp.toLp (MeasureTheory.Filtration.limitProcess (↑X) 𝓕 P) ⋯

theorem ProbabilityTheory.SquareIntegrable.toL2_ae_eq {ι : 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] [Nonempty ι] (X : SquareIntegrable E P 𝓕) : ↑↑((toL2 E P 𝓕) X) =ᵐ[P] MeasureTheory.Filtration.limitProcess (↑X) 𝓕 P

theorem ProbabilityTheory.SquareIntegrable.injective_toL2 {ι : 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] [Nonempty ι] [TopologicalSpace.SeparableSpace ι] : Function.Injective ⇑(toL2 E P 𝓕)

@[instance_reducible]

noncomputable instance ProbabilityTheory.instNormedAddCommGroupSquareIntegrable {ι : 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] [Nonempty ι] [TopologicalSpace.SeparableSpace ι] : NormedAddCommGroup (SquareIntegrable E P 𝓕)

Equations

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

theorem ProbabilityTheory.SquareIntegrable.norm_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] [NormedSpace ℝ E] [Nonempty ι] [TopologicalSpace.SeparableSpace ι] {X : SquareIntegrable E P 𝓕} : ‖X‖ = MeasureTheory.lpNorm (MeasureTheory.Filtration.limitProcess (↑X) 𝓕 P) 2 P

theorem ProbabilityTheory.SquareIntegrable.enorm_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] [NormedSpace ℝ E] [Nonempty ι] [TopologicalSpace.SeparableSpace ι] {X : SquareIntegrable E P 𝓕} : ‖X‖ₑ = MeasureTheory.eLpNorm (MeasureTheory.Filtration.limitProcess (↑X) 𝓕 P) 2 P

@[instance_reducible]

noncomputable instance ProbabilityTheory.instInnerProductSpaceRealSquareIntegrable {ι : 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] [Nonempty ι] [TopologicalSpace.SeparableSpace ι] : InnerProductSpace ℝ (SquareIntegrable E P 𝓕)

Equations

• ProbabilityTheory.instInnerProductSpaceRealSquareIntegrable = InnerProductSpace.induced (ProbabilityTheory.SquareIntegrable.toL2 E P 𝓕)

theorem ProbabilityTheory.SquareIntegrable.inner_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] [Nonempty ι] [TopologicalSpace.SeparableSpace ι] {X Y : SquareIntegrable E P 𝓕} : inner ℝ X Y = ∫ (x : Ω), (fun (ω : Ω) => inner ℝ (MeasureTheory.Filtration.limitProcess (↑X) 𝓕 P ω) (MeasureTheory.Filtration.limitProcess (↑Y) 𝓕 P ω)) x ∂P

theorem ProbabilityTheory.IsAESquareIntegrable.inner_limitProcess_eq {ι : 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] [Nonempty ι] [TopologicalSpace.SeparableSpace ι] (hX : IsAESquareIntegrable X 𝓕 P) (hY : IsAESquareIntegrable Y 𝓕 P) : ∫ (x : Ω), (fun (ω : Ω) => inner ℝ (MeasureTheory.Filtration.limitProcess X 𝓕 P ω) (MeasureTheory.Filtration.limitProcess Y 𝓕 P ω)) x ∂P = inner ℝ (SquareIntegrable.mk X hX) (SquareIntegrable.mk Y hY)

theorem ProbabilityTheory.isSquareIntegrable_cadlagModif_condExp {ι : 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] [OrderTopology ι] [SecondCountableTopology ι] [OrderBot ι] [𝓕.IsRightContinuous] [𝓕.IsComplete P] {X : Ω → E} (hX : MeasureTheory.MemLp X 2 P) : IsSquareIntegrable (cadlagModif fun (t : ι) => P[X | ↑𝓕 t]) 𝓕 P

noncomputable def ProbabilityTheory.SquareIntegrable.toL2Isom {ι : 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] [Nonempty ι] [TopologicalSpace.SeparableSpace ι] [OrderTopology ι] [SecondCountableTopology ι] [OrderBot ι] [𝓕.IsRightContinuous] [𝓕.IsComplete P] : SquareIntegrable E P 𝓕 ≃ₗᵢ[ℝ] ↥(MeasureTheory.lpMeas E ℝ (⨆ (t : ι), ↑𝓕 t) 2 P)

The LinearIsometryEquiv between square integrable martingales and the type of L^2 random variables that are strongly measurable with respect to ⨆ t, 𝓕 t, given by X ↦ X ∞.

Equations

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

instance ProbabilityTheory.instCompleteSpaceSquareIntegrable {ι : 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] [Nonempty ι] [TopologicalSpace.SeparableSpace ι] [OrderTopology ι] [SecondCountableTopology ι] [OrderBot ι] [𝓕.IsRightContinuous] [𝓕.IsComplete P] : CompleteSpace (SquareIntegrable E P 𝓕)

def ProbabilityTheory.IsLocallySquareIntegrable {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} [LinearOrder ι] [TopologicalSpace ι] [NormedSpace ℝ E] [OrderBot ι] [OrderTopology ι] (X : ι → Ω → E) (𝓕 : MeasureTheory.Filtration ι mΩ) (P : MeasureTheory.Measure Ω := by volume_tac) : Prop

A stochastic process is locally square-integrable if it satisfies the square-integrable martingale property locally.

Equations

• ProbabilityTheory.IsLocallySquareIntegrable X 𝓕 P = ProbabilityTheory.Locally (fun (Y : ι → Ω → E) => ProbabilityTheory.IsSquareIntegrable Y 𝓕 P) 𝓕 X P

theorem ProbabilityTheory.IsSquareIntegrable.isLocallySquareIntegrable {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [TopologicalSpace ι] {X : ι → Ω → E} {𝓕 : MeasureTheory.Filtration ι mΩ} [NormedSpace ℝ E] [OrderBot ι] [OrderTopology ι] (hX : IsSquareIntegrable X 𝓕 P) : IsLocallySquareIntegrable X 𝓕 P

theorem ProbabilityTheory.IsLocallySquareIntegrable.isLocalSubmartingale_sq_norm {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [TopologicalSpace ι] {X : ι → Ω → E} {𝓕 : MeasureTheory.Filtration ι mΩ} [NormedSpace ℝ E] [MeasureTheory.SigmaFiniteFiltration P 𝓕] [OrderBot ι] [OrderTopology ι] [CompleteSpace E] (hX : IsLocallySquareIntegrable X 𝓕 P) : IsLocalSubmartingale (fun (t : ι) (ω : Ω) => ‖X t ω‖ ^ 2) 𝓕 P

A locally square-integrable martingale has locally submartingale squared norm.

@[simp]

theorem ProbabilityTheory.isLocallySquareIntegrable_of_isEmpty {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} [ConditionallyCompleteLinearOrderBot ι] [TopologicalSpace ι] [OrderTopology ι] [NormedSpace ℝ E] [IsEmpty Ω] (X : ι → Ω → E) (𝓕 : MeasureTheory.Filtration ι mΩ) (P : MeasureTheory.Measure Ω) : IsLocallySquareIntegrable X 𝓕 P

theorem MeasureTheory.Martingale.isLocallySquareIntegrable_of_jump_le {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {P : Measure Ω} [ConditionallyCompleteLinearOrderBot ι] [TopologicalSpace ι] [OrderTopology ι] [NormedSpace ℝ E] {X : ι → Ω → E} {𝓕 : Filtration ι mΩ} [𝓕.IsComplete P] [𝓕.IsRightContinuous] [IsFiniteMeasure P] [Approximable 𝓕 P] [PolishSpace ι] [CompleteSpace E] (hX : Martingale X 𝓕 P) (h_cadlag : ∀ (ω : Ω), IsCadlag fun (x : ι) => X x ω) {C : ℝ} (h_jump : ∀ (t : ι) (ω : Ω), ‖Function.jump (fun (x : ι) => X x ω) t‖ ≤ C) : ProbabilityTheory.IsLocallySquareIntegrable X 𝓕 P

theorem MeasureTheory.Martingale.isLocallySquareIntegrable_of_continuous {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {P : Measure Ω} [ConditionallyCompleteLinearOrderBot ι] [TopologicalSpace ι] [OrderTopology ι] [NormedSpace ℝ E] {X : ι → Ω → E} {𝓕 : Filtration ι mΩ} [𝓕.IsComplete P] [𝓕.IsRightContinuous] [IsFiniteMeasure P] [Approximable 𝓕 P] [PolishSpace ι] [CompleteSpace E] [DenselyOrdered ι] (hX : Martingale X 𝓕 P) (h_cont : ∀ (ω : Ω), Continuous fun (x : ι) => X x ω) : ProbabilityTheory.IsLocallySquareIntegrable X 𝓕 P

theorem ProbabilityTheory.isStable_isSquareIntegrable {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [ConditionallyCompleteLinearOrderBot ι] [TopologicalSpace ι] [OrderTopology ι] [NormedSpace ℝ E] {𝓕 : MeasureTheory.Filtration ι mΩ} [𝓕.IsComplete P] [𝓕.IsRightContinuous] [MeasureTheory.IsFiniteMeasure P] [MeasureTheory.Approximable 𝓕 P] [PolishSpace ι] [CompleteSpace E] [SecondCountableTopology E] : IsStable 𝓕 fun (X : ι → Ω → E) => IsSquareIntegrable X 𝓕 P

theorem ProbabilityTheory.isStable_jump_le {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} [ConditionallyCompleteLinearOrderBot ι] [TopologicalSpace ι] [OrderTopology ι] {𝓕 : MeasureTheory.Filtration ι mΩ} {C : ℝ} (hC : 0 ≤ C) : IsStable 𝓕 fun (X : ι → Ω → E) => ∀ (t : ι) (ω : Ω), ‖Function.jump (fun (x : ι) => X x ω) t‖ ≤ C

theorem ProbabilityTheory.locally_jump_le_iff {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [ConditionallyCompleteLinearOrderBot ι] [TopologicalSpace ι] [OrderTopology ι] {𝓕 : MeasureTheory.Filtration ι mΩ} [𝓕.IsComplete P] {C : ℝ} (hC : 0 ≤ C) {X : ι → Ω → E} : Locally (fun (X : ι → Ω → E) => ∀ (t : ι) (ω : Ω), ‖Function.jump (fun (x : ι) => X x ω) t‖ ≤ C) 𝓕 X P ↔ ∀ᵐ (ω : Ω) ∂P, ∀ (t : ι), ‖Function.jump (fun (x : ι) => X x ω) t‖ ≤ C

theorem ProbabilityTheory.IsLocalMartingale.isLocallySquareIntegrable_of_jump_le {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [ConditionallyCompleteLinearOrderBot ι] [TopologicalSpace ι] [OrderTopology ι] [NormedSpace ℝ E] {X : ι → Ω → E} {𝓕 : MeasureTheory.Filtration ι mΩ} [𝓕.IsComplete P] [𝓕.IsRightContinuous] [MeasureTheory.IsFiniteMeasure P] [MeasureTheory.Approximable 𝓕 P] [DenselyOrdered ι] [NoMaxOrder ι] [PolishSpace ι] [SecondCountableTopology E] [CompleteSpace E] (hX : IsLocalMartingale X 𝓕 P) {C : ℝ} (hC : 0 ≤ C) (h_jump : ∀ᵐ (ω : Ω) ∂P, ∀ (t : ι), ‖Function.jump (fun (x : ι) => X x ω) t‖ ≤ C) : IsLocallySquareIntegrable X 𝓕 P

theorem ProbabilityTheory.IsLocalMartingale.isLocallySquareIntegrable_of_continuous {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [ConditionallyCompleteLinearOrderBot ι] [TopologicalSpace ι] [OrderTopology ι] [NormedSpace ℝ E] {X : ι → Ω → E} {𝓕 : MeasureTheory.Filtration ι mΩ} [𝓕.IsComplete P] [𝓕.IsRightContinuous] [MeasureTheory.IsFiniteMeasure P] [MeasureTheory.Approximable 𝓕 P] [DenselyOrdered ι] [NoMaxOrder ι] [PolishSpace ι] [SecondCountableTopology E] [CompleteSpace E] (hX : IsLocalMartingale X 𝓕 P) (h_cont : ∀ᵐ (ω : Ω) ∂P, Continuous fun (x : ι) => X x ω) : IsLocallySquareIntegrable X 𝓕 P