Ornstein–Uhlenbeck process

DefinitionCovariance of the Ornstein–Uhlenbeck process started at zero#✓fully proved

The covariance function of the Ornstein–Uhlenbeck process started at 0: (σ² / (2θ)) (e^{-θ|t-s|} - e^{-θ(t+s)}) (Karatzas–Shreve 1991, Section 5.6). It is meant for θ > 0 and times s, t ≥ 0; at θ = 0 the division by zero makes it 0.

noncomputable def ouCovariance (θ σ s t : ℝ) : ℝ :=
  σ ^ 2 / (2 * θ) * (exp (-θ * |t - s|) - exp (-θ * (t + s)))

Used by 10

Used byTransition law · Mean reversion · One-time law of the Ornstein–Uhlenbeck process from zero · Ornstein–Uhlenbeck process started at zero · Construction (Doob 1942) · The pathwise Langevin solution is an OU process · Symmetry of the Ornstein–Uhlenbeck covariance · Variance of the Ornstein–Uhlenbeck process started at zero · Relaxation to stationarity · Ornstein–Uhlenbeck covariance converges to the stationary one

DefinitionCovariance of the stationary Ornstein–Uhlenbeck process#✓fully proved

The covariance function of the stationary Ornstein–Uhlenbeck process: (σ² / (2θ)) e^{-θ|t-s|} (Uhlenbeck–Ornstein 1930). It is meant for θ > 0.

noncomputable def ouStationaryCovariance (θ σ s t : ℝ) : ℝ :=
  σ ^ 2 / (2 * θ) * exp (-θ * |t - s|)

Used by 11

Used byTransition law · Mean reversion · Stationary law · Stationary Ornstein–Uhlenbeck process · Stationary start · Construction (Doob 1942) · Strict stationarity · Variance of the stationary Ornstein–Uhlenbeck process · Time shifts of a stationary Ornstein–Uhlenbeck process · Relaxation to stationarity · Ornstein–Uhlenbeck covariance converges to the stationary one

TheoremSymmetry of the Ornstein–Uhlenbeck covariance#✓fully proved

The OU covariance is symmetric.

theorem ouCovariance_comm (θ σ s t : ℝ) : ouCovariance θ σ s t = ouCovariance θ σ t s

Uses 1

Statement usesCovariance of the Ornstein–Uhlenbeck process started at zero

TheoremVariance of the Ornstein–Uhlenbeck process started at zero#✓fully proved

The variance of the OU process started at 0: (σ² / (2θ)) (1 - e^{-2θt}).

theorem ouCovariance_self (θ σ t : ℝ) :
    ouCovariance θ σ t t = σ ^ 2 / (2 * θ) * (1 - exp (-2 * θ * t))

Uses 1 · Used by 2

Statement usesCovariance of the Ornstein–Uhlenbeck process started at zero

Used byTransition law · One-time law of the Ornstein–Uhlenbeck process from zero

TheoremVariance of the stationary Ornstein–Uhlenbeck process#✓fully proved

The stationary variance σ² / (2θ).

theorem ouStationaryCovariance_self (θ σ t : ℝ) :
    ouStationaryCovariance θ σ t t = σ ^ 2 / (2 * θ)

Uses 1 · Used by 2

Statement usesCovariance of the stationary Ornstein–Uhlenbeck process

Used byTransition law · Stationary law

TheoremOrnstein–Uhlenbeck covariance converges to the stationary one#✓fully proved

Shifting both times by h → ∞ turns ouCovariance into ouStationaryCovariance.

theorem tendsto_ouCovariance_add {θ : ℝ} (hθ : 0 < θ) (σ s t : ℝ) :
    Tendsto (fun h : ℝ ↦ ouCovariance θ σ (s + h) (t + h)) atTop
      (𝓝 (ouStationaryCovariance θ σ s t))

Uses 2 · Used by 1

Statement usesCovariance of the Ornstein–Uhlenbeck process started at zero · Covariance of the stationary Ornstein–Uhlenbeck process

Used byRelaxation to stationarity

StructureOrnstein–Uhlenbeck process started at zero#✓fully proved

X is an Ornstein–Uhlenbeck process started at 0 with rate θ > 0 and noise amplitude σ under P: a centered Gaussian process with covariance ouCovariance θ σ. Only the finite-dimensional laws are fixed (no path regularity).

structure IsOrnsteinUhlenbeckFromZero (θ σ : ℝ) (X : ℝ≥0 → Ω → ℝ) (P : Measure Ω := by volume_tac) :
    Prop where
  rate_pos : 0 < θ
  isGaussianProcess : IsGaussianProcess X P
  integral_eval : ∀ t, P[X t] = 0
  covariance_eval : ∀ s t, cov[X s, X t; P] = ouCovariance θ σ s t

Uses 1 · Used by 8

Statement usesCovariance of the Ornstein–Uhlenbeck process started at zero

Used byTransition law · Mean reversion · The Ornstein–Uhlenbeck process from zero starts at zero · Existence of the Ornstein–Uhlenbeck process started at zero · One-time law of the Ornstein–Uhlenbeck process from zero · Construction (Doob 1942) · The pathwise Langevin solution is an OU process · Relaxation to stationarity

StructureStationary Ornstein–Uhlenbeck process#✓fully proved

X is a stationary Ornstein–Uhlenbeck process with rate θ > 0 and noise amplitude σ under P: a centered Gaussian process with covariance ouStationaryCovariance θ σ. Only the finite-dimensional laws are fixed.

structure IsStationaryOrnsteinUhlenbeck (θ σ : ℝ) (X : ℝ≥0 → Ω → ℝ)
    (P : Measure Ω := by volume_tac) : Prop where
  rate_pos : 0 < θ
  isGaussianProcess : IsGaussianProcess X P
  integral_eval : ∀ t, P[X t] = 0
  covariance_eval : ∀ s t, cov[X s, X t; P] = ouStationaryCovariance θ σ s t

Uses 1 · Used by 8

Statement usesCovariance of the stationary Ornstein–Uhlenbeck process

Used byTransition law · Mean reversion · Existence of the stationary Ornstein–Uhlenbeck process · Stationary law · Stationary start · Construction (Doob 1942) · Strict stationarity · Time shifts of a stationary Ornstein–Uhlenbeck process

DefinitionDoob's clock for the Ornstein–Uhlenbeck process from zero#✓fully proved

Doob's clock τ t = (e^{2θt} - 1)/(2θ) for the process started at 0. The value is nonnegative for every real θ, so Real.toNNReal only changes its type.

noncomputable def ouClock (θ : ℝ) (t : ℝ≥0) : ℝ≥0 :=
  Real.toNNReal ((exp (2 * θ * t) - 1) / (2 * θ))

Used by 2

Used byConstruction (Doob 1942) · Doob's time change of Brownian motion

DefinitionDoob's clock for the stationary Ornstein–Uhlenbeck process#✓fully proved

Doob's clock t ↦ e^{2θt}/(2θ) for the stationary process (positive for θ > 0).

noncomputable def ouStationaryClock (θ : ℝ) (t : ℝ≥0) : ℝ≥0 :=
  Real.toNNReal (exp (2 * θ * t) / (2 * θ))

Used by 2

Used byConstruction (Doob 1942) · Doob's stationary time change of Brownian motion

DefinitionDoob's time change of Brownian motion#✓fully proved

Doob's time change t ↦ σ e^{-θt} B(τ t) of a process B, with τ = ouClock θ.

noncomputable def ouOfBrownian (θ σ : ℝ) (B : ℝ≥0 → Ω → ℝ) (t : ℝ≥0) (ω : Ω) : ℝ :=
  σ * exp (-θ * t) * B (ouClock θ t) ω

Uses 1 · Used by 2

Statement usesDoob's clock for the Ornstein–Uhlenbeck process from zero

Used byExistence of the Ornstein–Uhlenbeck process started at zero · Construction (Doob 1942)

DefinitionDoob's stationary time change of Brownian motion#✓fully proved

Doob's stationary time change t ↦ σ e^{-θt} B(e^{2θt}/(2θ)) of a process B.

noncomputable def ouStationaryOfBrownian (θ σ : ℝ) (B : ℝ≥0 → Ω → ℝ) (t : ℝ≥0) (ω : Ω) : ℝ :=
  σ * exp (-θ * t) * B (ouStationaryClock θ t) ω

Uses 1 · Used by 2

Statement usesDoob's clock for the stationary Ornstein–Uhlenbeck process

Used byExistence of the stationary Ornstein–Uhlenbeck process · Construction (Doob 1942)

TheoremConstruction (Doob 1942)#✓fully proved

The time change σ e^{-θt} B((e^{2θt} - 1)/(2θ)) of a pre-Brownian motion is an Ornstein–Uhlenbeck process started at 0.

theorem IsPreBrownianReal.isOrnsteinUhlenbeckFromZero_ouOfBrownian {B : ℝ≥0 → Ω → ℝ}
    (hB : IsPreBrownianReal B P) {θ : ℝ} (hθ : 0 < θ) (σ : ℝ) :
    IsOrnsteinUhlenbeckFromZero θ σ (ouOfBrownian θ σ B) P

Uses 4 · Used by 1

Statement usesOrnstein–Uhlenbeck process started at zero · Doob's time change of Brownian motion

Proof usesDoob's clock for the Ornstein–Uhlenbeck process from zero · Covariance of the Ornstein–Uhlenbeck process started at zero

Used byExistence of the Ornstein–Uhlenbeck process started at zero

TheoremConstruction (Doob 1942)#✓fully proved

The time change σ e^{-θt} B(e^{2θt}/(2θ)) of a pre-Brownian motion is a stationary Ornstein–Uhlenbeck process.

theorem IsPreBrownianReal.isStationaryOrnsteinUhlenbeck_ouStationaryOfBrownian
    {B : ℝ≥0 → Ω → ℝ} (hB : IsPreBrownianReal B P) {θ : ℝ} (hθ : 0 < θ) (σ : ℝ) :
    IsStationaryOrnsteinUhlenbeck θ σ (ouStationaryOfBrownian θ σ B) P

Uses 4 · Used by 1

Statement usesStationary Ornstein–Uhlenbeck process · Doob's stationary time change of Brownian motion

Proof usesDoob's clock for the stationary Ornstein–Uhlenbeck process · Covariance of the stationary Ornstein–Uhlenbeck process

Used byExistence of the stationary Ornstein–Uhlenbeck process

TheoremExistence of a pre-Brownian motion on path space#✓fully proved

There is a probability measure on paths ℝ≥0 → ℝ under which the coordinate process is a pre-Brownian motion (Kolmogorov extension of the Brownian finite-dimensional laws).

theorem exists_isPreBrownianReal_eval :
    ∃ μ : Measure (ℝ≥0 → ℝ), IsPreBrownianReal (fun t f ↦ f t) μ

Uses 1 · Used by 2

Proof usesKolmogorov extension theorem

Used byExistence of the Ornstein–Uhlenbeck process started at zero · Existence of the stationary Ornstein–Uhlenbeck process

TheoremExistence of the Ornstein–Uhlenbeck process started at zero#✓fully proved

An Ornstein–Uhlenbeck process started at 0 exists for every θ > 0 and σ.

theorem exists_isOrnsteinUhlenbeckFromZero {θ : ℝ} (hθ : 0 < θ) (σ : ℝ) :
    ∃ μ : Measure (ℝ≥0 → ℝ), ∃ X : ℝ≥0 → (ℝ≥0 → ℝ) → ℝ, IsOrnsteinUhlenbeckFromZero θ σ X μ

Uses 4

Statement usesOrnstein–Uhlenbeck process started at zero

Proof usesConstruction (Doob 1942) · Existence of a pre-Brownian motion on path space · Doob's time change of Brownian motion

TheoremExistence of the stationary Ornstein–Uhlenbeck process#✓fully proved

A stationary Ornstein–Uhlenbeck process exists for every θ > 0 and σ.

theorem exists_isStationaryOrnsteinUhlenbeck {θ : ℝ} (hθ : 0 < θ) (σ : ℝ) :
    ∃ μ : Measure (ℝ≥0 → ℝ), ∃ X : ℝ≥0 → (ℝ≥0 → ℝ) → ℝ,
      IsStationaryOrnsteinUhlenbeck θ σ X μ

Uses 4

Statement usesStationary Ornstein–Uhlenbeck process

Proof usesConstruction (Doob 1942) · Existence of a pre-Brownian motion on path space · Doob's stationary time change of Brownian motion

TheoremOne-time law of the Ornstein–Uhlenbeck process from zero#✓fully proved

The one-time law of the OU process started at 0: X t ~ N(0, (σ² / (2θ)) (1 - e^{-2θt})).

theorem IsOrnsteinUhlenbeckFromZero.hasLaw_eval {θ σ : ℝ} {X : ℝ≥0 → Ω → ℝ}
    (hX : IsOrnsteinUhlenbeckFromZero θ σ X P) (t : ℝ≥0) :
    HasLaw (X t) (gaussianReal 0 (σ ^ 2 / (2 * θ) * (1 - exp (-2 * θ * t))).toNNReal) P

Uses 3 · Used by 1

Statement usesOrnstein–Uhlenbeck process started at zero

Proof usesCovariance of the Ornstein–Uhlenbeck process started at zero · Variance of the Ornstein–Uhlenbeck process started at zero

Used byThe Ornstein–Uhlenbeck process from zero starts at zero

TheoremThe Ornstein–Uhlenbeck process from zero starts at zero#✓fully proved

The OU process of IsOrnsteinUhlenbeckFromZero starts at 0 almost surely.

theorem IsOrnsteinUhlenbeckFromZero.eval_zero_ae_eq_zero {θ σ : ℝ} {X : ℝ≥0 → Ω → ℝ}
    (hX : IsOrnsteinUhlenbeckFromZero θ σ X P) : ∀ᵐ ω ∂P, X 0 ω = 0

Uses 2

Statement usesOrnstein–Uhlenbeck process started at zero

Proof usesOne-time law of the Ornstein–Uhlenbeck process from zero

TheoremRelaxation to stationarity#✓fully proved

For the process started at 0, cov(X (s + h), X (t + h)) → (σ² / (2θ)) e^{-θ|t-s|} as h → ∞.

theorem IsOrnsteinUhlenbeckFromZero.tendsto_covariance_add {θ σ : ℝ} {X : ℝ≥0 → Ω → ℝ}
    (hX : IsOrnsteinUhlenbeckFromZero θ σ X P) (s t : ℝ≥0) :
    Tendsto (fun h : ℝ≥0 ↦ cov[X (s + h), X (t + h); P]) atTop
      (𝓝 (ouStationaryCovariance θ σ s t))

Uses 4

Statement usesOrnstein–Uhlenbeck process started at zero · Covariance of the stationary Ornstein–Uhlenbeck process

Proof usesCovariance of the Ornstein–Uhlenbeck process started at zero · Ornstein–Uhlenbeck covariance converges to the stationary one

TheoremStationary law#✓fully proved

Each X t of a stationary OU process is N(0, σ² / (2θ)).

theorem IsStationaryOrnsteinUhlenbeck.hasLaw_eval {θ σ : ℝ} {X : ℝ≥0 → Ω → ℝ}
    (hX : IsStationaryOrnsteinUhlenbeck θ σ X P) (t : ℝ≥0) :
    HasLaw (X t) (gaussianReal 0 (σ ^ 2 / (2 * θ)).toNNReal) P

Uses 3

Statement usesStationary Ornstein–Uhlenbeck process

Proof usesCovariance of the stationary Ornstein–Uhlenbeck process · Variance of the stationary Ornstein–Uhlenbeck process

TheoremGaussian process laws are determined by mean and covariance#✓fully proved

The finite-dimensional laws of a real Gaussian process are determined by its mean and covariance functions: two Gaussian processes with the same means and covariances (possibly on different probability spaces) have the same finite-dimensional laws.

theorem IsGaussianProcess.map_restrict_eq_of_covariance_eq {T Ω' : Type*}
    {mΩ' : MeasurableSpace Ω'} {Q : Measure Ω'} {X : T → Ω → ℝ} {Y : T → Ω' → ℝ}
    (hX : IsGaussianProcess X P) (hY : IsGaussianProcess Y Q)
    (hmean : ∀ t, P[X t] = Q[Y t]) (hcov : ∀ s t, cov[X s, X t; P] = cov[Y s, Y t; Q])
    (I : Finset T) :
    P.map (fun ω ↦ I.restrict (X · ω)) = Q.map (fun ω ↦ I.restrict (Y · ω))

Used by 1

Used byStrict stationarity

TheoremTime shifts of a stationary Ornstein–Uhlenbeck process#✓fully proved

A time shift of a stationary OU process is a stationary OU process.

theorem IsStationaryOrnsteinUhlenbeck.shift {θ σ : ℝ} {X : ℝ≥0 → Ω → ℝ}
    (hX : IsStationaryOrnsteinUhlenbeck θ σ X P) (h : ℝ≥0) :
    IsStationaryOrnsteinUhlenbeck θ σ (fun t ↦ X (t + h)) P

Uses 2 · Used by 1

Statement usesStationary Ornstein–Uhlenbeck process

Proof usesCovariance of the stationary Ornstein–Uhlenbeck process

Used byStrict stationarity

TheoremStrict stationarity#✓fully proved

Every finite-dimensional law of a stationary OU process is invariant under time shifts.

theorem IsStationaryOrnsteinUhlenbeck.map_restrict_shift {θ σ : ℝ} {X : ℝ≥0 → Ω → ℝ}
    (hX : IsStationaryOrnsteinUhlenbeck θ σ X P) (h : ℝ≥0) (I : Finset ℝ≥0) :
    P.map (fun ω ↦ I.restrict (fun t ↦ X (t + h) ω)) = P.map (fun ω ↦ I.restrict (X · ω))

Uses 4

Statement usesStationary Ornstein–Uhlenbeck process

Proof usesGaussian process laws are determined by mean and covariance · Time shifts of a stationary Ornstein–Uhlenbeck process · Covariance of the stationary Ornstein–Uhlenbeck process

TheoremConditional expectation of a Gaussian process given its past#✓fully proved

For a centered Gaussian process with cov(X u, X t) = c cov(X u, X s) for all u ≤ s, the conditional expectation of X t given the natural filtration at s is c X s.

theorem IsGaussianProcess.condExp_natural_eq_of_covariance {X : ℝ≥0 → Ω → ℝ}
    (hX : IsGaussianProcess X P) (hm : ∀ t, StronglyMeasurable (X t))
    (hint : ∀ t, P[X t] = 0) {s t : ℝ≥0} (c : ℝ)
    (hc : ∀ u ≤ s, cov[X u, X t; P] = c * cov[X u, X s; P]) :
    P[X t | Filtration.natural X hm s] =ᵐ[P] fun ω ↦ c * X s ω

Used by 2

Used byMean reversion · Mean reversion

TheoremConditional law of a Gaussian process at one time given another#✓fully proved

For a centered Gaussian process with cov(X s, X t) = c Var(X s), the conditional law of X t given X s = x is N(c x, Var(X t) - c² Var(X s)) for almost every x.

theorem IsGaussianProcess.condDistrib_eval_eq_of_covariance {T : Type*}
    {X : T → Ω → ℝ} (hX : IsGaussianProcess X P) (hm : ∀ t, Measurable (X t))
    (hint : ∀ t, P[X t] = 0) {s t : T} (c : ℝ) (hc : cov[X s, X t; P] = c * Var[X s; P]) :
    haveI := hX.isProbabilityMeasure
    ∀ᵐ x ∂(P.map (X s)),
      condDistrib (X t) (X s) P x =
        gaussianReal (c * x) (Var[X t; P] - c ^ 2 * Var[X s; P]).toNNReal

Uses 2 · Used by 2

Proof usesGaussian conditioning · The additive-noise kernel

Used byTransition law · Transition law

TheoremMean reversion#✓fully proved

For the OU process started at 0 and s ≤ t, E[X t | F s] = e^{-θ(t-s)} X s, where F is the natural filtration of X.

theorem IsOrnsteinUhlenbeckFromZero.condExp_natural {θ σ : ℝ} {X : ℝ≥0 → Ω → ℝ}
    (hX : IsOrnsteinUhlenbeckFromZero θ σ X P) (hm : ∀ t, StronglyMeasurable (X t)) {s t : ℝ≥0}
    (hst : s ≤ t) :
    P[X t | Filtration.natural X hm s] =ᵐ[P] fun ω ↦ exp (-θ * (t - s)) * X s ω

Uses 3

Statement usesOrnstein–Uhlenbeck process started at zero

Proof usesConditional expectation of a Gaussian process given its past · Covariance of the Ornstein–Uhlenbeck process started at zero

TheoremMean reversion#✓fully proved

For the stationary OU process and s ≤ t, E[X t | F s] = e^{-θ(t-s)} X s, where F is the natural filtration of X.

theorem IsStationaryOrnsteinUhlenbeck.condExp_natural {θ σ : ℝ} {X : ℝ≥0 → Ω → ℝ}
    (hX : IsStationaryOrnsteinUhlenbeck θ σ X P) (hm : ∀ t, StronglyMeasurable (X t))
    {s t : ℝ≥0} (hst : s ≤ t) :
    P[X t | Filtration.natural X hm s] =ᵐ[P] fun ω ↦ exp (-θ * (t - s)) * X s ω

Uses 3

Statement usesStationary Ornstein–Uhlenbeck process

Proof usesConditional expectation of a Gaussian process given its past · Covariance of the stationary Ornstein–Uhlenbeck process

TheoremTransition law#✓fully proved

For the OU process started at 0 and s ≤ t, the conditional law of X t given X s = x is N(e^{-θ(t-s)} x, (σ² / (2θ)) (1 - e^{-2θ(t-s)})) for almost every x.

theorem IsOrnsteinUhlenbeckFromZero.condDistrib_eval {θ σ : ℝ}
    {X : ℝ≥0 → Ω → ℝ} (hX : IsOrnsteinUhlenbeckFromZero θ σ X P)
    (hm : ∀ t, Measurable (X t)) {s t : ℝ≥0} (hst : s ≤ t) :
    haveI := hX.isGaussianProcess.isProbabilityMeasure
    ∀ᵐ x ∂(P.map (X s)), condDistrib (X t) (X s) P x =
      gaussianReal (exp (-θ * (t - s)) * x)
        (σ ^ 2 / (2 * θ) * (1 - exp (-2 * θ * (t - s)))).toNNReal

Uses 4

Statement usesOrnstein–Uhlenbeck process started at zero

Proof usesConditional law of a Gaussian process at one time given another · Covariance of the Ornstein–Uhlenbeck process started at zero · Variance of the Ornstein–Uhlenbeck process started at zero

TheoremTransition law#✓fully proved

For the stationary OU process and s ≤ t, the conditional law of X t given X s = x is N(e^{-θ(t-s)} x, (σ² / (2θ)) (1 - e^{-2θ(t-s)})) for almost every x.

theorem IsStationaryOrnsteinUhlenbeck.condDistrib_eval {θ σ : ℝ}
    {X : ℝ≥0 → Ω → ℝ} (hX : IsStationaryOrnsteinUhlenbeck θ σ X P)
    (hm : ∀ t, Measurable (X t)) {s t : ℝ≥0} (hst : s ≤ t) :
    haveI := hX.isGaussianProcess.isProbabilityMeasure
    ∀ᵐ x ∂(P.map (X s)), condDistrib (X t) (X s) P x =
      gaussianReal (exp (-θ * (t - s)) * x)
        (σ ^ 2 / (2 * θ) * (1 - exp (-2 * θ * (t - s)))).toNNReal

Uses 4

Statement usesStationary Ornstein–Uhlenbeck process

Proof usesConditional law of a Gaussian process at one time given another · Covariance of the stationary Ornstein–Uhlenbeck process · Variance of the stationary Ornstein–Uhlenbeck process

DefinitionPathwise solution of the Langevin equation#✓fully proved

The explicit solution of the pathwise Langevin equation driven by a path w: e^{-θt} x₀ + σ (w t - e^{-θt} w 0 - θ ∫_0^t e^{-θ(t-u)} w u du). This is e^{-θt} x₀ + σ ∫_0^t e^{-θ(t-u)} dw(u) after integration by parts (the Itô-integral form for a Brownian path is a wanted statement).

noncomputable def ouPathSolution (θ σ x₀ : ℝ) (w : ℝ → ℝ) (t : ℝ) : ℝ :=
  exp (-θ * t) * x₀ +
    σ * (w t - exp (-θ * t) * w 0 - θ * ∫ u in (0 : ℝ)..t, exp (-θ * (t - u)) * w u)

Used by 9

Used byThe Itô form of the Ornstein–Uhlenbeck solution · The Ornstein–Uhlenbeck solution in Itô form · Ornstein–Uhlenbeck path solution by integration by parts · Continuity of the pathwise Langevin solution · Uniqueness · The pathwise Langevin solution driven by Brownian motion is Gaussian · The pathwise Langevin solution is an OU process · Stationary start · Pathwise Langevin equation

TheoremContinuity of the pathwise Langevin solution#✓fully proved

The pathwise solution is continuous when the driving path is.

theorem continuous_ouPathSolution (θ σ x₀ : ℝ) {w : ℝ → ℝ} (hw : Continuous w) :
    Continuous (ouPathSolution θ σ x₀ w)

Uses 1 · Used by 2

Statement usesPathwise solution of the Langevin equation

Used byUniqueness · Pathwise Langevin equation

TheoremPathwise Langevin equation#✓fully proved

For a continuous path w and every real t, ouPathSolution θ σ x₀ w satisfies x t = x₀ - θ ∫_0^t x + σ (w t - w 0) (any real θ, σ, x₀).

theorem ouPathSolution_integral_eq (θ σ x₀ : ℝ) {w : ℝ → ℝ} (hw : Continuous w) (t : ℝ) :
    ouPathSolution θ σ x₀ w t =
      x₀ - θ * (∫ u in (0 : ℝ)..t, ouPathSolution θ σ x₀ w u) + σ * (w t - w 0)

Uses 2 · Used by 1

Statement usesPathwise solution of the Langevin equation

Proof usesContinuity of the pathwise Langevin solution

Used byUniqueness

TheoremUniqueness#✓fully proved

A continuous solution of x t = x₀ - θ ∫_0^t x + σ (w t - w 0) on t ≥ 0 equals ouPathSolution θ σ x₀ w there.

theorem eq_ouPathSolution_of_integral_eq {θ σ x₀ : ℝ} {w x : ℝ → ℝ} (hw : Continuous w)
    (hx : Continuous x)
    (h : ∀ t, 0 ≤ t → x t = x₀ - θ * (∫ u in (0 : ℝ)..t, x u) + σ * (w t - w 0))
    {t : ℝ} (ht : 0 ≤ t) : x t = ouPathSolution θ σ x₀ w t

Uses 3

Statement usesPathwise solution of the Langevin equation

Proof usesContinuity of the pathwise Langevin solution · Pathwise Langevin equation

TheoremElementary Itô integrals agree for modifications#✓fully proved

Elementary Itô integrals against two modifications of the same process agree almost surely.

theorem ElementaryIntegrand.itoIntegral_ae_eq_of_ae_eq {Ω : Type*} {mΩ : MeasurableSpace Ω}
    {F : Filtration ℝ≥0 mΩ} {P : Measure Ω} (H : ElementaryIntegrand F) {B B' : ℝ≥0 → Ω → ℝ}
    (h : ∀ t, B t =ᵐ[P] B' t) (t : ℝ≥0) : H.itoIntegral B t =ᵐ[P] H.itoIntegral B' t

Uses 2 · Used by 1

Statement usesElementary integrand · Itô integral of an elementary integrand

Used byThe pathwise Langevin solution driven by Brownian motion is Gaussian

TheoremAdjoining an independent Gaussian variable#✓fully proved

If X₀ is a real Gaussian random variable independent of the real Gaussian process B, the process indexed by Option T that is X₀ at none and B t at some t is a Gaussian process.

theorem IsGaussianProcess.option_elim {Ω : Type*} {mΩ : MeasurableSpace Ω} {P : Measure Ω}
    {T : Type*} {X₀ : Ω → ℝ} {B : T → Ω → ℝ} (hX₀ : HasGaussianLaw X₀ P)
    (hB : IsGaussianProcess B P) (hind : IndepFun X₀ (fun ω t ↦ B t ω) P) :
    IsGaussianProcess (fun (o : Option T) ω ↦ o.elim (X₀ ω) (fun t ↦ B t ω)) P

Used by 1

Used byThe pathwise Langevin solution driven by Brownian motion is Gaussian

TheoremCovariance of the Wiener integrals#✓fully proved

Covariance of the Wiener integrals I_t = ∫_0^t e^{θu} dB_u: for a pre-Brownian motion B adapted to F with increments independent of the past and θ ≠ 0, E[I_s I_t] = (e^{2θ (s ∧ t)} - 1) / (2θ), by the martingale property and the Itô isometry.

theorem integral_itoIntegralL2_exp_mul {Ω : Type*} {mΩ : MeasurableSpace Ω} {P : Measure Ω}
    {F : Filtration ℝ≥0 mΩ} {B : ℝ≥0 → Ω → ℝ} (hB : IsPreBrownianReal B P) (hBF : Adapted F B)
    (hInd : ∀ s t, s ≤ t → Indep (MeasurableSpace.comap (fun ω ↦ B t ω - B s ω) inferInstance)
      (F s) P) {θ : ℝ} (hθ : θ ≠ 0) (s t : ℝ≥0) :
    ∫ ω, (itoIntegralL2 P F B (fun u _ ↦ exp (θ * u)) s : Ω → ℝ) ω *
      (itoIntegralL2 P F B (fun u _ ↦ exp (θ * u)) t : Ω → ℝ) ω ∂P =
      (exp (2 * θ * min (s : ℝ) t) - 1) / (2 * θ)

Uses 13 · Used by 1

Statement usesItô integral as an element of \(L^2\)

Proof usesElementary integrand · Left-point step approximation of a deterministic integrand · Elementary integrand as a process · Itô-approximable process · Squared \(L^2\) distance between integrands · Itô integral process · Itô integral process is a version of the \(L^2\) integral · Itô isometry · Martingale property of the Itô integral · Restriction to (0, t) preserves joint measurability · Restriction of a process to the time interval (0, t) · \(L^2\) convergence of left-point approximations of a continuous function

Used byThe pathwise Langevin solution driven by Brownian motion is Gaussian

TheoremThe pathwise Langevin solution driven by Brownian motion is Gaussian#✓fully proved

For a Brownian motion B, θ ≠ 0, any real σ, and a start X₀ ~ N(0, v) independent of B, the process X t = ouPathSolution θ σ X₀ B t (t ≥ 0) is a Gaussian process with E[X t] = 0 and cov[X s, X t] = e^{-θ(s+t)} (v + σ² (e^{2θ (s ∧ t)} - 1) / (2θ)) (Karatzas–Shreve 1991, Section 5.6).

theorem IsBrownianReal.isGaussianProcess_ouPathSolution {Ω : Type*} {mΩ : MeasurableSpace Ω}
    {P : Measure Ω} {B : ℝ≥0 → Ω → ℝ} (hB : IsBrownianReal B P) {θ : ℝ} (hθ : θ ≠ 0) (σ : ℝ)
    {X₀ : Ω → ℝ} {v : ℝ≥0} (hX₀ : HasLaw X₀ (gaussianReal 0 v) P)
    (hind : IndepFun X₀ (fun ω t ↦ B t ω) P) :
    IsGaussianProcess
        (fun (t : ℝ≥0) ω ↦ ouPathSolution θ σ (X₀ ω) (fun u ↦ B (Real.toNNReal u) ω) t) P ∧
      (∀ t : ℝ≥0, P[fun ω ↦ ouPathSolution θ σ (X₀ ω) (fun u ↦ B (Real.toNNReal u) ω) t] = 0) ∧
      ∀ s t : ℝ≥0,
        cov[fun ω ↦ ouPathSolution θ σ (X₀ ω) (fun u ↦ B (Real.toNNReal u) ω) s,
          fun ω ↦ ouPathSolution θ σ (X₀ ω) (fun u ↦ B (Real.toNNReal u) ω) t; P] =
          exp (-θ * (s + t)) * (v + σ ^ 2 * ((exp (2 * θ * min (s : ℝ) t) - 1) / (2 * θ)))

Uses 18 · Used by 2

Statement usesPathwise solution of the Langevin equation

Proof usesItô integral of an elementary integrand · Elementary Itô integrals agree for modifications · Itô integral of a Riemann step approximation · Square integrability of the elementary Itô integral · Left-point step approximation of a deterministic integrand · The Itô form of the Ornstein–Uhlenbeck solution · Closure of Gaussian processes under L² limits · Adjoining an independent Gaussian variable · Increments are independent of the past · Processes with measurable coordinates are adapted to their natural filtration · Covariance of the Wiener integrals · Itô integral as an element of \(L^2\) · Restriction to (0, t) preserves joint measurability · Continuity of the second moment pairing in L² · \(L^2\) convergence of left-point approximations of a continuous function · The Itô integral is well defined · Function as an element of \(L^2\)

Used byThe pathwise Langevin solution is an OU process · Stationary start

TheoremThe pathwise Langevin solution is an OU process#✓fully proved

Driven by a Brownian motion and started at 0, ouPathSolution is an Ornstein–Uhlenbeck process started at 0 (Karatzas–Shreve 1991, Section 5.6). No filtration and no measurability of the coordinates of B is assumed.

theorem IsBrownianReal.isOrnsteinUhlenbeckFromZero_ouPathSolution {Ω : Type*}
    {mΩ : MeasurableSpace Ω} {P : Measure Ω} {B : ℝ≥0 → Ω → ℝ} (hB : IsBrownianReal B P)
    {θ : ℝ} (hθ : 0 < θ) (σ : ℝ) :
    IsOrnsteinUhlenbeckFromZero θ σ
      (fun t ω ↦ ouPathSolution θ σ 0 (fun u ↦ B (Real.toNNReal u) ω) t) P

Uses 4

Statement usesOrnstein–Uhlenbeck process started at zero · Pathwise solution of the Langevin equation

Proof usesThe pathwise Langevin solution driven by Brownian motion is Gaussian · Covariance of the Ornstein–Uhlenbeck process started at zero

TheoremStationary start#✓fully proved

Driven by a Brownian motion B and started from X₀ ~ N(0, σ²/(2θ)) independent of B, ouPathSolution is a stationary Ornstein–Uhlenbeck process (Karatzas–Shreve 1991, Section 5.6).

theorem IsBrownianReal.isStationaryOrnsteinUhlenbeck_ouPathSolution {Ω : Type*}
    {mΩ : MeasurableSpace Ω} {P : Measure Ω} {B : ℝ≥0 → Ω → ℝ} (hB : IsBrownianReal B P)
    {θ : ℝ} (hθ : 0 < θ) (σ : ℝ) {X₀ : Ω → ℝ}
    (hX₀ : HasLaw X₀ (gaussianReal 0 (σ ^ 2 / (2 * θ)).toNNReal) P)
    (hind : IndepFun X₀ (fun ω t ↦ B t ω) P) :
    IsStationaryOrnsteinUhlenbeck θ σ
      (fun t ω ↦ ouPathSolution θ σ (X₀ ω) (fun u ↦ B (Real.toNNReal u) ω) t) P

Uses 4

Statement usesStationary Ornstein–Uhlenbeck process · Pathwise solution of the Langevin equation

Proof usesThe pathwise Langevin solution driven by Brownian motion is Gaussian · Covariance of the stationary Ornstein–Uhlenbeck process

40 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.