Uniform Bounds on Truncated Product Derivatives through Order Two
ProvedItoLemma.fin_two_smooth_compact_iterated_derivatives_boundedbounded-derivativescompact-supportfderivito-lemma
For a C∞ compactly supported real function of two real coordinates, a single nonnegative constant bounds the norms of all iterated Fréchet derivatives of orders zero, one, and two. This is the bounded-derivative ingredient of the finite-dimensional Itô formula.
Preamble
import Mathlib.Analysis.Calculus.ContDiff.Basic
Formal statement
theorem ItoLemma.fin_two_smooth_compact_iterated_derivatives_bounded
(f : (Fin 2 → ℝ) → ℝ)
(hf : ContDiff ℝ (↑(⊤ : ℕ∞)) f)
(hs : HasCompactSupport f) :
∃ C : ℝ, 0 ≤ C ∧
∀ i : ℕ, i ≤ 2 → ∀ z : Fin 2 → ℝ, ‖iteratedFDeriv ℝ i f z‖ ≤ C := by sorrySource
Official Mathlib.Analysis.Calculus.ContDiff.Basic documentation, HasCompactSupport.exists_bound_iteratedFDeriv, read 26 October 2026: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Calculus/ContDiff/Basic.html. Pinned index omission noted; proof availability requires remote verification.
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.