Local Lipschitzness of Localization Noise Columns

This statement establishes local Lipschitzness of each noise column in the finite-dimensional localization system.

Let $n\in\mathbb N$, let $\mu$ be a probability measure on $\mathbb R^n$ represented as EuclideanSpace ℝ (Fin n), and assume that its support is compact and that $\mu$ is isotropic. Let $k\in\operatorname{Fin}(n)$. For a localization parameter $p=(c,Q)$, let noise μ hc p k denote the $k$th noise column, whose first component is the inverse square root of the posterior covariance applied to the $k$th standard basis vector.

Then

is locally Lipschitz. The conclusion is asserted separately for every coordinate $k$ and does not provide a common global Lipschitz constant.

Original Lean declaration header

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

theorem locallyLipschitz_noise (hiso : KLS.Isotropic μ) (k : Fin n) :
    LocallyLipschitz (fun p : Param n => noise μ hc p k)

Module navigation

Module: KLS/BKL/Localization/Coefficients.

Definition modules: KLS/Isotropic.

Supporting theorems: Covariance.inner_operator_self_pos_of_affineSupport_eq_top, Isotropic.locallyLipschitz_inverseSqrt_covariance_joint, contDiff_posteriorCovariance_joint, contDiff_posteriorMean_joint.

Next: cutoffCoefficients_admissible.

Source excerpt, lines 89–90 · Frozen source 408915f.