Prove2Me

Pointwise Covariance Convergence Under Tilting

Proved
FunctionalInequalities.Probability.inner_covariance_quadraticTilt_tendsto_readable

by Lazyfill · Oct 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This is the scalar covariance convergence statement for small quadratic tilts.

Let EE be a complete finite-dimensional real inner-product space with Borel measurable structure, let μ\mu be a probability measure with finite second moment, expressed as MemLp id 2 μ, and let u,v∈Eu,v\in E. For the tilted probability measure with weight e−δ∥x∥2/2e^{-\delta\|x\|^2/2},

⟨Cov⁡(μδ)u,v⟩⟶⟨Cov⁡(μ)u,v⟩(δ→0+).\left\langle \operatorname{Cov}(\mu_\delta)u,v\right\rangle \longrightarrow \left\langle \operatorname{Cov}(\mu)u,v\right\rangle \qquad(\delta\to0^+).

The convergence is in R\mathbb R along the one-sided neighborhood of zero. This scalar form is the ingredient used to establish operator-norm covariance convergence.

Original Lean declaration header

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

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

Module navigation

Module: Probability/QuadraticTilt.

Definition modules: Probability/Covariance/Basic.

Supporting theorems: integral_quadraticTilt_tendsto.

Previous: integral_quadraticTilt_tendsto · Next: covariance_quadraticTilt_tendsto.

Source excerpt, lines 188–192 · Frozen source 408915f.

Preamble
import Definitions.Def_KLSModular_FunctionalInequalities_Probability_QuadraticTilt

open MeasureTheory Filter Topology Set
open scoped RealInnerProductSpace
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
Formal statement

theorem FunctionalInequalities.Probability.inner_covariance_quadraticTilt_tendsto_readable (μ : ProbabilityMeasure E)
    (hμ2 : MemLp (id : E → E) 2 (μ : Measure E)) (u v : E) :
    Tendsto (fun δ : ℝ => ⟪Covariance.operator
      ((μ : Measure E).tilted (fun x => -(δ / 2) * ‖x‖ ^ 2)) u, v⟫)
      (𝓝[>] (0 : ℝ)) (𝓝 ⟪Covariance.operator (μ : Measure E) u, v⟫) := by sorry
Source
Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Probability/QuadraticTilt.lean#L187-L214 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Probability.QuadraticTilt`, declaration `FunctionalInequalities.Probability.inner_covariance_quadraticTilt_tendsto`; the repository is private at upload time).

View graph