Operator Covariance Convergence Under Tilting

This formalizes covariance convergence for the small quadratic tilts used in the regular approximation, associated in the literature register with Section 2, equation (12), of Bizeul–Klartag–Lehec (arXiv:2610.05474v1).

Let $E$ be a complete finite-dimensional real inner-product space with Borel measurable structure, let $\mu$ be a probability measure, and assume the identity map has finite second moment: MemLp id 2 μ. Let $\mu_\delta=\mu.\operatorname{tilted}(x\mapsto-\delta\|x\|^2/2)$.

Then, as $\delta\to0^+$,

in the topology of continuous linear operators, hence in operator norm. This is a convergence statement only; it does not assert log-concavity or invertibility of either covariance operator.

Original Lean declaration header

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

theorem covariance_quadraticTilt_tendsto (μ : ProbabilityMeasure E)
    (hμ2 : MemLp (id : E → E) 2 (μ : Measure E)) :
    Tendsto (fun δ : ℝ => Covariance.operator
      ((μ : Measure E).tilted (fun x => -(δ / 2) * ‖x‖ ^ 2)))
      (𝓝[>] (0 : ℝ)) (𝓝 (Covariance.operator (μ : Measure E)))

Module navigation

Module: Probability/QuadraticTilt.

Definition modules: Probability/Covariance/Basic.

Supporting theorems: inner_covariance_quadraticTilt_tendsto.

Previous: inner_covariance_quadraticTilt_tendsto.

Source excerpt, lines 217–221 · Frozen source 408915f.