Smoothed Covariance Bilinear Form

Proved

FunctionalInequalities.KLS.LogConcave.GaussianSmoothing.smoothedLaw_covarianceBilin_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This is the covariance-bilinear-form identity for Gaussian smoothing.

Let $E$ be a complete finite-dimensional real inner-product space with Borel measurable structure. Let $\mu$ be a probability measure with finite second moment, let $s>0$ , and let $v,w\in E$ . For the smoothed law smoothedLaw μ s,

\operatorname{CovBilin}_{\mu*\gamma_s}(v,w) =\operatorname{CovBilin}_{\mu}(v,w)+\frac{\langle v,w\rangle}{2s}.

Equivalently, Gaussian smoothing adds $(2s)^{-1}$ times the ambient inner product to the covariance bilinear form. The declaration does not reformulate this as an operator equality, although it determines the corresponding quadratic covariance operator.

Original Lean declaration header

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

theorem smoothedLaw_covarianceBilin (μ : Measure E) [IsProbabilityMeasure μ]
    (hμ2 : MemLp id 2 μ) {s : ℝ} (hs : 0 < s) (v w : E) :
    covarianceBilin (smoothedLaw μ s) v w = covarianceBilin μ v w + ⟪v, w⟫ / (2 * s)

Module navigation

Module: KLS/LogConcave/Density/GaussianSmoothing/Moments.

Definition modules: KLS/LogConcave/Density/GaussianSmoothing/Basic.

Supporting theorems: gaussianLaw_exp_norm_integrable, smoothedLaw_variance.

Previous: smoothedLaw_variance · Next: smoothedLaw_inner_sq.

Source excerpt, lines 275–277 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_Density_GaussianSmoothing_Moments

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

Formal statement


theorem FunctionalInequalities.KLS.LogConcave.GaussianSmoothing.smoothedLaw_covarianceBilin_readable (μ : Measure E) [IsProbabilityMeasure μ]
    (hμ2 : MemLp id 2 μ) {s : ℝ} (hs : 0 < s) (v w : E) :
    covarianceBilin (smoothedLaw μ s) v w = covarianceBilin μ v w + ⟪v, w⟫ / (2 * s) := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/LogConcave/Density/GaussianSmoothing/Moments.lean#L274-L291 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.LogConcave.Density.GaussianSmoothing.Moments`, declaration `FunctionalInequalities.KLS.LogConcave.GaussianSmoothing.smoothedLaw_covarianceBilin`; the repository is private at upload time).

View graph