Prove2Me

Constant Mixed Hessian of the Two-Coordinate Product

Proved
ItoLemma.fin_two_product_gradient_hasFDerivAt

by WillR · Oct 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

frechet-derivativehessianito-lemmaproduct-rule

The Fréchet derivative of the gradient map of f(x)=x₀x₁ is the constant continuous linear operator H(v)=v₀·proj₁+v₁·proj₀. This operator is the symmetric mixed Hessian, with zero diagonal entries and unit off-diagonal entries.

Preamble
import Mathlib.Analysis.Calculus.FDeriv.Linear
import Mathlib.Analysis.Calculus.FDeriv.Prod
import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Formal statement
theorem ItoLemma.fin_two_product_gradient_hasFDerivAt (z : Fin 2 → ℝ) :
    HasFDerivAt
      (fun x : Fin 2 → ℝ =>
        x 0 • (ContinuousLinearMap.proj (1 : Fin 2) : (Fin 2 → ℝ) →L[ℝ] ℝ) +
        x 1 • (ContinuousLinearMap.proj (0 : Fin 2) : (Fin 2 → ℝ) →L[ℝ] ℝ))
      (((ContinuousLinearMap.proj (0 : Fin 2) :
            (Fin 2 → ℝ) →L[ℝ] ℝ).smulRight
          (ContinuousLinearMap.proj (1 : Fin 2) : (Fin 2 → ℝ) →L[ℝ] ℝ)) +
        ((ContinuousLinearMap.proj (1 : Fin 2) :
            (Fin 2 → ℝ) →L[ℝ] ℝ).smulRight
          (ContinuousLinearMap.proj (0 : Fin 2) : (Fin 2 → ℝ) →L[ℝ] ℝ))) z := by sorry
Source
Pinned Mathlib 0df444a360eaa60ab8c11dca51a86af692955474, ContinuousLinearMap.smulRight and ContinuousLinearMap.hasFDerivAt source headers verified 26 October 2026; official documentation https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Calculus/FDeriv/Linear.html.
Human review

  • Endorsed by Shuze Chen · Oct 27, 2026

    Confirmed by the moderator at approval.

  • Endorsed by WillR · Oct 27, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph