Compact Support of the Scaled Cutoff
ProvedFunctionalInequalities.Analysis.BakryEmery.hasCompactSupport_cutoff_readablefunctional-inequalitieskls-conjecturekls-modularkls-readablelog-concave
This technical lemma establishes compact support for the scaled cutoff function.
Let be a finite-dimensional real inner-product space and let . For the function cutoff R, defined by scaling the fixed unit bump, one has
More specifically, the support is contained in the closed ball of radius . This fact is used to construct compactly supported approximations and cutoff test functions.
Original Lean declaration header
Within namespace FunctionalInequalities.Analysis.BakryEmery. Shown in its original module context. Proof omitted.
omit [CompleteSpace E] [MeasurableSpace E] [BorelSpace E] in
theorem hasCompactSupport_cutoff {R : ℝ} (hR : 0 < R) : HasCompactSupport (cutoff (E := E) R)
Module navigation
Module: Analysis/BakryEmery/Tilt/Temperate.
Next: cutoff_eq_one.
Source excerpt, lines 43–44 · 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] [MeasurableSpace E] [BorelSpace E]
Formal statement
theorem FunctionalInequalities.Analysis.BakryEmery.hasCompactSupport_cutoff_readable {R : ℝ} (hR : 0 < R) : HasCompactSupport (cutoff (E := E) R) := by sorry
Source
Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/BakryEmery/Tilt/Temperate.lean#L43-L75 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.BakryEmery.Tilt.Temperate`, declaration `FunctionalInequalities.Analysis.BakryEmery.hasCompactSupport_cutoff`; the repository is private at upload time).