Diffusion Generator Under Linear Coordinate Transport

Proved

FunctionalInequalities.Probability.Diffusion.diffusionGenerator_transport_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

Let $V,V'$ be finite-dimensional real normed spaces, let $\Phi:V\simeq V'$ be a continuous linear equivalence, let $b:V\to V$ , $\sigma:V\to\mathrm{Fin}(d)\to V$ , and $F:V\to\mathbb R$ . For every $x\in V$ , the generator is invariant under transport:

\mathcal L_{\Phi_*b,\Phi_*\sigma}(F\circ\Phi^{-1})(\Phi x) =\mathcal L_{b,\sigma}F(x).

Here transportDrift, transportNoise, and diffusionGenerator are the Lean definitions involved. No differentiability assumption on $F$ is included in the theorem statement.

Original Lean declaration header

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

theorem diffusionGenerator_transport {V' : Type*} [NormedAddCommGroup V'] [NormedSpace ℝ V']
    {d : ℕ} (Φ : V ≃L[ℝ] V') (b : V → V) (σ : V → Fin d → V) (F : V → ℝ) (x : V) :
    diffusionGenerator (transportDrift Φ b) (transportNoise Φ σ) (F ∘ Φ.symm) (Φ x) =
      diffusionGenerator b σ F x

Module navigation

Module: Probability/Diffusion/Generator.

Next: diffusionGenerator_comp.

Source excerpt, lines 46–49 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Diffusion_Generator

variable {V : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V]

Formal statement


theorem FunctionalInequalities.Probability.Diffusion.diffusionGenerator_transport_readable {V' : Type*} [NormedAddCommGroup V'] [NormedSpace ℝ V']
    {d : ℕ} (Φ : V ≃L[ℝ] V') (b : V → V) (σ : V → Fin d → V) (F : V → ℝ) (x : V) :
    diffusionGenerator (transportDrift Φ b) (transportNoise Φ σ) (F ∘ Φ.symm) (Φ x) =
      diffusionGenerator b σ F x := by sorry

Source

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

View graph