Theorem 4.1, proof (p. 95) — $L_U$ has a subgradient at $(\bar x, y(\bar x))$ with null $y$ -projection

Open

ShorNonsmooth.Decomposition.exists_subgradient_zero_y

by mikedeng1 · Oct 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

convex-analysisdecompositionp2o-batch-b23ap2o-gran-per-chapterp2o-plan-bookp2o-v1subgradient

Let $f_0$ and $f_i$ , $i = 1,\dots,n$ , be jointly convex, and let $U$ be Kuhn–Tucker multipliers of the subproblem (4.3)–(4.4) at $\bar x$ relative to an optimal $\bar y$ ; in particular $U \ge 0$ and $\bar y$ minimizes $L_U(\bar x, \cdot)$ over all $y$ . Then there is a vector $g^x \in E^x_l$ such that $(g^x, 0)$ is a subgradient of the Lagrange function $L_U$ at $(\bar x,\bar y)$ :

L_U(x,y) - L_U(\bar x,\bar y) \ge (g^x, x - \bar x) \qquad \text{for all } (x,y).

In the book's words, the subdifferential of $L_U$ at $(\bar x,\bar y)$ intersects the hyperplane $y = 0$ . This justifies the choice of subgradient in formula (4.6).

Preamble

import Mathlib
import Definitions.Def_ShorNonsmooth_Decomposition_ValueFunction

Formal statement

namespace ShorNonsmooth.Decomposition

/-- Shor (1985), proof of Theorem 4.1, p. 95 ("this is always possible, since
`L_U(x̄, y(x̄)) = min L(x̄, y)`"): if `f₀` and all `f_i` are jointly convex and `U` are Kuhn–Tucker
multipliers at `xbar` for the optimal point `ybar` (so `ybar` minimizes `L_U(xbar, ·)`), then the Lagrange
function `L_U` has a subgradient at `(xbar, ybar)` whose projection on the `y`-space vanishes. -/
theorem exists_subgradient_zero_y {l m n : ℕ}
    (f₀ : EuclideanSpace ℝ (Fin l) → EuclideanSpace ℝ (Fin m) → ℝ)
    (f : Fin n → EuclideanSpace ℝ (Fin l) → EuclideanSpace ℝ (Fin m) → ℝ)
    (hf₀ : JointlyConvex f₀) (hf : ∀ i, JointlyConvex (f i))
    (xbar : EuclideanSpace ℝ (Fin l)) (ybar : EuclideanSpace ℝ (Fin m))
    (U : Fin n → ℝ) (hU : IsKuhnTuckerMultiplier f₀ f xbar ybar U) :
    ∃ gx : EuclideanSpace ℝ (Fin l), IsJointSubgradient (lagrangian f₀ f U) xbar ybar gx 0 := by sorry

end ShorNonsmooth.Decomposition

Source

Shor, Minimization Methods for Non-Differentiable Functions, Springer 1985, p. 95, proof of Theorem 4.1 ("this is always possible, since L_U(x̄, y(x̄)) = min L(x̄, y)")

Human review

Endorsed by Shuze Chen · Oct 2, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 2, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Theorem 4.1, proof (p. 95) — LUL_ULU​ has a subgradient at (xˉ,y(xˉ))(\bar x, y(\bar x))(xˉ,y(xˉ)) with null yyy-projection

Theorem 4.1, proof (p. 95) — $L_U$ has a subgradient at $(\bar x, y(\bar x))$ with null $y$ -projection