Uniform multi-derivative bound for shrinking normal cutoffs
ProvedHunterPDE.Shared.uniform_normalCutoff_multiDeriv_boundFix a coordinate and a multi-index . Let be a smooth compactly supported real function on Euclidean space, with every pure normal derivative of order less than vanishing on the coordinate hyperplane. Let be any smooth real cutoff equal to zero on and one on . There is a nonnegative constant , independent of the real scale and of , such that
No bound on the cutoff in the transition interval is assumed: smoothness supplies all required bounds on that compact interval. The assertion includes zero normal order, when the boundary hypothesis is empty.
The intended proof expands by Leibniz, preserves vanishing normal jets under tangential differentiation, and uses one-dimensional Taylor bounds to cancel the scale factors on the shrinking transition strip. This quantitative calculus estimate is an Open proof obligation, separate from support geometry and convergence of an approximating sequence.
import Definitions.Def_HunterPDE_Shared_WeakDeriv open HunterPDE.Shared open scoped ContDiff set_option autoImplicit false
theorem HunterPDE.Shared.uniform_normalCutoff_multiDeriv_bound
{n : ℕ} (i : Fin n) (α : Fin n → ℕ)
(ψ : EuclideanSpace ℝ (Fin n) → ℝ)
(hψ : ContDiff ℝ ∞ ψ) (hc : HasCompactSupport ψ)
(hb : ∀ r : ℕ, r < α i → ∀ x : EuclideanSpace ℝ (Fin n), x i = 0 →
iteratedPartial ψ (List.replicate r i) x = 0)
(q : ℝ → ℝ) (hq : ContDiff ℝ ∞ q)
(hlo : ∀ s : ℝ, s ≤ 1 → q s = 0)
(hhi : ∀ s : ℝ, 2 ≤ s → q s = 1) :
∃ C : ℝ, 0 ≤ C ∧ ∀ a : ℝ, 1 ≤ a →
∀ x : EuclideanSpace ℝ (Fin n),
‖multiDeriv (fun y => q (a * y i) * ψ y) α x‖ ≤ C := by sorry