Existence Of A Globally Lipschitz Bounded Diffusion

This theorem establishes existence of a diffusion on a Brownian filtered probability space. Let $(\Omega,P)$ be a probability space, let $W$ be a $d$-dimensional Brownian motion, and let $\mathcal F$ be a right-continuous filtration making each coordinate Brownian. Assume the filtration ordering and null-set hypotheses in the statement. Let

and let $K\in[0,\infty)$ be an NNReal. Suppose $b$ and every $x\mapsto\sigma(x,k)$ are $K$-Lipschitz. Suppose also that for some $B\in\mathbb R$,

for all $x$ and $k$. Then for every initial state $x_0\in\mathbb R^N$ there exists a path map $Y:\mathbb R\to\Omega\to\mathbb R^N$ such that IsDiffusion W ℱ hW b σ x₀ Y holds. The bundled predicate supplies the diffusion's measurability, adaptedness, continuity, and Itô representation properties.

Original Lean declaration header

Within namespace FunctionalInequalities.Probability.Diffusion. Shown in its original module context. Proof omitted.

theorem exists_isDiffusion (W : MultidimBrownianMotion P d)
    (ℱ : Filtration ℝ ‹MeasurableSpace Ω›) [ℱ.IsRightContinuous]
    (hW : ∀ k, IsBrownianFiltration (W.W k) ℱ)
    (hℱ0 : ∀ t : ℝ, t ≤ 0 → ℱ 0 ≤ ℱ t)
    (hnull : ∀ s : Set Ω, MeasurableSet s → P s = 0 → MeasurableSet[ℱ 0] s)
    {b : (Fin N → ℝ) → Fin N → ℝ} {σ : (Fin N → ℝ) → Fin d → Fin N → ℝ} {K : ℝ≥0}
    (hb : LipschitzWith K b) (hσ : ∀ k, LipschitzWith K fun x => σ x k)
    {B : ℝ} (hbB : ∀ x, ‖b x‖ ≤ B) (hσB : ∀ x k, ‖σ x k‖ ≤ B) (x₀ : Fin N → ℝ) :
    ∃ Y : ℝ → Ω → Fin N → ℝ, IsDiffusion W ℱ hW b σ x₀ Y

Module navigation

Module: Probability/Diffusion/Existence.

Definition modules: LevyStochCalc/Brownian/Filtered, LevyStochCalc/Brownian/Multidim, Probability/Diffusion/Setup.

Supporting theorems: exists_isVectorItoVersion_of_unbounded, vectorItoProcess_ae_eq_zero, exists_globalSolution, itoIntegral_congr_ae, diffusionCoeffs_lipschitz.

Previous: diffusionCoeffs_lipschitz.

Source excerpt, lines 164–172 · Frozen source 408915f.