Prove2Me

Uniform Derivative Bounds for Cutoffs

Proved
FunctionalInequalities.Analysis.BakryEmery.norm_iteratedFDeriv_cutoff_le_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This technical lemma gives uniform bounds for every fixed derivative order of the scaled cutoff.

Let EE be a finite-dimensional real inner-product space and let n∈Nn\in\mathbb N. There exists C∈RC\in\mathbb R such that for every R≥1R\ge1 and every x∈Ex\in E,

∥Dncutoff⁡(R)(x)∥≤C.\left\|D^n\operatorname{cutoff}(R)(x)\right\|\le C.

The constant depends on nn and EE but is independent of R≥1R\ge1 and xx. This estimate supports cutoff approximation arguments for functions of polynomial growth.

Original Lean declaration header

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

theorem norm_iteratedFDeriv_cutoff_le (n : ℕ) :
    ∃ C : ℝ, ∀ R : ℝ, 1 ≤ R → ∀ x : E, ‖iteratedFDeriv ℝ n (cutoff R) x‖ ≤ C

Module navigation

Module: Analysis/BakryEmery/Tilt/Temperate.

Previous: cutoff_eq_one · Next: abs_laplacian_le.

Source excerpt, lines 108–109 · 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.norm_iteratedFDeriv_cutoff_le_readable (n : ℕ) :
    ∃ C : ℝ, ∀ R : ℝ, 1 ≤ R → ∀ x : E, ‖iteratedFDeriv ℝ n (cutoff R) x‖ ≤ C := by sorry
Source
Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/BakryEmery/Tilt/Temperate.lean#L106-L166 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.BakryEmery.Tilt.Temperate`, declaration `FunctionalInequalities.Analysis.BakryEmery.norm_iteratedFDeriv_cutoff_le`; the repository is private at upload time).

View graph