Dynkin Identity for Compactly Supported Diffusions

This formalizes the Dynkin identity associated with the diffusion generator. Let $Y$ be an IsDiffusion in $\mathbb R^N$ with drift $b$ and noise columns $\sigma_k$. Assume $b$ and each $\sigma_k$ are continuous and compactly supported, the filtration satisfies the stated pre-zero and null-set conditions, and $F:\mathbb R^N\to\mathbb R$ is $C^2$. For every $T\ge0$, $F(Y_T)$ is integrable and

where $\mathcal L$ is diffusionGenerator b σ F. This is the generator-form expectation identity used in the diffusion formalization.

Original Lean declaration header

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

theorem IsDiffusion.dynkin {W : MultidimBrownianMotion P d}
    {ℱ : Filtration ℝ ‹MeasurableSpace Ω›} {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 → ℝ} {x₀ : Fin N → ℝ}
    (hbc : Continuous b) (hσc : ∀ k, Continuous fun x => σ x k)
    (hbs : HasCompactSupport b) (hσs : ∀ k, HasCompactSupport fun x => σ x k)
    {Y : ℝ → Ω → Fin N → ℝ} (h : IsDiffusion W ℱ hW b σ x₀ Y)
    {F : (Fin N → ℝ) → ℝ} (hF : ContDiff ℝ 2 F) {T : ℝ} (hT : 0 ≤ T) :
    Integrable (fun ω => F (Y T ω)) P ∧
      ∫ ω, F (Y T ω) ∂P - F x₀ =
        ∫ ω, ∫ s in Set.Ioc (0 : ℝ) T, diffusionGenerator b σ F (Y s ω) ∂volume ∂P

Module navigation

Module: Probability/Diffusion/Dynkin.

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

Supporting theorems: IsVectorItoVersion.itoFormula_localise, itoFormula_of_unbounded_coeff, version_ae_eq_zero.

Next: weighted_noise_zero.

Source excerpt, lines 97–108 · Frozen source 408915f.