Uniform bounds for every finite derivative jet of expanding smooth cutoffs

Proved

HunterPDE.Sobolev.uniform_cutoff_jet_bound

by Mazecto · Oct 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

approximationsobolev-spacesweak-derivatives

Let $\chi\in C_c^\infty(\mathbb R^n)$ and $k\ge0$ . There is a finite constant $C\ge0$ such that, for every integer $j\ge0$ , every multi-index $|\beta|\le k$ , and every $x$ ,

\left|D^\beta\left[1-\chi\left(\frac{\cdot}{j+1}\right)\right](x)\right|\le C.

No equality to one near zero is required. The derivative scaling formula supplies the factor $(j+1)^{-|\beta|}\le1$ for positive orders. Compact support and smoothness bound each derivative of $\chi$ , and there are only finitely many orders. At order zero, use $1+\sup|\chi|$ . This is useful in uniform Sobolev multiplier estimates and includes dimension zero. It is an independent open calculus obligation.

Preamble

import Definitions.Def_HunterPDE_Sobolev_SobolevSpace

open HunterPDE.Sobolev

Formal statement

theorem HunterPDE.Sobolev.uniform_cutoff_jet_bound {n : ℕ} (k : ℕ)
    (χ : EuclideanSpace ℝ (Fin n) → ℝ) (hχ : IsTestFunction Set.univ χ) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ (j : ℕ) (β : Fin n → ℕ), ∑ i, β i ≤ k →
      ∀ x, ‖iteratedPartial β (fun y => 1 - χ (((j : ℝ) + 1)⁻¹ • y)) x‖ ≤ C := by sorry

Source

John K. Hunter, Notes on Partial Differential Equations (revised 6/18/2014), https://www.math.ucdavis.edu/~hunter/pdes/pde_notes.pdf, Section 1.8 (multi-index derivatives), printed p. 10, and the scaled cutoff in the proof of Theorem 3.24, printed p. 59. This uniform jet bound is an elementary consequence of derivative scaling and compact support, used in the cutoff proof; not a verbatim numbered theorem.

View graph