Unit bump and scaled cutoff for tempered-growth tests

Definition

KLSModular_FunctionalInequalities_Analysis_BakryEmery_Tilt_Temperate

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

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

For a finite-dimensional real inner-product space $E$ with its Borel measurable structure, unitBump is a smooth bump centered at $0$ that equals $1$ on the closed unit ball and vanishes outside the ball of radius $2$ . cutoff R x is the scaled function $\chi_R(x)=\varphi(R^{-1}x)$ , where R is real and $\varphi$ is unitBump; the bundle contains no integrated generator identity.

Original module imports

import FunctionalInequalities.Analysis.BakryEmery.Tilt.Basic
import FunctionalInequalities.Analysis.BakryEmery.Gamma
import Mathlib.Analysis.Distribution.TemperateGrowth
import Mathlib.Analysis.Calculus.BumpFunction.InnerProduct

Original declaration excerpt

Shown in the original module context.

def unitBump : ContDiffBump (0 : E) := ⟨1, 2, one_pos, one_lt_two⟩

Module navigation

Direct project imports: Analysis/BakryEmery/Tilt/Basic, Analysis/BakryEmery/Gamma.

Theorems in source order:

Project result: The KLS conjecture.

Original module · FunctionalInequalities.Analysis.BakryEmery.Tilt.Temperate · Frozen source 408915f.

Definition code

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_BakryEmery_Tilt_Basic
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_BakryEmery_Gamma
import Mathlib.Analysis.Distribution.TemperateGrowth
import Mathlib.Analysis.Calculus.BumpFunction.InnerProduct

noncomputable section
open MeasureTheory Filter Topology FunctionalInequalities.Analysis.Tensor
open scoped RealInnerProductSpace ContDiff
namespace FunctionalInequalities
namespace Analysis
namespace BakryEmery
universe u
variable {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
/-- The bump `φ` on `E`: one on the closed unit ball, zero outside the ball of radius `2`. -/
def unitBump : ContDiffBump (0 : E) := ⟨1, 2, one_pos, one_lt_two⟩
/-- The scaled cutoff `χ_R(x) = φ(x / R)`. -/
def cutoff (R : ℝ) (x : E) : ℝ := (unitBump : ContDiffBump (0 : E)) (R⁻¹ • x)
variable (m : Measure E) [m.IsAddHaarMeasure]
end BakryEmery
end Analysis
end FunctionalInequalities

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/BakryEmery/Tilt/Temperate.lean#L31-L35 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.BakryEmery.Tilt.Temperate`, definition bundle `KLSModular_FunctionalInequalities_Analysis_BakryEmery_Tilt_Temperate`; the repository is private at upload time).

View graph