Gaussian–quadratic regularization sequences

Definition

KLSModular_FunctionalInequalities_KLS_LogConcave_Density_GaussianSmoothing_RegularApproximation

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

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

tiltRate k is the positive rate $\delta_k=1/(k+1)$ , gaussianSeq μ n is the Gaussian smoothing of $\mu$ with inverse-variance parameter $n+1$ , and rowLaw μ n k applies the quadratic tilt of rate $\delta_k$ . Given a Borell density, regularSeq packages the probability law associated with the regular potential obtained from the same smoothing and tilt parameters. statistics records the mean, raw second moment, and covariance operator of a probability law.

Original module imports

import FunctionalInequalities.KLS.LogConcave.Density.GaussianSmoothing.Moments
import FunctionalInequalities.KLS.LogConcave.Density.GaussianSmoothing.Approximation
import FunctionalInequalities.KLS.LogConcave.Density.GaussianSmoothing.Regular
import FunctionalInequalities.Probability.QuadraticTilt
import FunctionalInequalities.Analysis.DiagonalSelector
import Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Original declaration excerpt

Shown in the original module context.

def tiltRate (k : ℕ) : ℝ := 1 / ((k : ℝ) + 1)

Module navigation

Direct project imports: KLS/LogConcave/Density/GaussianSmoothing/Moments, KLS/LogConcave/Density/GaussianSmoothing/Approximation, KLS/LogConcave/Density/GaussianSmoothing/Regular, Probability/QuadraticTilt, Analysis/DiagonalSelector.

Theorems in source order:

row_joint_tendsto

Project result: The KLS conjecture.

Original module · FunctionalInequalities.KLS.LogConcave.Density.GaussianSmoothing.RegularApproximation · Frozen source 408915f.

Definition code

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_Density_GaussianSmoothing_Moments
import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_Density_GaussianSmoothing_Approximation
import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_Density_GaussianSmoothing_Regular
import Definitions.Def_KLSModular_FunctionalInequalities_Probability_QuadraticTilt
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_DiagonalSelector
import Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

open MeasureTheory Filter Topology
open FunctionalInequalities.Analysis
noncomputable section
namespace FunctionalInequalities
namespace KLS
namespace LogConcave
namespace GaussianSmoothing
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [CompleteSpace E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
/-- The quadratic-tilt rates `δ_k = 1/(k+1)`. -/
def tiltRate (k : ℕ) : ℝ := 1 / ((k : ℝ) + 1)
theorem tiltRate_pos (k : ℕ) : 0 < tiltRate k := by unfold tiltRate; positivity
/-- The Gaussian smoothings `μ * γ_{n+1}` as probability laws. -/
def gaussianSeq (μ : ProbabilityMeasure E) (n : ℕ) : ProbabilityMeasure E :=
  smoothedProbabilityLaw μ ((n : ℝ) + 1) (by positivity)
/-- Mean, raw second moment and covariance operator of a law. -/
def statistics (ν : ProbabilityMeasure E) : E × (ℝ × (E →L[ℝ] E)) :=
  (∫ y, y ∂(ν : Measure E), ∫ y, ‖y‖ ^ 2 ∂(ν : Measure E), Covariance.operator (ν : Measure E))
/-- The two-step laws: Gaussian smoothing `n`, then quadratic tilt with tiltRate `δ_k`. -/
def rowLaw (μ : ProbabilityMeasure E) (n k : ℕ) : ProbabilityMeasure E :=
  Probability.quadraticTiltLaw (gaussianSeq μ n) (tiltRate k) (tiltRate_pos k).le
/-- The law of the produced regular potential at smoothing `n+1` and tilt tiltRate `δ_k`. -/
def regularSeq {μ : ProbabilityMeasure E} {ρ : E → ℝ}
    (hρ : KLS.IsBorellDensity (μ : Measure E) volume ρ) (n k : ℕ) : ProbabilityMeasure E :=
  (regularPotential_quadraticPotential hρ
    (by positivity : (0 : ℝ) < (n : ℝ) + 1) (tiltRate_pos k)).law
end GaussianSmoothing
end LogConcave
end KLS
end FunctionalInequalities
end

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/LogConcave/Density/GaussianSmoothing/RegularApproximation.lean#L31-L163 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.LogConcave.Density.GaussianSmoothing.RegularApproximation`, definition bundle `KLSModular_FunctionalInequalities_KLS_LogConcave_Density_GaussianSmoothing_RegularApproximation`; the repository is private at upload time).

View graph