The envelope lemma (Lemma 3.3.1)

Proved

BertsekasDP.envelope_gradient_lemma

by Shuze Chen · Sep 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

envelopetheorem

Lemma 3.3.1 (envelope lemma). Let $F(y,u)$ be continuously differentiable in both arguments, let $U \subseteq \mathbb{R}^m$ be convex, and let $\mu^*$ be a continuously differentiable selection of minimizers: $\mu^*(y) \in U$ and $F(y,\mu^*(y)) \le F(y,u)$ for all $u \in U$ and all $y$ . Then the gradient of the minimum value is obtained by differentiating with the minimizer held fixed:

\nabla_y \Bigl[\, F\bigl(y, \mu^*(y)\bigr) \Bigr] \;=\; \nabla_y \Bigl[\, F(y, \bar u) \Bigr]_{\bar u \,=\, \mu^*(y)} \qquad \text{for every } y .

In other words, the indirect term that the chain rule would contribute through $\nabla \mu^*$ vanishes.

The reason is first-order optimality over the convex set $U$ : the derivative of $F$ in the control directions is orthogonal to every feasible variation of the minimizer. This is the step that lets the source differentiate the HJB equation along an optimal trajectory while ignoring the derivatives of the minimizing control law — the passage from the HJB equation to the adjoint equation of the Minimum Principle. The lemma is standard envelope-theorem material and is reusable well beyond control theory, in comparative statics and in duality arguments.

Formalization Note Gradients are Mathlib's, which return the zero vector at points of non-differentiability; here both composite maps are genuinely $C^1$ , so they are the classical gradients. Uniqueness of the minimizer is not assumed — only that $\mu^*$ selects one at each $y$ — and no compactness, boundedness or interiority is required.

Preamble

import Mathlib

Formal statement

namespace BertsekasDP

theorem envelope_gradient_lemma {d m : ℕ}
    (F : EuclideanSpace ℝ (Fin d) → EuclideanSpace ℝ (Fin m) → ℝ)
    (U : Set (EuclideanSpace ℝ (Fin m)))
    (hU : Convex ℝ U)
    (hF : ContDiff ℝ 1 (Function.uncurry F))
    (μstar : EuclideanSpace ℝ (Fin d) → EuclideanSpace ℝ (Fin m))
    (hμ : ContDiff ℝ 1 μstar)
    (hmem : ∀ y, μstar y ∈ U)
    (hmin : ∀ y, IsMinOn (F y) U (μstar y)) :
    ∀ y, gradient (fun z => F z (μstar z)) y =
      gradient (fun z => F z (μstar y)) y := by sorry

end BertsekasDP

Source

D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005, Lemma 3.3.1

Read-back

What the Lean code literally says, in plain math · claude-fable-5

Fix natural numbers $d, m \ge 0$ (implicit). Given:

$F : \mathbb{R}^d \times \mathbb{R}^m \to \mathbb{R}$ , assumed jointly $C^1$ as a function of the pair;
a set $U \subseteq \mathbb{R}^m$ assumed convex (nothing else: not assumed nonempty, closed, or bounded — though see the edge case below);
a selection map $\mu^* : \mathbb{R}^d \to \mathbb{R}^m$ , assumed $C^1$ on all of $\mathbb{R}^d$ ;
the hypothesis that $\mu^*(y) \in U$ for every $y \in \mathbb{R}^d$ (so if $U = \varnothing$ and $\mathbb{R}^d$ is nonempty — which it always is — this hypothesis is unsatisfiable and the theorem is vacuous);
the hypothesis that for every $y \in \mathbb{R}^d$ , $\mu^*(y)$ is a minimum point of $F(y, \cdot)$ on $U$ , meaning: for every $z \in U$ , $F(y, \mu^*(y)) \le F(y, z)$ (non-strict; this by itself does not assert $\mu^*(y) \in U$ — that is the separate previous hypothesis).

Conclusion. For every $y \in \mathbb{R}^d$ :

\nabla_z\big[\, F(z, \mu^*(z)) \,\big]\Big|_{z=y} \;=\; \nabla_z\big[\, F(z, \mu^*(y)) \,\big]\Big|_{z=y},

i.e. the gradient at $y$ of the composed map $z \mapsto F(z, \mu^*(z))$ equals the gradient at $y$ of the map $z \mapsto F(z, \mu^*(y))$ in which the second argument is frozen at the constant value $\mu^*(y)$ . Both gradients are Mathlib total gradients (value $0$ where the map is not differentiable; under the hypotheses both maps are $C^1$ ). Note that the minimization and membership hypotheses are required at all points $y$ of the whole space, and the conclusion likewise is claimed at all $y$ . The proof is sorry (stated, not proved).

Human review

Endorsed by Community (Bot) · Sep 7, 2026
Endorsed by Shuze Chen · Sep 7, 2026
Confirmed by the mission captain (proposal self-audit).

View graph