Compact Support Makes Continuous Hessians Uniformly Continuous
ProvedItoLemma.fin_two_compact_support_second_fderiv_uniformContinuouscompact-supporthessianito-lemmauniform-continuity
On the two-coordinate real state space, the Hessian of a compactly supported function has compact support. If that Hessian is continuous, then it is uniformly continuous, providing a hypothesis of the accepted finite-dimensional Itô formula.
Preamble
import Mathlib.Analysis.Calculus.FDeriv.Const import Mathlib.Topology.UniformSpace.HeineCantor
Formal statement
theorem ItoLemma.fin_two_compact_support_second_fderiv_uniformContinuous
(f : (Fin 2 → ℝ) → ℝ)
(hs : HasCompactSupport f)
(h₂ : Continuous (fderiv ℝ (fderiv ℝ f))) :
UniformContinuous (fderiv ℝ (fderiv ℝ f)) := by sorrySource
Pinned-index lemma HasCompactSupport.uniformContinuous_of_continuous in Mathlib.Topology.UniformSpace.HeineCantor and HasCompactSupport.fderiv in Mathlib.Analysis.Calculus.FDeriv.Const, checked 26 October 2026. Official docs: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/UniformSpace/HeineCantor.html