First and Second Truncated-Product Derivatives Agree Inside the Plateau
ProvedItoLemma.fin_two_truncated_product_derivatives_eq_on_plateau_interiorderivative-congruenceito-lemmalocalisationproduct-rule
If a two-dimensional cutoff equals one throughout the closed radius-R ball, then at every point strictly inside that ball the first and second Fréchet derivatives of the cutoff coordinate product coincide with those of the ordinary coordinate product. Equality in a neighbourhood transfers to derivatives.
Preamble
import Mathlib.Analysis.Calculus.FDeriv.Congr
Formal statement
theorem ItoLemma.fin_two_truncated_product_derivatives_eq_on_plateau_interior
(R : ℝ) (ψ : (Fin 2 → ℝ) → ℝ)
(hp : ∀ y : Fin 2 → ℝ, ‖y‖ ≤ R → ψ y = 1)
(z : Fin 2 → ℝ) (hz : ‖z‖ < R) :
fderiv ℝ (fun y : Fin 2 → ℝ => ψ y * (y 0 * y 1)) z =
fderiv ℝ (fun y : Fin 2 → ℝ => y 0 * y 1) z ∧
fderiv ℝ (fderiv ℝ (fun y : Fin 2 → ℝ => ψ y * (y 0 * y 1))) z =
fderiv ℝ (fderiv ℝ (fun y : Fin 2 → ℝ => y 0 * y 1)) z := by sorrySource
Mathlib.Analysis.Calculus.FDeriv.Congr, Filter.EventuallyEq.fderiv_eq and Filter.EventuallyEq.fderiv, verified in pinned Mathlib index and official documentation on 26 October 2026: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Calculus/FDeriv/Congr.html
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.