Prove2Me

Cutoff Equals One Inside Its Radius

Proved
FunctionalInequalities.Analysis.BakryEmery.cutoff_eq_one_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This is a basic property of the scaled smooth cutoff.

Let EE be a real inner-product space, let R>0R>0, and let x∈Ex\in E satisfy ∥x∥≤R\|x\|\leq R. Then

cutoff⁡R(x)=1.\operatorname{cutoff}_R(x)=1.

The function cutoff R is the unit bump evaluated at R−1xR^{-1}x. No completeness, finite-dimensionality, or measurable-space assumptions are required. This fact is used when removing compact-support restrictions by cutoff approximation.

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis.BakryEmery. Shown in its original module context. Proof omitted.

omit [CompleteSpace E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] in
theorem cutoff_eq_one {R : ℝ} (hR : 0 < R) {x : E} (hx : ‖x‖ ≤ R) : cutoff R x = 1

Module navigation

Module: Analysis/BakryEmery/Tilt/Temperate.

Previous: hasCompactSupport_cutoff · Next: norm_iteratedFDeriv_cutoff_le.

Source excerpt, lines 77–78 · Frozen source 408915f.

Preamble
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_BakryEmery_Tilt_Temperate

universe u
variable {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
omit [CompleteSpace E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
Formal statement
theorem FunctionalInequalities.Analysis.BakryEmery.cutoff_eq_one_readable {R : ℝ} (hR : 0 < R) {x : E} (hx : ‖x‖ ≤ R) : cutoff R x = 1 := by sorry
Source
Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/BakryEmery/Tilt/Temperate.lean#L77-L93 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.BakryEmery.Tilt.Temperate`, declaration `FunctionalInequalities.Analysis.BakryEmery.cutoff_eq_one`; the repository is private at upload time).

View graph