Local Chain Rule for the Diffusion Generator

This is the local, pointwise form of the chain rule for diffusionGenerator.

Let $V$ and $W$ be real normed additive groups, let $d\in\mathbb N$, let $b:V\to V$, $\sigma:V\to\mathrm{Fin}(d)\to V$, $\Phi:W\to\mathbb R$, $G:V\to W$, and $x\in V$. Assume only that $\Phi$ is $C^2$ at $G(x)$ and $G$ is $C^2$ at $x$, namely ContDiffAt ℝ 2 Φ (G x) and ContDiffAt ℝ 2 G x.

With $\sigma_k(x)=\sigma(x,k)$,

This local variant avoids global smoothness assumptions and can be reused whenever only the behavior at one state point is available.

Original Lean declaration header

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

theorem diffusionGenerator_comp_of_contDiffAt {d : ℕ} (b : V → V) (σ : V → Fin d → V)
    (Φ : W → ℝ) (G : V → W) (x : V) (hΦ : ContDiffAt ℝ 2 Φ (G x)) (hG : ContDiffAt ℝ 2 G x) :
    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_comp · Next: diffusionGenerator_mul.

Source excerpt, lines 243–248 · Frozen source 408915f.