Vector Generator Commutation with Continuous Linear Maps

This is a compatibility identity for the vector-valued diffusion generator under a continuous linear map.

Let $V$, $W$, and $W'$ be real normed additive groups and normed spaces, let $d$ be a natural number, let $b:V\to V$ and $\sigma:V\to\operatorname{Fin}(d)\to V$, and let $\ell:W\to W'$ be a continuous linear map. For $G:V\to W$ and $x\in V$, assume that $G$ is twice continuously differentiable at $x$.

Then, writing vectorGenerator for the generator,

The result allows generator calculations for vector-valued functions to be transported through continuous linear maps, including trace and coordinate maps.

Original Lean declaration header

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

theorem vectorGenerator_clm_comp (b : V → V) (σ : V → Fin d → V)
    (ℓ : W →L[ℝ] W') {G : V → W} {x : V} (hG : ContDiffAt ℝ 2 G x) :
    vectorGenerator b σ (fun y => ℓ (G y)) x = ℓ (vectorGenerator b σ G x)

Module navigation

Module: Probability/Diffusion/VectorGenerator.

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