L¹ Convergence of Normalized Gaussian Smoothing
ProvedFunctionalInequalities.KLS.LogConcave.GaussianSmoothing.normalizedDensity_tendsto_L1_readableThis statement proves convergence in of normalized Gaussian smoothing to its source density.
Let be a finite-dimensional real inner-product space with its Borel measurable structure. Let be a probability measure on , and let satisfy IsBorellDensity ν volume ρ. For each real parameter , let normalizedDensity ρ s denote the normalized Gaussian-smoothed density. As tends to infinity through the real numbers,
The result supplies total-variation-type approximation at the density level and can be reused to compare integrals of bounded observables.
Original Lean declaration header
Within namespace FunctionalInequalities.KLS.LogConcave.GaussianSmoothing. Shown in its original module context. Proof omitted.
theorem normalizedDensity_tendsto_L1 {ν : Measure V}
[IsProbabilityMeasure ν] {ρ : V → ℝ}
(hρ : IsBorellDensity ν volume ρ) :
Tendsto (fun s : ℝ => ∫ x : V, |normalizedDensity ρ s x - ρ x|)
atTop (𝓝 0)
Module navigation
Module: KLS/LogConcave/Density/GaussianSmoothing/Approximation.
Definition modules: KLS/LogConcave/Density/GaussianSmoothing/Basic, KLS/LogConcave/Density/BorellRepresentation/Basic.
Supporting theorems: ae_continuous.
Next: smoothedLaw_integral_bounded_tendsto.
Source excerpt, lines 187–191 · Frozen source 408915f.
import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_Density_GaussianSmoothing_Approximation
set_option autoImplicit false
open MeasureTheory Set Filter Topology Bornology
variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V]
[FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V]
theorem FunctionalInequalities.KLS.LogConcave.GaussianSmoothing.normalizedDensity_tendsto_L1_readable {ν : Measure V}
[IsProbabilityMeasure ν] {ρ : V → ℝ}
(hρ : IsBorellDensity ν volume ρ) :
Tendsto (fun s : ℝ => ∫ x : V, |normalizedDensity ρ s x - ρ x|)
atTop (𝓝 0) := by sorry