Global Chain Rule for the Diffusion Generator

This formalizes the global chain rule for diffusionGenerator, identified in the source as step (82) of Bizeul–Klartag–Lehec (arXiv:2610.05474v1).

Let $V$ and $W$ be real normed additive groups, let $d\in\mathbb N$, let $b:V\to V$ be a drift field, let $\sigma:V\to\mathrm{Fin}(d)\to V$ be the noise field, let $\Phi:W\to\mathbb R$, let $G:V\to W$, and let $x\in V$. Assume that $\Phi$ and $G$ are globally $C^2$ (ContDiff ℝ 2).

Writing $\sigma_k(x)=\sigma(x,k)$, the generator of the composite satisfies

Here diffusionGenerator is the first-order drift term plus one half of the diagonal second-derivative noise sum. The statement is a reusable coordinate-free composition rule on normed spaces; it is an equality at every point, not merely almost everywhere.

Original Lean declaration header

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

theorem diffusionGenerator_comp {V W : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V]
    [NormedAddCommGroup W] [NormedSpace ℝ W] {d : ℕ} (b : V → V) (σ : V → Fin d → V)
    (Φ : W → ℝ) (G : V → W) (x : V) (hΦ : ContDiff ℝ 2 Φ) (hG : ContDiff ℝ 2 G) :
    diffusionGenerator b σ (Φ ∘ G) x =
      fderiv ℝ Φ (G x) (fderiv ℝ G x (b x) +
          (1 / 2 : ℝ) • ∑ k, fderiv ℝ (fderiv ℝ G) x (σ x k) (σ x k)) +
        (1 / 2 : ℝ) * ∑ k, fderiv ℝ (fderiv ℝ Φ) (G x) (fderiv ℝ G x (σ x k)) (fderiv ℝ G x (σ x k))

Module navigation

Module: Probability/Diffusion/Generator.

Previous: diffusionGenerator_transport · Next: diffusionGenerator_comp_of_contDiffAt.

Source excerpt, lines 88–94 · Frozen source 408915f.