Weak Convergence of Smoothed Laws on Bounded Continuous Tests

Proved

FunctionalInequalities.KLS.LogConcave.GaussianSmoothing.smoothedLaw_integral_bounded_tendsto_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This statement proves convergence of bounded continuous test-function integrals under Gaussian smoothing.

Let $E$ be a finite-dimensional real inner-product space with its Borel measurable structure. Let $μ$ be a probability measure on $E$ , let $ρ : E → ℝ$ satisfy IsBorellDensity μ volume ρ, and let $f : E → ℝ$ be a bounded continuous function, represented in Lean by a BoundedContinuousFunction. For the smoothed law smoothedLaw μ s, as $s\to\text{atTop}$ ,

\int_E f(y)\,d(\operatorname{smoothedLaw}(μ,s))(y) \longrightarrow \int_E f(y)\,dμ(y).

This is the bounded-continuous-function form of weak convergence for the Gaussian-smoothed laws.

Original Lean declaration header

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

theorem smoothedLaw_integral_bounded_tendsto {μ : Measure E} [IsProbabilityMeasure μ]
    {ρ : E → ℝ} (hρ : KLS.IsBorellDensity μ volume ρ) (f : BoundedContinuousFunction E ℝ) :
    Tendsto (fun s : ℝ => ∫ y, f y ∂(smoothedLaw μ s)) atTop (𝓝 (∫ y, f y ∂μ))

Module navigation

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

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

Supporting theorems: normalizedDensity_tendsto_L1.

Previous: normalizedDensity_tendsto_L1.

Source excerpt, lines 307–309 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_Density_GaussianSmoothing_Approximation

set_option autoImplicit false
open MeasureTheory Set Filter Topology Bornology
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]

Formal statement


theorem FunctionalInequalities.KLS.LogConcave.GaussianSmoothing.smoothedLaw_integral_bounded_tendsto_readable {μ : Measure E} [IsProbabilityMeasure μ]
    {ρ : E → ℝ} (hρ : KLS.IsBorellDensity μ volume ρ) (f : BoundedContinuousFunction E ℝ) :
    Tendsto (fun s : ℝ => ∫ y, f y ∂(smoothedLaw μ s)) atTop (𝓝 (∫ y, f y ∂μ)) := by sorry

Source

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

View graph