Squared-Norm Moment Under Gaussian Smoothing

Proved

FunctionalInequalities.KLS.LogConcave.GaussianSmoothing.smoothedLaw_norm_sq_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This statement gives the exact change in the squared-norm moment under Gaussian smoothing.

Let $E$ be a finite-dimensional complete real inner-product space with its Borel measurable structure. Let $μ$ be a probability measure on $E$ with finite second moment, expressed as MemLp id 2 μ. Let $s>0$ . Then

\int_E \|y\|^2\,d(\operatorname{smoothedLaw}(μ,s))(y) = \int_E \|y\|^2\,dμ(y) +\frac{\operatorname{finrank}_{\mathbb R}E}{2s}.

The theorem records the dimension-dependent increase in the total second moment caused by the Gaussian noise.

Original Lean declaration header

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

theorem smoothedLaw_norm_sq (μ : Measure E) [IsProbabilityMeasure μ]
    (hμ2 : MemLp id 2 μ) {s : ℝ} (hs : 0 < s) :
    (∫ y : E, ‖y‖ ^ 2 ∂(smoothedLaw μ s)) =
      (∫ y : E, ‖y‖ ^ 2 ∂μ) + (Module.finrank ℝ E : ℝ) / (2 * s)

Module navigation

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

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

Supporting theorems: gaussianLaw_exp_norm_integrable, smoothedLaw_inner_sq.

Previous: smoothedLaw_inner_sq · Next: gaussianLaw_directional_identity_of_bounded_lipschitz_test.

Source excerpt, lines 332–335 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_Density_GaussianSmoothing_Moments

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

Formal statement


theorem FunctionalInequalities.KLS.LogConcave.GaussianSmoothing.smoothedLaw_norm_sq_readable (μ : Measure E) [IsProbabilityMeasure μ]
    (hμ2 : MemLp id 2 μ) {s : ℝ} (hs : 0 < s) :
    (∫ y : E, ‖y‖ ^ 2 ∂(smoothedLaw μ s)) =
      (∫ y : E, ‖y‖ ^ 2 ∂μ) + (Module.finrank ℝ E : ℝ) / (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#L331-L354 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.LogConcave.Density.GaussianSmoothing.Moments`, declaration `FunctionalInequalities.KLS.LogConcave.GaussianSmoothing.smoothedLaw_norm_sq`; the repository is private at upload time).

View graph