diff --git a/BrownianMotion.lean b/BrownianMotion.lean index 67b6b37d..34d28932 100644 --- a/BrownianMotion.lean +++ b/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 diff --git a/BrownianMotion/StochasticIntegral/Cadlag.lean b/BrownianMotion/StochasticIntegral/Cadlag.lean index 2b0c7184..64c6c1d8 100644 --- a/BrownianMotion/StochasticIntegral/Cadlag.lean +++ b/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. -/ diff --git a/BrownianMotion/StochasticIntegral/DoobMeyer.lean b/BrownianMotion/StochasticIntegral/DoobMeyer.lean index 9c92e3a9..2b9df40d 100644 --- a/BrownianMotion/StochasticIntegral/DoobMeyer.lean +++ b/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 diff --git a/BrownianMotion/StochasticIntegral/QuadraticVariation.lean b/BrownianMotion/StochasticIntegral/QuadraticVariation.lean index f680e964..2af698ed 100644 --- a/BrownianMotion/StochasticIntegral/QuadraticVariation.lean +++ b/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 diff --git a/BrownianMotion/StochasticIntegral/QuadraticVariationBrownian.lean b/BrownianMotion/StochasticIntegral/QuadraticVariationBrownian.lean new file mode 100644 index 00000000..1f1d2a52 --- /dev/null +++ b/BrownianMotion/StochasticIntegral/QuadraticVariationBrownian.lean @@ -0,0 +1,446 @@ +/- +Copyright (c) 2025 Rémy Degenne. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Rémy Degenne +-/ +module + +public import BrownianMotion.Gaussian.BrownianMotion +public import BrownianMotion.StochasticIntegral.QuadraticVariation + +/-! # Quadratic variation of Brownian motion + +-/ + +@[expose] public section + +open MeasureTheory Filter Filtration +open scoped ENNReal NNReal + +namespace ProbabilityTheory + +/-- The linear order instance on `ℝ≥0` used locally for the quadratic-variation construction. -/ +noncomputable local instance qvLinearOrderNNReal : LinearOrder ℝ≥0 := + let inst := (inferInstance : ConditionallyCompleteLinearOrderBot ℝ≥0) + inst.toConditionallyCompleteLinearOrder.toLinearOrder + +/-- The natural filtration of the canonical Brownian motion. -/ +noncomputable abbrev brownianNaturalFiltration : + Filtration ℝ≥0 (inferInstance : MeasurableSpace (ℝ≥0 → ℝ)) := + natural brownian fun t ↦ (measurable_brownian t).stronglyMeasurable + +/-- The Brownian natural filtration admits dyadic approximations of stopping times. -/ +noncomputable instance brownianNaturalFiltrationApproximable : + Approximable brownianNaturalFiltration gaussianLimit := + ⟨fun τ hτ ↦ ⟨nnrealApproxSeq τ, nnrealApproxSeq_isStoppingTime brownianNaturalFiltration hτ, + nnrealApproxSeq_countable τ, nnrealApproxSeq_antitone τ, + nnrealApproxSeq_le τ, ae_of_all _ <| nnrealApproxSeq_tendsto τ⟩⟩ + +/-- The canonical Brownian motion has càdlàg paths. -/ +lemma isCadlag_brownian (ω : ℝ≥0 → ℝ) : IsCadlag (brownian · ω) := + (continuous_brownian ω).isCadlag + +/-- The canonical Brownian motion is a martingale with respect to its natural filtration. -/ +lemma martingale_brownian : + Martingale brownian brownianNaturalFiltration gaussianLimit := by + haveI : IsFilteredPreBrownian brownian brownianNaturalFiltration gaussianLimit := + isBrownianReal_brownian.toIsPreBrownianReal.isFilteredPreBrownian measurable_brownian + exact IsPreBrownianReal.isMartingale brownian brownianNaturalFiltration gaussianLimit + +/-- The canonical Brownian square minus time process is a martingale. -/ +lemma martingale_brownian_sq_sub_time : + Martingale (fun t omega => brownian t omega ^ 2 - (t : ℝ)) + brownianNaturalFiltration gaussianLimit := by + refine ⟨?_, ?_⟩ + · intro t + have ht : StronglyMeasurable[brownianNaturalFiltration t] (brownian t) := + martingale_brownian.stronglyAdapted t + have hsm : StronglyMeasurable[brownianNaturalFiltration t] + (fun ω => brownian t ω * brownian t ω - (t : ℝ)) := by + convert (ht.mul ht).sub + (stronglyMeasurable_const : + StronglyMeasurable[brownianNaturalFiltration t] + (fun _ : ℝ≥0 → ℝ => (t : ℝ))) using 1 + ext ω + rfl + simpa [pow_two] using hsm + · intro s t hst + haveI : IsFilteredPreBrownian brownian brownianNaturalFiltration gaussianLimit := + isBrownianReal_brownian.toIsPreBrownianReal.isFilteredPreBrownian measurable_brownian + have hM := fun u ↦ + ((IsFilteredPreBrownian.stronglyAdapted (X := brownian) + (𝓕 := brownianNaturalFiltration) (P := gaussianLimit) u).mono + (brownianNaturalFiltration.le u)).measurable + have hBs_sm : StronglyMeasurable[brownianNaturalFiltration s] (brownian s) := + martingale_brownian.stronglyAdapted s + have hBs_L2 : MemLp (brownian s) 2 gaussianLimit := + (isGaussianProcess_brownian.hasGaussianLaw_eval s).memLp_two + have hDelta_L2 : MemLp (brownian t - brownian s) 2 gaussianLimit := + (isGaussianProcess_brownian.hasGaussianLaw_fun_sub (s := t) (t := s)).memLp_two + have hDeltaLaw : HasLaw (brownian t - brownian s) (gaussianReal 0 (t - s)) + gaussianLimit := by + have hvar : nndist t s = t - s := by + rw [NNReal.nndist_eq] + rw [tsub_eq_zero_of_le hst] + simp + simpa [hvar] using (hasLaw_brownian_sub (s := t) (t := s)) + have hDeltaMean : gaussianLimit[brownian t - brownian s] = 0 := by + calc + gaussianLimit[brownian t - brownian s] + = ∫ x, x ∂gaussianReal 0 (t - s) := hDeltaLaw.integral_eq + _ = 0 := by simp + have hDeltaSqIntegral : + ∫ ω, (brownian t - brownian s) ω ^ 2 ∂gaussianLimit = + ((t - s : ℝ≥0) : ℝ) := by + have hvar_delta : + Var[brownian t - brownian s; gaussianLimit] = ((t - s : ℝ≥0) : ℝ) := by + rw [hDeltaLaw.variance_eq, variance_id_gaussianReal] + rw [variance_eq_integral hDeltaLaw.aemeasurable, hDeltaMean] at hvar_delta + simpa using hvar_delta + have hDeltaNoCond : + gaussianLimit[brownian t - brownian s | brownianNaturalFiltration s] + =ᵐ[gaussianLimit] fun _ => gaussianLimit[brownian t - brownian s] := by + refine condExp_indep_eq ?_ (brownianNaturalFiltration.le s) ?_ + (IsFilteredPreBrownian.indep (X := brownian) (𝓕 := brownianNaturalFiltration) + (P := gaussianLimit) s t hst) + · exact Measurable.comap_le (Measurable.sub (hM t) (hM s)) + · exact (comap_measurable (brownian t - brownian s)).stronglyMeasurable + have hDeltaCondZero : + gaussianLimit[brownian t - brownian s | brownianNaturalFiltration s] + =ᵐ[gaussianLimit] fun _ => 0 := + hDeltaNoCond.trans (ae_of_all _ fun _ => hDeltaMean) + have hProdInt : + Integrable (fun ω => brownian s ω * (brownian t ω - brownian s ω)) + gaussianLimit := by + rw [← memLp_one_iff_integrable] + exact hDelta_L2.mul' hBs_L2 + have hDeltaInt : Integrable (brownian t - brownian s) gaussianLimit := + (isGaussianProcess_brownian.hasGaussianLaw_fun_sub (s := t) (t := s)).integrable + have hProdCondZero : + gaussianLimit[fun ω => brownian s ω * (brownian t ω - brownian s ω) | + brownianNaturalFiltration s] =ᵐ[gaussianLimit] fun _ => 0 := by + have hpull := condExp_mul_of_stronglyMeasurable_left hBs_sm hProdInt + hDeltaInt + have hDeltaCondZero' : + gaussianLimit[fun ω => brownian t ω - brownian s ω | brownianNaturalFiltration s] + =ᵐ[gaussianLimit] fun _ => 0 := by + convert hDeltaCondZero using 1 + ext ω + rfl + have hpull' : + gaussianLimit[fun ω => brownian s ω * (brownian t ω - brownian s ω) | + brownianNaturalFiltration s] + =ᵐ[gaussianLimit] + brownian s * gaussianLimit[fun ω => brownian t ω - brownian s ω | + brownianNaturalFiltration s] := by + convert hpull using 1 + ext ω + rfl + filter_upwards [hpull', hDeltaCondZero'] with ω hpullω hzeroω + have hzeroω' : + (gaussianLimit[fun ω => brownian t ω - brownian s ω | + brownianNaturalFiltration s]) ω = 0 := by + exact hzeroω + rw [hpullω] + simp [Pi.mul_apply, hzeroω'] + have hTwoProdInt : + Integrable (fun ω => (2 : ℝ) * (brownian s ω * (brownian t ω - brownian s ω))) + gaussianLimit := by + simpa [Pi.smul_apply, smul_eq_mul] using hProdInt.const_mul (2 : ℝ) + have hTwoProdCondZero : + gaussianLimit[fun ω => (2 : ℝ) * (brownian s ω * (brownian t ω - brownian s ω)) | + brownianNaturalFiltration s] =ᵐ[gaussianLimit] fun _ => 0 := by + have hsmul := condExp_smul (μ := gaussianLimit) (c := (2 : ℝ)) + (f := fun ω => brownian s ω * (brownian t ω - brownian s ω)) + (m := brownianNaturalFiltration s) + have hsmul_zero : + gaussianLimit[(2 : ℝ) • + (fun ω => brownian s ω * (brownian t ω - brownian s ω)) | + brownianNaturalFiltration s] + =ᵐ[gaussianLimit] + fun _ => 0 := by + filter_upwards [hsmul, hProdCondZero] with ω hsmulω hzeroω + rw [hsmulω] + simp [Pi.smul_apply, hzeroω] + change gaussianLimit[(2 : ℝ) • + (fun ω => brownian s ω * (brownian t ω - brownian s ω)) | + brownianNaturalFiltration s] =ᵐ[gaussianLimit] fun _ => 0 + exact hsmul_zero + have hCenterInt : + Integrable (fun ω => (brownian t ω - brownian s ω) ^ 2 - (t - s : ℝ≥0)) + gaussianLimit := + hDelta_L2.integrable_sq.sub (integrable_const ((t - s : ℝ≥0) : ℝ)) + have hCenterIndep : Indep + (MeasurableSpace.comap + (fun ω => (brownian t ω - brownian s ω) ^ 2 - (t - s : ℝ≥0)) inferInstance) + (brownianNaturalFiltration s) gaussianLimit := by + refine indep_of_indep_of_le_left + (IsFilteredPreBrownian.indep (X := brownian) (𝓕 := brownianNaturalFiltration) + (P := gaussianLimit) s t hst) ?_ + have hcomp : + (fun ω => (brownian t ω - brownian s ω) ^ 2 - (t - s : ℝ≥0)) = + (fun x : ℝ => x ^ 2 - (t - s : ℝ≥0)) ∘ (brownian t - brownian s) := rfl + rw [hcomp, ← MeasurableSpace.comap_comp] + exact MeasurableSpace.comap_mono (Measurable.comap_le (by fun_prop)) + have hCenterNoCond : + gaussianLimit[fun ω => (brownian t ω - brownian s ω) ^ 2 - (t - s : ℝ≥0) | + brownianNaturalFiltration s] + =ᵐ[gaussianLimit] + fun _ => ∫ ω, (brownian t ω - brownian s ω) ^ 2 - (t - s : ℝ≥0) + ∂gaussianLimit := by + refine condExp_indep_eq ?_ (brownianNaturalFiltration.le s) ?_ hCenterIndep + · exact Measurable.comap_le + (((Measurable.sub (hM t) (hM s)).pow_const 2).sub measurable_const) + · exact (comap_measurable + (fun ω => (brownian t ω - brownian s ω) ^ 2 - (t - s : ℝ≥0))).stronglyMeasurable + have hCenterIntegralZero : + ∫ ω, (brownian t ω - brownian s ω) ^ 2 - (t - s : ℝ≥0) ∂gaussianLimit = 0 := by + change ∫ ω, (brownian t - brownian s) ω ^ 2 - ((t - s : ℝ≥0) : ℝ) + ∂gaussianLimit = 0 + rw [integral_sub hDelta_L2.integrable_sq + (integrable_const ((t - s : ℝ≥0) : ℝ)), hDeltaSqIntegral, integral_const] + simp [smul_eq_mul] + have hCenterCondZero : + gaussianLimit[fun ω => (brownian t ω - brownian s ω) ^ 2 - (t - s : ℝ≥0) | + brownianNaturalFiltration s] =ᵐ[gaussianLimit] fun _ => 0 := + hCenterNoCond.trans (ae_of_all _ fun _ => hCenterIntegralZero) + let twoProd : (ℝ≥0 → ℝ) → ℝ := + fun ω => (2 : ℝ) * (brownian s ω * (brownian t ω - brownian s ω)) + let center : (ℝ≥0 → ℝ) → ℝ := + fun ω => (brownian t ω - brownian s ω) ^ 2 - (t - s : ℝ≥0) + let rest : (ℝ≥0 → ℝ) → ℝ := fun ω => twoProd ω + center ω + let past : (ℝ≥0 → ℝ) → ℝ := fun ω => brownian s ω ^ 2 - (s : ℝ) + have hTwoProdInt' : Integrable twoProd gaussianLimit := by + dsimp only [twoProd] + exact hTwoProdInt + have hCenterInt' : Integrable center gaussianLimit := by + dsimp only [center] + exact hCenterInt + have hTwoProdCondZero' : + gaussianLimit[twoProd | brownianNaturalFiltration s] + =ᵐ[gaussianLimit] fun _ => 0 := by + dsimp only [twoProd] + exact hTwoProdCondZero + have hCenterCondZero' : + gaussianLimit[center | brownianNaturalFiltration s] + =ᵐ[gaussianLimit] fun _ => 0 := by + dsimp only [center] + exact hCenterCondZero + have hRestInt : Integrable rest gaussianLimit := by + dsimp only [rest] + exact hTwoProdInt'.add hCenterInt' + have hRestCondZero : gaussianLimit[rest | brownianNaturalFiltration s] + =ᵐ[gaussianLimit] fun _ => 0 := by + dsimp only [rest] + calc + gaussianLimit[fun ω => twoProd ω + center ω | brownianNaturalFiltration s] + =ᵐ[gaussianLimit] + gaussianLimit[twoProd | brownianNaturalFiltration s] + + gaussianLimit[center | brownianNaturalFiltration s] := + condExp_add hTwoProdInt' hCenterInt' _ + _ =ᵐ[gaussianLimit] fun _ => 0 := by + filter_upwards [hTwoProdCondZero', hCenterCondZero'] with ω htwo hcenter + rw [Pi.add_apply, htwo, hcenter] + simp + have hPastInt : Integrable past gaussianLimit := by + dsimp only [past] + exact hBs_L2.integrable_sq.sub (integrable_const (s : ℝ)) + have hPastSm : StronglyMeasurable[brownianNaturalFiltration s] past := by + dsimp only [past] + have hsm : StronglyMeasurable[brownianNaturalFiltration s] + (fun ω => brownian s ω * brownian s ω - (s : ℝ)) := by + convert (hBs_sm.mul hBs_sm).sub + (stronglyMeasurable_const : + StronglyMeasurable[brownianNaturalFiltration s] + (fun _ : ℝ≥0 → ℝ => (s : ℝ))) using 1 + ext ω + rfl + simpa [pow_two] using hsm + have hExpand : + (fun omega => brownian t omega ^ 2 - (t : ℝ)) = fun omega => past omega + rest omega := by + funext omega + dsimp only [past, rest, twoProd, center] + have htime : (t : ℝ) = (s : ℝ) + ((t - s : ℝ≥0) : ℝ) := by + rw [← NNReal.coe_add, add_tsub_cancel_of_le hst] + rw [htime] + ring + calc + gaussianLimit[fun omega => brownian t omega ^ 2 - (t : ℝ) | brownianNaturalFiltration s] + = gaussianLimit[fun omega => past omega + rest omega | brownianNaturalFiltration s] := by + rw [hExpand] + _ =ᵐ[gaussianLimit] + gaussianLimit[past | brownianNaturalFiltration s] + + gaussianLimit[rest | brownianNaturalFiltration s] := + condExp_add hPastInt hRestInt _ + _ =ᵐ[gaussianLimit] past + (fun _ => 0) := + by + rw [condExp_of_stronglyMeasurable (brownianNaturalFiltration.le s) hPastSm hPastInt] + filter_upwards [hRestCondZero] with omega hrest + rw [Pi.add_apply, hrest] + simp + _ =ᵐ[gaussianLimit] (fun omega => brownian s omega ^ 2 - (s : ℝ)) := by + filter_upwards with omega + dsimp only [past] + simp + +/-- Brownian square minus deterministic time has càdlàg paths. -/ +lemma isCadlag_brownian_sq_sub_time (ω : ℝ≥0 → ℝ) : + IsCadlag (fun t : ℝ≥0 => brownian t ω ^ 2 - (t : ℝ)) := by + have hsq : IsCadlag (fun t : ℝ≥0 => brownian t ω ^ 2) := by + have hpow : Continuous fun x : ℝ => x ^ 2 := by fun_prop + simpa [Function.comp_def] using (isCadlag_brownian ω).continuous_comp hpow + have htime : IsCadlag (fun t : ℝ≥0 => (t : ℝ)) := + (NNReal.continuous_coe : Continuous fun t : ℝ≥0 => (t : ℝ)).isCadlag + have hneg : IsCadlag (fun t : ℝ≥0 => (-1 : ℝ) • (t : ℝ)) := + htime.const_smul (-1) + have hadd : IsCadlag + ((fun t : ℝ≥0 => brownian t ω ^ 2) + + fun t : ℝ≥0 => (-1 : ℝ) • (t : ℝ)) := + hsq.add hneg + change IsCadlag ((fun t : ℝ≥0 => brownian t ω ^ 2) + fun t : ℝ≥0 => -(t : ℝ)) + simpa [Pi.add_apply, smul_eq_mul] using hadd + +/-- The deterministic time process `A_t = t`, used as the predictable Brownian quadratic +variation candidate. -/ +@[nolint unusedArguments] +noncomputable abbrev brownianDeterministicTime : + ℝ≥0 → (ℝ≥0 → ℝ) → ℝ := + fun t _ => (t : ℝ) + +/-- The deterministic time process is strongly adapted to the Brownian natural filtration. -/ +lemma stronglyAdapted_brownianDeterministicTime : + StronglyAdapted brownianNaturalFiltration brownianDeterministicTime := by + intro t + exact stronglyMeasurable_const + +/-- The deterministic time process is strongly predictable. -/ +lemma isStronglyPredictable_brownianDeterministicTime : + IsStronglyPredictable brownianNaturalFiltration brownianDeterministicTime := by + refine stronglyAdapted_brownianDeterministicTime.isStronglyPredictable_of_leftContinuous ?_ + intro ω a + change ContinuousWithinAt (fun t : ℝ≥0 => (t : ℝ)) (Set.Iio a) a + exact (NNReal.continuous_coe.continuousAt (x := a)).continuousWithinAt + +/-- The deterministic time process is strongly progressive. -/ +lemma isStronglyProgressive_brownianDeterministicTime : + IsStronglyProgressive brownianNaturalFiltration brownianDeterministicTime := by + refine stronglyAdapted_brownianDeterministicTime.isStronglyProgressive_of_rightContinuous ?_ + intro ω a + change ContinuousWithinAt (fun t : ℝ≥0 => (t : ℝ)) (Set.Ioi a) a + exact (NNReal.continuous_coe.continuousAt (x := a)).continuousWithinAt + +/-- The deterministic time process has càdlàg paths. -/ +lemma isCadlag_brownianDeterministicTime (ω : ℝ≥0 → ℝ) : + IsCadlag (brownianDeterministicTime · ω) := by + simpa [brownianDeterministicTime] using + ((NNReal.continuous_coe : Continuous fun t : ℝ≥0 => (t : ℝ)).isCadlag) + +/-- The deterministic time process is pathwise monotone. -/ +lemma monotone_brownianDeterministicTime (ω : ℝ≥0 → ℝ) : + Monotone (brownianDeterministicTime · ω) := by + intro s t hst + exact_mod_cast hst + +/-- The deterministic time process starts from zero. -/ +lemma brownianDeterministicTime_bot_eq_zero (ω : ℝ≥0 → ℝ) : + brownianDeterministicTime ⊥ ω = 0 := by + simp [brownianDeterministicTime] + +/-- The deterministic time process has integrable running supremum on every deterministic +time interval. -/ +lemma hasIntegrableSup_brownianDeterministicTime : + HasIntegrableSup brownianDeterministicTime gaussianLimit := by + have hsup_eq : + (fun tω : ℝ≥0 × (ℝ≥0 → ℝ) => + ⨆ s ≤ tω.1, ‖brownianDeterministicTime s tω.2‖ₑ) + = fun tω => ‖(tω.1 : ℝ)‖ₑ := by + funext tω + refine le_antisymm ?_ ?_ + · refine iSup₂_le fun s hs => ?_ + simp only [brownianDeterministicTime] + rw [Real.enorm_of_nonneg (NNReal.coe_nonneg s), + Real.enorm_of_nonneg (NNReal.coe_nonneg tω.1)] + exact ENNReal.ofReal_le_ofReal (by exact_mod_cast hs) + · exact le_iSup₂_of_le tω.1 le_rfl (by simp [brownianDeterministicTime]) + have hdet_meas : + Measurable (fun tω : ℝ≥0 × (ℝ≥0 → ℝ) => ‖(tω.1 : ℝ)‖ₑ) := + measurable_enorm.comp (NNReal.continuous_coe.measurable.comp measurable_fst) + have hsup_meas : + HasStronglyMeasurableSupProcess + (mΩ := (inferInstance : MeasurableSpace (ℝ≥0 → ℝ))) + brownianDeterministicTime := by + rw [HasStronglyMeasurableSupProcess, hsup_eq] + exact hdet_meas.stronglyMeasurable + refine ⟨hsup_meas, fun t => ?_⟩ + refine Integrable.of_mem_Icc_enorm (a := 0) (b := ‖(t : ℝ)‖ₑ) ?_ enorm_ne_top + (hsup_meas.comp_measurable (measurable_const.prodMk measurable_id)).aemeasurable ?_ + · simp + · filter_upwards with ω + have hle : (⨆ s ≤ t, ‖brownianDeterministicTime s ω‖ₑ) ≤ ‖(t : ℝ)‖ₑ := by + refine iSup₂_le fun s hs => ?_ + simp only [brownianDeterministicTime] + rw [Real.enorm_of_nonneg (NNReal.coe_nonneg s), + Real.enorm_of_nonneg (NNReal.coe_nonneg t)] + exact ENNReal.ofReal_le_ofReal (by exact_mod_cast hs) + exact ⟨bot_le, hle⟩ + +/-- The deterministic time process has locally integrable running supremum. -/ +lemma hasLocallyIntegrableSup_brownianDeterministicTime : + HasLocallyIntegrableSup brownianDeterministicTime brownianNaturalFiltration gaussianLimit := by + simpa [HasLocallyIntegrableSup] using + (Locally.of_prop (𝓕 := brownianNaturalFiltration) (P := gaussianLimit) + (p := fun X : ℝ≥0 → (ℝ≥0 → ℝ) → ℝ => HasIntegrableSup X gaussianLimit) + hasIntegrableSup_brownianDeterministicTime) + +section UsualConditions + +variable [brownianNaturalFiltration.IsComplete gaussianLimit] +variable [brownianNaturalFiltration.IsRightContinuous] + +/-- The canonical Brownian motion is locally square-integrable. -/ +lemma locally_isSquareIntegrable_brownian : + IsLocallySquareIntegrable brownian brownianNaturalFiltration gaussianLimit := + Martingale.isLocallySquareIntegrable_of_continuous martingale_brownian continuous_brownian + +/-- The quadratic variation process attached to the canonical Brownian motion. -/ +noncomputable abbrev brownianQuadraticVariation : ℝ≥0 → (ℝ≥0 → ℝ) → ℝ := + quadraticVariation locally_isSquareIntegrable_brownian isCadlag_brownian + +/-- At each deterministic time, the Brownian quadratic variation is almost surely `t`. -/ +theorem quadraticVariation_brownian (t : ℝ≥0) : + brownianQuadraticVariation t =ᵐ[gaussianLimit] fun _ => (t : ℝ) := by + let X2 : ℝ≥0 → (ℝ≥0 → ℝ) → ℝ := fun s ω => ‖brownian s ω‖ ^ 2 + have hX2_cadlag : ∀ ω, IsCadlag (X2 · ω) := by + intro ω + simpa [X2, Function.comp_def] using IsCadlag.norm_sq (isCadlag_brownian ω) + have hX_sub : IsLocalSubmartingale X2 brownianNaturalFiltration gaussianLimit := by + simpa [X2] using + locally_isSquareIntegrable_brownian.isLocalSubmartingale_sq_norm + let M : ℝ≥0 → (ℝ≥0 → ℝ) → ℝ := fun s ω => brownian s ω ^ 2 - (s : ℝ) + have hM : IsLocalMartingale M brownianNaturalFiltration gaussianLimit := by + simpa [M] using + (Martingale.IsLocalMartingale martingale_brownian_sq_sub_time + isCadlag_brownian_sq_sub_time) + have hM_cadlag : ∀ ω, IsCadlag (M · ω) := by + intro ω + simpa [M, Function.comp_def] using isCadlag_brownian_sq_sub_time ω + have hX_decomp : X2 = M + brownianDeterministicTime := by + ext s ω + simp only [X2, M, Pi.add_apply, brownianDeterministicTime] + rw [Real.norm_eq_abs, sq_abs] + ring + have hcompare : + IsLocalSubmartingale.normalizedPredictablePart X2 hX_sub hX2_cadlag t + =ᵐ[gaussianLimit] + brownianDeterministicTime t := + IsLocalSubmartingale.normalizedPredictablePart_eq_of_normalized_decomposition + hX_sub hX2_cadlag hX_decomp hM hM_cadlag isStronglyPredictable_brownianDeterministicTime + isStronglyProgressive_brownianDeterministicTime isCadlag_brownianDeterministicTime + hasLocallyIntegrableSup_brownianDeterministicTime monotone_brownianDeterministicTime + brownianDeterministicTime_bot_eq_zero t + simpa [brownianQuadraticVariation, quadraticVariation, X2, + brownianDeterministicTime] using hcompare + +end UsualConditions + +end ProbabilityTheory diff --git a/BrownianMotion/StochasticIntegral/SquareIntegrable.lean b/BrownianMotion/StochasticIntegral/SquareIntegrable.lean index 77516d4b..0a8418c2 100644 --- a/BrownianMotion/StochasticIntegral/SquareIntegrable.lean +++ b/BrownianMotion/StochasticIntegral/SquareIntegrable.lean @@ -82,6 +82,12 @@ lemma IsSquareIntegrable.smul [CompleteSpace E] (hX : IsSquareIntegrable X 𝓕 simp only [eLpNorm_const_smul, ← ENNReal.mul_iSup] exact ENNReal.mul_lt_top ENNReal.coe_lt_top hX.bounded +lemma Martingale.isLocallySquareIntegrable_of_continuous [OrderBot ι] [OrderTopology ι] + [IsFiniteMeasure P] [Approximable 𝓕 P] [𝓕.IsComplete P] [𝓕.IsRightContinuous] + (hX : Martingale X 𝓕 P) (hX_cont : ∀ ω, Continuous (X · ω)) : + IsLocallySquareIntegrable X 𝓕 P := by + sorry + variable [SigmaFiniteFiltration P 𝓕] lemma IsSquareIntegrable.submartingale_sq_norm [CompleteSpace E] (hX : IsSquareIntegrable X 𝓕 P) :