Add Brownian quadratic variation module

BrownianMotion.lean

@@ -62,6 +62,7 @@ public import BrownianMotion.StochasticIntegral.MonotoneProcess
 public import BrownianMotion.StochasticIntegral.OptionalSampling
 public import BrownianMotion.StochasticIntegral.Predictable
 public import BrownianMotion.StochasticIntegral.QuadraticVariation
+public import BrownianMotion.StochasticIntegral.QuadraticVariationBrownian
 public import BrownianMotion.StochasticIntegral.SimpleProcess
 public import BrownianMotion.StochasticIntegral.SquareIntegrable
 public import BrownianMotion.StochasticIntegral.StochasticInterval

BrownianMotion/StochasticIntegral/Cadlag.lean

@@ -42,6 +42,12 @@ structure IsCadlag [TopologicalSpace E] [Preorder ι] (f : ι → E) : Prop wher
   right_continuous : Function.IsRightContinuous f
   left_limit : ∀ x, ∃ l, Tendsto f (𝓝[<] x) (𝓝 l)
 
+/-- A continuous function is càdlàg. -/
+lemma Continuous.isCadlag [TopologicalSpace E] [Preorder ι] {f : ι → E}
+    (hf : Continuous f) : IsCadlag f where
+  right_continuous _ := hf.continuousAt.continuousWithinAt
+  left_limit x := ⟨f x, hf.continuousAt.tendsto.mono_left nhdsWithin_le_nhds⟩
+
 section Jump
 
 /-- The set of left jump times of a function. -/

BrownianMotion/StochasticIntegral/DoobMeyer.lean

@@ -1333,6 +1333,46 @@ lemma monotone_predictablePart (hX : IsLocalSubmartingale X 𝓕 P)
     ∀ ω, Monotone (hX.predictablePart X hX_cadlag · ω) :=
   (hX.doob_meyer hX_cadlag).choose_spec.choose_spec.2.2.2.2.2.2
 
+section Normalized
+
+variable {κ Ω' : Type*} [ConditionallyCompleteLinearOrderBot κ] [TopologicalSpace κ]
+  [OrderTopology κ] [MeasurableSpace κ] [BorelSpace κ] [PolishSpace κ]
+  {mΩ' : MeasurableSpace Ω'} {P' : Measure Ω'} {X' : κ → Ω' → ℝ}
+  {𝓕' : Filtration κ mΩ'} [IsFiniteMeasure P'] [Approximable 𝓕' P']
+  [𝓕'.IsComplete P'] [𝓕'.IsRightContinuous]
+
+/-- A normalized local Doob-Meyer decomposition whose predictable part starts from zero. -/
+theorem doob_meyer_normalized (hX : IsLocalSubmartingale X' 𝓕' P')
+    (hX_cadlag : ∀ ω, IsCadlag (X' · ω)) :
+    ∃ (M A : κ → Ω' → ℝ), X' = M + A ∧ IsLocalMartingale M 𝓕' P' ∧
+      (∀ ω, IsCadlag (M · ω)) ∧ IsStronglyPredictable 𝓕' A ∧
+      IsStronglyProgressive 𝓕' A ∧ (∀ ω, IsCadlag (A · ω)) ∧
+      HasLocallyIntegrableSup A 𝓕' P' ∧ (∀ ω, Monotone (A · ω)) ∧
+      (∀ ω, A ⊥ ω = 0) := by
+  sorry
+
+/-- The normalized predictable part of the Doob-Meyer decomposition. -/
+noncomputable
+def normalizedPredictablePart (X : κ → Ω' → ℝ)
+    (hX : IsLocalSubmartingale X 𝓕' P') (hX_cadlag : ∀ ω, IsCadlag (X · ω)) :
+    κ → Ω' → ℝ :=
+  (hX.doob_meyer_normalized hX_cadlag).choose_spec.choose
+
+/-- Any normalized Doob-Meyer decomposition has the same predictable part as the choice-based
+normalized decomposition, at each deterministic time and almost surely. -/
+lemma normalizedPredictablePart_eq_of_normalized_decomposition
+    (hX : IsLocalSubmartingale X' 𝓕' P') (hX_cadlag : ∀ ω, IsCadlag (X' · ω))
+    {M A : κ → Ω' → ℝ} (hXA : X' = M + A)
+    (hM : IsLocalMartingale M 𝓕' P') (hM_cadlag : ∀ ω, IsCadlag (M · ω))
+    (hA_pred : IsStronglyPredictable 𝓕' A) (hA_prog : IsStronglyProgressive 𝓕' A)
+    (hA_cadlag : ∀ ω, IsCadlag (A · ω))
+    (hA_int : HasLocallyIntegrableSup A 𝓕' P') (hA_mono : ∀ ω, Monotone (A · ω))
+    (hA_zero : ∀ ω, A ⊥ ω = 0) (t : κ) :
+    hX.normalizedPredictablePart X' hX_cadlag t =ᵐ[P'] A t := by
+  sorry
+
+end Normalized
+
 end IsLocalSubmartingale
 
 end ProbabilityTheory

BrownianMotion/StochasticIntegral/QuadraticVariation.lean

@@ -19,9 +19,11 @@ open scoped ENNReal
 
 namespace ProbabilityTheory
 
-variable {ι Ω E : Type*} [LinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι]
-  [MeasurableSpace ι] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
+variable {ι Ω E : Type*} [ConditionallyCompleteLinearOrderBot ι] [TopologicalSpace ι]
+  [OrderTopology ι] [MeasurableSpace ι] [BorelSpace ι] [PolishSpace ι]
+  [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
   {mΩ : MeasurableSpace Ω} {P : Measure Ω} {X : ι → Ω → E} {𝓕 : Filtration ι mΩ}
+  [IsFiniteMeasure P] [Approximable 𝓕 P] [𝓕.IsComplete P] [𝓕.IsRightContinuous]
 
 /-- The quadratic variation of a locally square-integrable martingale, defined as the predictable
 part of the Doob-Meyer decomposition of its squared norm. -/
@@ -32,7 +34,7 @@ def quadraticVariation [SigmaFiniteFiltration P 𝓕]
     ι → Ω → ℝ :=
   have hX2_cadlag : ∀ ω, IsCadlag (fun t ↦ ‖X t ω‖ ^ 2) :=
     fun ω ↦ IsCadlag.norm_sq (hX_cadlag ω)
-  (hX_sq.isLocalSubmartingale_sq_norm).predictablePart
+  (hX_sq.isLocalSubmartingale_sq_norm).normalizedPredictablePart
     (fun t ω ↦ ‖X t ω‖ ^ 2) hX2_cadlag
 
 end ProbabilityTheory