Smoothness of the Localization Lyapunov Function

This auxiliary regularity theorem states that the localization Lyapunov function is infinitely differentiable.

Let $\mu$ be a probability measure on $\operatorname{EuclideanSpace}(\mathbb R,\operatorname{Fin}(n))$ with compact support, and assume that $\mu$ is isotropic. Then the function

on the localization parameter space is $C^\infty$.

The result supplies the smoothness required for generator calculations involving the Lyapunov function.

Formalization Note. Lean expresses infinite differentiability as ContDiff ℝ ∞; the function is the definition lyapunov μ hc.

Original Lean declaration header

Within namespace FunctionalInequalities.KLS.BKL.Localization. Shown in its original module context. Proof omitted.

theorem contDiff_lyapunov (hiso : KLS.Isotropic μ) : ContDiff ℝ ∞ (lyapunov μ hc)

Module navigation

Module: KLS/BKL/Localization/Lyapunov/Basic.

Definition modules: KLS/BKL/Localization/Coefficients, KLS/Isotropic.

Supporting theorems: Covariance.inner_operator_self_pos_of_affineSupport_eq_top, contDiff_posteriorCovariance_joint.

Next: generator_norm_sq_fst.

Source excerpt, lines 193–193 · Frozen source 408915f.