§2, p. 211 — the restriction of $f^{**}$ to $E$ is $f$

Proved

RockafellarMaxMono.Maximality.biconj_restrict_eq

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

convex-analysisconvex-conjugatep2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $E$ be a real Banach space, regarded as a subspace of its bidual $E^{**}$ through the canonical embedding $x \mapsto \hat x$ , $\hat x(x^*) = \langle x, x^* \rangle$ . If $f$ is a lower semicontinuous proper convex function on $E$ , then the biconjugate $f^{**} = (f^*)^*$ , a function on $E^{**}$ , satisfies

f^{**}(\hat x) = f(x) \qquad \text{for every } x \in E .

This is the Fenchel–Moreau theorem in the Banach-space setting, which the paper cites from Moreau. It is used, together with (2.2) and (2.4), to relate $\partial f$ and $\partial f^*$ .

Formalization Note The canonical embedding is Mathlib's NormedSpace.inclusionInDoubleDual ℝ E. $E$ is not assumed reflexive.

Preamble

import Mathlib
import Definitions.Def_RockafellarMaxMono_Shared_ProperConvex
import Definitions.Def_RockafellarMaxMono_Shared_Conj

Formal statement

namespace RockafellarMaxMono.Maximality

theorem biconj_restrict_eq {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [CompleteSpace E] (f : E → EReal) (hf : Shared.ProperConvex f) (hlsc : LowerSemicontinuous f) :
    ∀ x : E, Shared.conj (Shared.conj f) (NormedSpace.inclusionInDoubleDual ℝ E x) = f x := by sorry

end RockafellarMaxMono.Maximality

Source

Rockafellar, On the maximal monotonicity of subdifferential mappings, Pacific J. Math. 33 (1970), p. 211, §2

Read-back

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

Setting. $E$ is a real Banach space, $E^*$ is its continuous dual, and $E^{**}$ is the continuous dual of $E^*$ . The canonical embedding $\iota : E \to E^{**}$ is given by $\iota(x)(x^*) = x^*(x)$ . The function $f : E \to \overline{\mathbb{R}}$ has two hypotheses:

$f$ satisfies the imported predicate Shared.ProperConvex. It is not shown here; the name suggests "proper convex".
$f$ is lower semicontinuous for the norm topology.

The imported operation Shared.conj is not shown here; the name suggests the Fenchel conjugate. Applied to $f$ it gives $f^* : E^* \to \overline{\mathbb{R}}$ . Applied again, to $f^*$ on the normed space $E^*$ , it gives $f^{**} : E^{**} \to \overline{\mathbb{R}}$ .

Claim. For every $x \in E$ ,

f^{**}(\iota(x)) = f(x).

Degenerate cases. The claim concerns only points of $E^{**}$ in the image of $\iota$ . It says nothing about $f^{**}$ at other points of $E^{**}$ . If $E = \{0\}$ , the claim reduces to $f^{**}(0) = f(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

§2, p. 211 — the restriction of f∗∗f^{**}f∗∗ to EEE is fff

§2, p. 211 — the restriction of $f^{**}$ to $E$ is $f$