Prove2Me

Corollary (p. 12) — x0x_0 minimizes ff on MM iff 0∈G(x0)0 \in G(x_0)

Proved
ShorNonsmooth.Subdiff.isMinOn_iff_zero_mem_subdifferential

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

convex-analysisoptimality-conditionsp2o-batch-b23ap2o-gran-per-chapterp2o-plan-bookp2o-v1

Let M⊆EnM \subseteq E_n, let ff be convex on MM, and let x0x_0 be an interior point of MM. Then x0x_0 is a point of the minimum of ff on MM if and only if the zero vector is a subgradient:

f(x0)≤f(x)  for all x∈M  ⟺  0∈G(x0).f(x_0) \le f(x) \ \text{ for all } x \in M \iff 0 \in G(x_0).

This is the optimality condition of nonsmooth convex minimization.

Preamble
import Mathlib
import Definitions.Def_ShorNonsmooth_Subdiff_Subdifferential
Formal statement
namespace ShorNonsmooth.Subdiff

/-- Shor (1985), p. 12, Corollary (to Theorem 1.11): for a convex function `f` with domain `M`
and an interior point `x₀` of `M`, `x₀` is a point of the minimum of `f` on `M` if and only if
`0 ∈ G(x₀)`. -/
theorem isMinOn_iff_zero_mem_subdifferential {n : ℕ}
    (M : Set (EuclideanSpace ℝ (Fin n))) (f : EuclideanSpace ℝ (Fin n) → ℝ)
    (hf : ConvexOn ℝ M f) (x₀ : EuclideanSpace ℝ (Fin n)) (hx₀ : x₀ ∈ interior M) :
    (∀ x ∈ M, f x₀ ≤ f x) ↔ (0 : EuclideanSpace ℝ (Fin n)) ∈ subdifferential M f x₀ := by sorry

end ShorNonsmooth.Subdiff
Source
Shor, Minimization Methods for Non-Differentiable Functions, Springer 1985, p. 12, Corollary (after Theorem 1.11)
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