Compactly Supported Smooth Functions Are Admissible

Proved

FunctionalInequalities.Poincare.SmoothTest.Admissible.of_contDiff_hasCompactSupport_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This auxiliary statement supplies admissible smooth Poincaré tests for every finite measure.

Let $E$ be a finite-dimensional complete real inner product space with its Borel measurable structure, let $\mu$ be a finite measure on $E$ , and let $f:E\to\mathbb R$ be $C^\infty$ with compact support.

Then $f$ is admissible (Poincare.SmoothTest.Admissible):

f\in C^\infty(E),\qquad f\in L^2(\mu),\qquad \bigl(x\mapsto\|\nabla f(x)\|^2\bigr)\in L^1(\mu).

This provides tests usable in the smooth-test Poincaré inequality without a probability or density assumption on the measure.

Original Lean declaration header

Within namespace FunctionalInequalities.Poincare.SmoothTest. Shown in its original module context. Proof omitted.

theorem Admissible.of_contDiff_hasCompactSupport {μ : Measure E} [IsFiniteMeasure μ]
    {f : E → ℝ} (hf : ContDiff ℝ ∞ f) (hc : HasCompactSupport f) : Admissible μ f

Module navigation

Module: Poincare/SmoothTest/WeakLimit.

Definition modules: Poincare/SmoothTest/Basic.

Previous: variance_le_mul_energy_of_tendsto · Next: tendsto_integral_scaled_mul.

Source excerpt, lines 159–160 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Poincare_SmoothTest_WeakLimit

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

Formal statement


theorem FunctionalInequalities.Poincare.SmoothTest.Admissible.of_contDiff_hasCompactSupport_readable {μ : Measure E} [IsFiniteMeasure μ]
    {f : E → ℝ} (hf : ContDiff ℝ ∞ f) (hc : HasCompactSupport f) : Admissible μ f := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Poincare/SmoothTest/WeakLimit.lean#L158-L186 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Poincare.SmoothTest.WeakLimit`, declaration `FunctionalInequalities.Poincare.SmoothTest.Admissible.of_contDiff_hasCompactSupport`; the repository is private at upload time).

View graph