Convergence of Small Quadratic Tilts

This formalizes the normalized small-quadratic-tilt convergence described in the source module for the regular approximation of Bizeul–Klartag–Lehec (arXiv:2610.05474v1, Section 2, p. 5).

Let $E$ be a Borel real normed space, let $F$ be a complete real normed space, let $\mu$ be a probability measure on $E$, let $f:E\to F$ be integrable with respect to $\mu$, and for $\delta\in\mathbb R$ define the tilted measure by the weight $e^{-\delta\|x\|^2/2}$. As $\delta\to0^+$,

The limit is in the norm topology of $F$ and is taken through positive $\delta$. Only probability and integrability are assumed; no moment or log-concavity hypothesis is added.

Original Lean declaration header

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

theorem integral_quadraticTilt_tendsto {E F : Type*} [NormedAddCommGroup E]
    [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E]
    [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F]
    (μ : Measure E) [IsProbabilityMeasure μ] (f : E → F) (hf : Integrable f μ) :
    Tendsto
      (fun δ : ℝ => ∫ x, f x ∂(μ.tilted (fun x => -(δ / 2) * ‖x‖ ^ 2)))
      (𝓝[>] (0 : ℝ)) (𝓝 (∫ x, f x ∂μ))

Module navigation

Module: Probability/QuadraticTilt.

Next: inner_covariance_quadraticTilt_tendsto.

Source excerpt, lines 28–34 · Frozen source 408915f.