§3, p. 213 — Minty's theorem: finite continuous convex functions have maximal monotone subdifferentials

Proved

RockafellarMaxMono.Maximality.minty_maximal_monotone

by mikedeng1 · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

convex-analysismonotone-operatorsp2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $V$ be a real Banach space with dual $V^*$ , and let $h : V \to \mathbb{R}$ be a convex function that is finite and continuous everywhere on $V$ . Then its subdifferential

\partial h : V \to V^*

is a maximal monotone operator.

This is the case of Theorem A established earlier by Minty, which Rockafellar quotes and applies to the function $(f+j)^*$ on the Banach space $E^*$ ; it is therefore stated for an arbitrary real Banach space $V$ rather than only for $E$ .

Formalization Note "Everywhere finite" is real-valuedness of $h$ ; convexity is Mathlib's ConvexOn ℝ Set.univ h; continuity is for the norm topology. The subdifferential is taken of $h$ viewed as a function into $(-\infty,+\infty]$ .

Preamble

import Mathlib
import Definitions.Def_RockafellarMaxMono_Shared_Subdiff
import Definitions.Def_RockafellarMaxMono_Maximality_MonotoneOperator

Formal statement

namespace RockafellarMaxMono.Maximality

theorem minty_maximal_monotone {V : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V]
    [CompleteSpace V] (h : V → ℝ) (hconv : ConvexOn ℝ Set.univ h) (hcont : Continuous h) :
    IsMaximalMonotone (Shared.subdiff (fun x => ((h x : ℝ) : EReal))) := by sorry

end RockafellarMaxMono.Maximality

Source

Rockafellar, On the maximal monotonicity of subdifferential mappings, Pacific J. Math. 33 (1970), p. 213, §3, Proof of Theorem A (citing Minty [2])

Read-back

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

Setting. $V$ is a real Banach space and $V^*$ is its continuous dual. The function $h : V \to \mathbb{R}$ is real-valued (never infinite) and has two hypotheses:

$h$ is convex on all of $V$ : $h(tx + (1-t)y) \le t\,h(x) + (1-t)\,h(y)$ for all $x, y \in V$ and $t \in [0,1]$ .
$h$ is continuous for the norm topology.

Let $\tilde h : V \to \overline{\mathbb{R}}$ be $h$ with its values viewed as extended reals. Let $\partial \tilde h$ be the imported operation Shared.subdiff applied to $\tilde h$ . It is not shown here; the name suggests the subdifferential. It gives an operator $x \mapsto \partial \tilde h(x) \subseteq V^*$ .

Claim. This operator satisfies IsMaximalMonotone, a predicate imported from a separate definitions file. Its text is not part of this declaration. The name suggests: monotone, and not strictly contained, graph-wise, in any other monotone operator $V \to 2^{V^*}$ .

Degenerate cases. There are no hypotheses that could fail to be satisfiable: every continuous affine $h$ , including every constant, qualifies. If $V = \{0\}$ , then $V^* = \{0\}$ and $h$ is a single real number. The claim then concerns the operator $0 \mapsto \partial \tilde h(0) \subseteq \{0\}$ .

Human review

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

View graph