Theorem 4 — Arbitrarily Sharp Observationally Equivalent Minima

Proved

DinhSharpness.ArbitrarilySharpEquivalentMinima

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

analysismachine-learningneural-networks

Let the parameter loss $L$ be continuous. Suppose $\theta$ is a local minimum, $DL(\theta)=0$ , the local twice Fréchet differentiability condition holds, and $H_L(\theta)\ne0$ . Then

\forall M>0\ \exists\alpha>0:\quad M\le\|H_L(T_\alpha\theta)\|.

For that same $\alpha$ , predictions on every input and the loss value are unchanged; $T_\alpha\theta$ is again a critical local minimum satisfying the same local regularity. No condition $W\ne0$ or $v\ne0$ is added.

Formalization note: direct source Theorem 4, including its accompanying observational-equivalence interpretation and explicitly stating the regularity implicit in the Hessian notation. This is the full arbitrary-dimensional, one-hidden-layer result, not a prescribed scalar example or an assumed Hessian-transformation rule. It asserts a parameterization dependence of sharpness; it is not a statistical generalization bound.

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 4 (Sharpest direction); proof and interpretation continue on PDF p. 6; Section 2, PDF p. 2. Displays are unnumbered.

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 ArbitrarilySharpEquivalentMinima :
  ∀ (d h : ℕ), 0 < d → 0 < h →
    ∀ (ℓ : (Input d → ℝ) → ℝ), Continuous (parameterLoss (h := h) ℓ) →
      ∀ (θ : Parameter d h), TwiceDifferentiableAt (parameterLoss ℓ) θ →
        IsLocalMin (parameterLoss ℓ) θ → fderiv ℝ (parameterLoss ℓ) θ = 0 →
          hessian (parameterLoss ℓ) θ ≠ 0 →
            ∀ M : ℝ, 0 < M → ∃ α : ℝ, 0 < α ∧
              prediction (scale α θ) = prediction θ ∧
              parameterLoss ℓ (scale α θ) = parameterLoss ℓ θ ∧
              IsLocalMin (parameterLoss ℓ) (scale α θ) ∧
              TwiceDifferentiableAt (parameterLoss ℓ) (scale α θ) ∧
              fderiv ℝ (parameterLoss ℓ) (scale α θ) = 0 ∧
              M ≤ ‖hessian (parameterLoss ℓ) (scale α θ)‖ := 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 4 (Sharpest direction); proof and interpretation continue on PDF p. 6; Section 2, PDF p. 2. Displays are unnumbered.

Read-back

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

For every pair of positive natural numbers $d,h$ , identify the input space with $\mathbb R^d$ and the parameter space with $\mathbb R^{d\times h}\times\mathbb R^h$ , with Euclidean norm $\|(W,v)\|=(\sum_{i=1}^d\sum_{j=1}^h W_{ij}^2+\sum_{j=1}^h v_j^2)^{1/2}$ . For every functional $\ell:(\mathbb R^d\to\mathbb R)\to\mathbb R$ , define $f_{W,v}(x)=\sum_{j=1}^h\max\{\sum_{i=1}^d x_iW_{ij},0\}\,v_j$ for every $x\in\mathbb R^d$ , and define $L(W,v)=\ell(f_{W,v})$ . Write $DL(z)$ for the real Fréchet derivative, with value the zero linear map at points where $L$ is not differentiable. Assume $L$ is continuous on the entire parameter space. For every parameter $\theta=(W,v)$ , suppose that $L$ is Fréchet differentiable at every point of some neighborhood of $\theta$ , that the map $z\mapsto DL(z)$ into the space of continuous real linear functionals is Fréchet differentiable at $\theta$ , that $L(\theta)\le L(z)$ for every $z$ in some neighborhood of $\theta$ , that $DL(\theta)=0$ , and that $H_\theta:=D(z\mapsto DL(z))(\theta)\ne0$ as a continuous linear map from the parameter space to its space of continuous real linear functionals. Then, for every real $M>0$ , there exists a real $\alpha>0$ such that, with $\theta_\alpha=(\alpha W,\alpha^{-1}v)$ , one has $f_{\theta_\alpha}(x)=f_\theta(x)$ for every $x\in\mathbb R^d$ , $L(\theta_\alpha)=L(\theta)$ , and $L(\theta_\alpha)\le L(z)$ for every $z$ in some neighborhood of $\theta_\alpha$ ; moreover, $L$ is Fréchet differentiable at every point of some neighborhood of $\theta_\alpha$ , the map $z\mapsto DL(z)$ is Fréchet differentiable at $\theta_\alpha$ , $DL(\theta_\alpha)=0$ , and $M\le\|D(z\mapsto DL(z))(\theta_\alpha)\|$ , where the final norm is the iterated operator norm, equivalently $\sup_{\|a\|\le1,\ \|b\|\le1}|D(z\mapsto DL(z))(\theta_\alpha)[a][b]|$ . The dimensions $d=0$ and $h=0$ are excluded by the hypotheses; no entry of $W$ or $v$ is individually required to be nonzero, and the quantified loss functional $\ell$ has no additional assumptions beyond the stated properties of its composite $L$ . The inverse $\alpha^{-1}$ is taken only for the positive, hence nonzero, scale supplied by the conclusion.

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