§2, p. 210 — the conjugate $f^$ is a weak lsc proper convex function on $E^*$

Proved

RockafellarMaxMono.Maximality.conj_properConvex_lsc

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 with dual $E^*$ , and let $f$ be a lower semicontinuous proper convex function on $E$ . Then its conjugate $f^*$ is

lower semicontinuous for the weak* topology on $E^*$ ,
lower semicontinuous for the strong (norm) topology on $E^*$ , and
a proper convex function on $E^*$ .

This is what allows the results stated for $f$ (for instance (2.2)) to be applied to $f^*$ on the Banach space $E^*$ .

Formalization Note Weak* lower semicontinuity is stated for $f^*$ viewed as a function on Mathlib's WeakDual ℝ E (the dual with the weak* topology), via the identity map StrongDual.toWeakDual. The paper says "(and hence strongly lower semicontinuous)"; both lower semicontinuity claims are part of the statement.

Preamble

import Mathlib
import Definitions.Def_RockafellarMaxMono_Shared_ProperConvex
import Definitions.Def_RockafellarMaxMono_Shared_Conj

Formal statement

namespace RockafellarMaxMono.Maximality

theorem conj_properConvex_lsc {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [CompleteSpace E] (f : E → EReal) (hf : Shared.ProperConvex f) (hlsc : LowerSemicontinuous f) :
    LowerSemicontinuous (fun w : WeakDual ℝ E => Shared.conj f (StrongDual.toWeakDual.symm w)) ∧
      LowerSemicontinuous (Shared.conj f) ∧ Shared.ProperConvex (Shared.conj f) := by sorry

end RockafellarMaxMono.Maximality

Source

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

Read-back

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

Setting. $E$ is a real Banach space and $E^*$ is its continuous dual with the operator norm. 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 on $E$ .

$f^* : E^* \to \overline{\mathbb{R}}$ denotes the imported operation Shared.conj f. It is not shown here; the name suggests the Fenchel conjugate.

Claim. Three things hold together:

$f^*$ is lower semicontinuous when $E^*$ carries the weak-* topology, the topology of pointwise convergence on $E$ . Formally, this is the function on the weak dual obtained by sending each weak-dual element to the same functional in $E^*$ and then applying $f^*$ .
$f^*$ is lower semicontinuous when $E^*$ carries its norm topology.
$f^*$ , as a function on the normed space $E^*$ , satisfies Shared.ProperConvex (the same unseen predicate, now applied on $E^*$ ).

Degenerate cases. If $E = \{0\}$ , then $E^* = \{0\}$ . Parts 1 and 2 hold automatically on a one-point space. The claim then reduces to $f^*$ on the one-point space $\{0\}$ satisfying Shared.ProperConvex. Whether that holds depends on the unseen definitions.

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. 210 — the conjugate f∗f^*f∗ is a weak* lsc proper convex function on E∗E^*E∗

§2, p. 210 — the conjugate $f^$ is a weak lsc proper convex function on $E^*$