Theorem 3 — Transformation of the Gradient and Hessian

Proved

DinhSharpness.DerivativeTransformation

by Minghui · Sep 26, 2026 · Mathlib c5ea003 (Lean v4.30.0)

analysismachine-learningneural-networks

Let $L$ be continuous and satisfy the local twice Fréchet differentiability condition at $\theta$ . For every $\alpha>0$ , the same regularity holds at $T_\alpha\theta$ , and for all parameter directions $u,w$ ,

DL(T_\alpha\theta)[u]=DL(\theta)[T_{\alpha^{-1}}u],

H_L(T_\alpha\theta)[u,w] =H_L(\theta)[T_{\alpha^{-1}}u,T_{\alpha^{-1}}w].

No critical-point or minimum assumption is imposed here. Formalization note: direct source Theorem 3, expressing its row-gradient formula as equality of linear functionals and its Hessian congruence as equality on two arguments. Transport of local regularity records that these are actual derivatives.

Source: Laurent Dinh, Razvan Pascanu, Samy Bengio, Yoshua Bengio, Sharp Minima Can Generalize For Deep Nets, ICML 2017, arXiv:1703.04933v2, https://arxiv.org/abs/1703.04933v2; Section 4.2, PDF p. 5, Theorem 3 and its unnumbered first- and second-derivative identities; Section 2, PDF p. 2.

Notation and network conventions

Let $d,h\ge1$ be the input dimension and hidden width. The parameter $\theta=(W,v)$ consists of $W\in\mathbb R^{d\times h}$ and $v\in\mathbb R^h$ , with the Euclidean norm on all $n=dh+h$ entries. The scalar-output network is

f_\theta(x)=\sum_{j=1}^h \max\!\left(\sum_{i=1}^d x_i W_{ij},0\right)v_j, \qquad x\in\mathbb R^d.

There are no biases and no output activation. For any real-valued functional $\ell$ on prediction functions, $L(\theta)=\ell(f_\theta)$ . In particular, losses with additional parameter-dependent penalties are not included unless they also admit this representation. The positive rescaling is

T_\alpha(W,v)=(\alpha W,\alpha^{-1}v),\qquad \alpha>0.

Observational equivalence means equality of predictions on every input.

The local regularity condition means that $L$ is Fréchet differentiable at every point of some neighborhood of $\theta$ , and the map $z\mapsto DL(z)$ is Fréchet differentiable at $\theta$ . Write $H_L(\theta)=D(DL)(\theta)$ , a continuous bilinear form. Its norm is

\|H_L(\theta)\|=\sup_{\|u\|\le1,\,\|w\|\le1} |H_L(\theta)[u,w]|.

Under Euclidean/Riesz identification, this is the spectral operator norm of the Hessian matrix. A local minimum uses the usual Euclidean neighborhood; it need not be isolated or global. No probability model is assumed: the claim is deterministic and compares the same prediction function.

Formalization note: the network and scaling directly encode Section 3, Definition 3 (PDF p. 3), Theorem 1 and Definition 5 (PDF p. 4). The function-based continuous-loss convention is Section 2, PDF p. 2. For the Hessian targets, the local regularity condition makes the source's implicit second differentiability explicit without requiring global smoothness or continuity of second derivatives. The model defines actual Fréchet derivatives, not an arbitrary matrix constrained by desired conclusions. Relevant displayed formulas have no equation numbers.

Preamble

import Definitions.Def_DinhSharpness_Model

Formal statement

namespace DinhSharpness
theorem DerivativeTransformation :
  ∀ (d h : ℕ), 0 < d → 0 < h →
    ∀ (ℓ : (Input d → ℝ) → ℝ), Continuous (parameterLoss (h := h) ℓ) →
      ∀ (θ : Parameter d h), TwiceDifferentiableAt (parameterLoss ℓ) θ →
        ∀ (α : ℝ), 0 < α →
          TwiceDifferentiableAt (parameterLoss ℓ) (scale α θ) ∧
          (∀ u : Parameter d h,
            fderiv ℝ (parameterLoss ℓ) (scale α θ) u =
              fderiv ℝ (parameterLoss ℓ) θ (scale α⁻¹ u)) ∧
          (∀ u v : Parameter d h,
            hessian (parameterLoss ℓ) (scale α θ) u v =
              hessian (parameterLoss ℓ) θ (scale α⁻¹ u) (scale α⁻¹ v)) := by sorry
end DinhSharpness

Source

Laurent Dinh, Razvan Pascanu, Samy Bengio, Yoshua Bengio, Sharp Minima Can Generalize For Deep Nets, ICML 2017, arXiv:1703.04933v2, https://arxiv.org/abs/1703.04933v2; Section 4.2, PDF p. 5, Theorem 3 and its unnumbered first- and second-derivative identities; Section 2, PDF p. 2.

Read-back

What the Lean code literally says, in plain math · gpt-6

For every pair of natural numbers $d,h$ with $d>0$ and $h>0$ , identify the input space with Euclidean $\mathbb R^d$ and the parameter space with the Euclidean space $P=\mathbb R^{d\times h}\times\mathbb R^h$ , whose coordinates are indexed by the disjoint union $(\{0,\ldots,d-1\}\times\{0,\ldots,h-1\})\sqcup\{0,\ldots,h-1\}$ . For every functional $\ell:(\mathbb R^d\to\mathbb R)\to\mathbb R$ , define the scalar parameter function by $L(W,a)=\ell\bigl(x\mapsto\sum_{j=0}^{h-1}\max\{\sum_{i=0}^{d-1}x_iW_{ij},0\}\,a_j\bigr)$ , and suppose that $L$ is continuous on all of $P$ . Write $DL(z)$ for the real Fréchet derivative, viewed as a continuous linear map $P\to\mathbb R$ , and write $H_L(z)=D(DL)(z)$ for the real Fréchet derivative of the map $z\mapsto DL(z)$ , viewed as a continuous linear map from $P$ to the space of continuous linear maps $P\to\mathbb R$ ; these derivative operators take the zero map at points where the corresponding function is not differentiable. For every parameter $\theta=(W,a)\in P$ , suppose that there is a neighborhood of $\theta$ on which $L$ is differentiable at every point, and that the map $z\mapsto DL(z)$ is differentiable at $\theta$ . Then, for every real $\alpha>0$ , at the scaled parameter $T_\alpha\theta=(\alpha W,\alpha^{-1}a)$ there is likewise a neighborhood on which $L$ is differentiable at every point, and the map $z\mapsto DL(z)$ is differentiable at $T_\alpha\theta$ ; moreover, for every direction $u=(U,b)\in P$ and every pair of directions $u=(U,b),v=(V,c)\in P$ , respectively, $DL(T_\alpha\theta)[u]=DL(\theta)[(\alpha^{-1}U,\alpha b)]$ and $H_L(T_\alpha\theta)[u][v]=H_L(\theta)[(\alpha^{-1}U,\alpha b)][(\alpha^{-1}V,\alpha c)]$ . Thus the inverse scaling in each direction multiplies its matrix coordinates by $\alpha^{-1}$ and its final $h$ coordinates by $\alpha$ . The quantifiers exclude zero input dimension, zero hidden dimension, and zero or negative scaling factors, so no inverse of zero occurs in these conclusions; they include arbitrary zero coordinates, the zero parameter, and zero directions. No regularity assumption is imposed on $\ell$ itself beyond the stated continuity and differentiability conditions on its composite $L$ , and differentiability of $z\mapsto DL(z)$ is assumed at $\theta$ only, rather than throughout a neighborhood.

Human review

Endorsed by Shuze Chen · Sep 26, 2026
Confirmed by the moderator at approval.
Endorsed by Minghui · Sep 26, 2026
Confirmed by the mission captain (proposal self-audit).

View graph