Transported Dynkin Identity in Finite Dimensions

Proved

FunctionalInequalities.Probability.Diffusion.IsDiffusion.dynkin_transport_readable

by Lazyfill · Oct 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This is Dynkin's identity in a finite-dimensional state space $V$ . Let $\Phi:V\simeq\mathrm{Fin}(N)\to\mathbb R$ be a continuous linear equivalence. Assume the coordinate process $\Phi\circ Y$ is an IsDiffusion with transported drift and noise, while $b$ and each $\sigma_k$ on $V$ are continuous and compactly supported; also assume the stated filtration, null-set, and $C^2$ hypotheses. For every $T\ge0$ , $F(Y_T)$ is integrable and

\mathbb E[F(Y_T)]-F(x_0) =\mathbb E\!\left[\int_{(0,T]}\mathcal L_{b,\sigma}F(Y_s)\,ds\right].

The generator on the right is the coordinate-free diffusionGenerator b σ F; the transported coordinate generator is identified with it by diffusionGenerator_transport_readable.

Original Lean declaration header

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

theorem IsDiffusion.dynkin_transport (Φ : V ≃L[ℝ] (Fin N → ℝ))
    (hℱ0 : ∀ t : ℝ, t ≤ 0 → ℱ 0 ≤ ℱ t)
    (hnull : ∀ s : Set Ω, MeasurableSet s → P s = 0 → MeasurableSet[ℱ 0] s)
    {b : V → V} {σ : V → Fin d → V} {x₀ : V}
    (hbc : Continuous b) (hσc : ∀ k, Continuous fun x => σ x k)
    (hbs : HasCompactSupport b) (hσs : ∀ k, HasCompactSupport fun x => σ x k)
    {Y : ℝ → Ω → V}
    (h : IsDiffusion W ℱ hW (transportDrift Φ b) (transportNoise Φ σ) (Φ x₀) (fun t ω => Φ (Y t ω)))
    {F : V → ℝ} (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/Transport.

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

Supporting theorems: IsDiffusion.dynkin, diffusionGenerator_transport.

Source excerpt, lines 43–54 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Diffusion_Transport

open MeasureTheory ProbabilityTheory Filter Topology
variable {Ω : Type*} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {N d : ℕ}
  {W : LevyStochCalc.Brownian.Multidim.MultidimBrownianMotion P d} {ℱ : MeasureTheory.Filtration ℝ ‹MeasurableSpace Ω›}
  {hW : ∀ k, LevyStochCalc.Brownian.IsBrownianFiltration (W.W k) ℱ}
variable {V : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V]

Formal statement


theorem FunctionalInequalities.Probability.Diffusion.IsDiffusion.dynkin_transport_readable (Φ : V ≃L[ℝ] (Fin N → ℝ))
    (hℱ0 : ∀ t : ℝ, t ≤ 0 → ℱ 0 ≤ ℱ t)
    (hnull : ∀ s : Set Ω, MeasurableSet s → P s = 0 → MeasurableSet[ℱ 0] s)
    {b : V → V} {σ : V → Fin d → V} {x₀ : V}
    (hbc : Continuous b) (hσc : ∀ k, Continuous fun x => σ x k)
    (hbs : HasCompactSupport b) (hσs : ∀ k, HasCompactSupport fun x => σ x k)
    {Y : ℝ → Ω → V}
    (h : IsDiffusion W ℱ hW (transportDrift Φ b) (transportNoise Φ σ) (Φ x₀) (fun t ω => Φ (Y t ω)))
    {F : V → ℝ} (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 := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Probability/Diffusion/Transport.lean#L39-L109 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Probability.Diffusion.Transport`, declaration `FunctionalInequalities.Probability.Diffusion.IsDiffusion.dynkin_transport`; the repository is private at upload time).

View graph