Lipschitz Bound For Transported Diffusion Coefficients

This auxiliary lemma concerns autonomous coefficients. Let $b:(\mathbb R^N)\to\mathbb R^N$ and $\sigma:(\mathbb R^N)\to(\mathbb R^d\to\mathbb R^N)$, and let $K\in[0,\infty)$ be an NNReal. If $b$ is $K$-Lipschitz and every map $x\mapsto\sigma(x,k)$ is $K$-Lipschitz, then there exists $L\in\mathbb R$ such that the corresponding diffusionCoeffs b σ are IsLipschitz with respect to the zero measure on the unit space:

This declaration serves as a technical bridge from componentwise Lipschitz hypotheses to the bundled coefficient condition.

Original Lean declaration header

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

private theorem diffusionCoeffs_lipschitz {N d : ℕ}
    {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) :
    ∃ L : ℝ, (diffusionCoeffs b σ).IsLipschitz (0 : Measure Unit) L

Module navigation

Module: Probability/Diffusion/Existence.

Definition modules: LevyStochCalc/Ito/Setting.

Next: exists_isDiffusion.

Source excerpt, lines 109–113 · Frozen source 408915f.