Local Lipschitzness of the Posterior Inverse Square Root

This statement gives a local regularity property of the diffusion coefficient used in the localization construction.

Let $E$ be a finite-dimensional real inner-product space and let $\mu$ be a probability measure with compact support. Assume that $\mu$ is isotropic, expressed by KLS.Isotropic μ. For each $(c,Q)\in E\times(E\to_L E)$, let $\mu_{c,Q}$ be the compact posterior and let $A(c,Q)=\operatorname{Covariance.operator}(\mu_{c,Q})$.

Then the map

represented by inverseSqrt, is locally Lipschitz on the whole parameter space in the operator norm:

The isotropy and compact-support assumptions are exactly those in the type; the statement does not assert a global Lipschitz constant.

Original Lean declaration header

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

theorem Isotropic.locallyLipschitz_inverseSqrt_covariance_joint (μ : ProbabilityMeasure E)
    (hc : IsCompact (μ : Measure E).support) (hiso : KLS.Isotropic μ) :
    LocallyLipschitz (fun p : E × (E →L[ℝ] E) =>
      inverseSqrt (Covariance.operator (compactPosterior μ hc p.1 p.2 : Measure E)))

Module navigation

Module: KLS/BKL/Posterior/Regularity.

Definition modules: Probability/Covariance/Basic, KLS/Isotropic, Analysis/Operator/InverseSqrt, Probability/Posterior/CompactDomain.

Supporting theorems: inner_self_pos_of_comp_eq_id, locallyLipschitz_inverseSqrt_of_contDiff_ringInverse, Covariance.inner_operator_self_pos_of_affineSupport_eq_top, contDiff_posteriorCovariance_joint.

Source excerpt, lines 60–63 · Frozen source 408915f.