Quadratic variation of locally square-integrable martingales

noncomputable def ProbabilityTheory.predQuadVariation {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] [MeasurableSpace ι] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {mΩ : MeasurableSpace Ω} (X : ι → Ω → E) (P : MeasureTheory.Measure Ω) (𝓕 : MeasureTheory.Filtration ι mΩ) [MeasureTheory.SigmaFiniteFiltration P 𝓕] : ι → Ω → ℝ

The predictable quadratic variation of a locally square-integrable martingale, defined as the predictable part of the Doob-Meyer decomposition of its squared norm.

Equations

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

def ProbabilityTheory.«term⟨_;_,_⟩ₘ» : Lean.ParserDescr

The predictable quadratic variation of a locally square-integrable martingale, defined as the predictable part of the Doob-Meyer decomposition of its squared norm.

Equations

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

@[simp]

theorem ProbabilityTheory.predQuadVariation_of_not_isLocallySquareIntegrable {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] [MeasurableSpace ι] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} [MeasureTheory.SigmaFiniteFiltration P 𝓕] {X : ι → Ω → E} (hX : ¬IsLocallySquareIntegrable X 𝓕 P) : predQuadVariation X P 𝓕 = fun (x : ι) (x_1 : Ω) => 0

@[simp]

theorem ProbabilityTheory.predQuadVariation_of_not_cadlag {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] [MeasurableSpace ι] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} [MeasureTheory.SigmaFiniteFiltration P 𝓕] {X : ι → Ω → E} (hX_cadlag : ¬∀ (ω : Ω), IsCadlag fun (x : ι) => X x ω) : predQuadVariation X P 𝓕 = fun (x : ι) (x_1 : Ω) => 0

theorem ProbabilityTheory.isStronglyPredictable_predQuadVariation {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] [MeasurableSpace ι] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} [MeasureTheory.SigmaFiniteFiltration P 𝓕] {X : ι → Ω → E} : MeasureTheory.IsStronglyPredictable 𝓕 (predQuadVariation X P 𝓕)

theorem ProbabilityTheory.isCadlag_predQuadVariation {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] [MeasurableSpace ι] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} [MeasureTheory.SigmaFiniteFiltration P 𝓕] {X : ι → Ω → E} (ω : Ω) : IsCadlag fun (x : ι) => predQuadVariation X P 𝓕 x ω

theorem ProbabilityTheory.hasLocallyIntegrableSup_predQuadVariation {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] [MeasurableSpace ι] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} [MeasureTheory.SigmaFiniteFiltration P 𝓕] {X : ι → Ω → E} : HasLocallyIntegrableSup (predQuadVariation X P 𝓕) 𝓕 P

theorem ProbabilityTheory.monotone_predQuadVariation {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] [MeasurableSpace ι] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} [MeasureTheory.SigmaFiniteFiltration P 𝓕] {X : ι → Ω → E} (ω : Ω) : Monotone fun (x : ι) => predQuadVariation X P 𝓕 x ω

noncomputable def ProbabilityTheory.predQuadCovariation {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] [MeasurableSpace ι] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {mΩ : MeasurableSpace Ω} (X Y : ι → Ω → E) (P : MeasureTheory.Measure Ω) (𝓕 : MeasureTheory.Filtration ι mΩ) [MeasureTheory.SigmaFiniteFiltration P 𝓕] : ι → Ω → ℝ

Predictable quadratic covariation of two processes.

Equations

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

def ProbabilityTheory.«term⟨_,_;_,_⟩ₘ» : Lean.ParserDescr

Predictable quadratic covariation of two processes.

Equations

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

theorem ProbabilityTheory.isStronglyPredictable_predQuadCovariation {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] [MeasurableSpace ι] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} [MeasureTheory.SigmaFiniteFiltration P 𝓕] {X Y : ι → Ω → E} : MeasureTheory.IsStronglyPredictable 𝓕 (predQuadCovariation X Y P 𝓕)

theorem ProbabilityTheory.isCadlag_predQuadCovariation {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] [MeasurableSpace ι] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} [MeasureTheory.SigmaFiniteFiltration P 𝓕] {X Y : ι → Ω → E} (ω : Ω) : IsCadlag fun (x : ι) => predQuadCovariation X Y P 𝓕 x ω

theorem ProbabilityTheory.hasLocallyIntegrableSup_predQuadCovariation {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] [MeasurableSpace ι] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} [MeasureTheory.SigmaFiniteFiltration P 𝓕] {X Y : ι → Ω → E} : HasLocallyIntegrableSup (predQuadCovariation X Y P 𝓕) 𝓕 P