Compactly Supported Smooth Plateau on the Two-Dimensional State Space
ProvedItoLemma.exists_smooth_fin_two_bump_plateaucompact-supportito-lemmastochastic-product-ruletwo-dimensional-bump
For any nonnegative radius, there is a smooth real-valued bump function on the two-dimensional product state space which is one throughout the closed ball of that radius and vanishes outside a slightly larger ball. It supports the direct truncation of the polynomial product test function before applying the vector Itô formula.
Preamble
import Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Formal statement
theorem ItoLemma.exists_smooth_fin_two_bump_plateau
(R : ℝ) (hR : 0 ≤ R) :
∃ ψ : (Fin 2 → ℝ) → ℝ,
ContDiff ℝ (↑(⊤ : ℕ∞)) ψ ∧ HasCompactSupport ψ ∧
(∀ z : Fin 2 → ℝ, ‖z‖ ≤ R → ψ z = 1) ∧
(∀ z : Fin 2 → ℝ, R + 2 ≤ ‖z‖ → ψ z = 0) := by sorrySource
Mathlib ContDiffBump construction in the finite-dimensional normed vector space Fin 2 → Real, with continuity and support properties documented on 26 October 2026 at https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Calculus/BumpFunction/Basic.html