§3, p. 213 — $(f+j)^$ is finite and continuous throughout $E^$

Proved

RockafellarMaxMono.Maximality.conj_add_halfSqNorm_finite_continuous

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, let $f$ be a lower semicontinuous proper convex function on $E$ , and let $j(x) = \tfrac12\|x\|^2$ . Then the conjugate $(f+j)^*$ is finite and continuous throughout $E^*$ : there is a continuous real-valued function $h$ on $E^*$ (with its norm topology) such that

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

This is what makes the finite-and-continuous case of Theorem A (Minty's theorem) applicable to $(f+j)^*$ on $E^*$ .

Formalization Note "Finite and continuous" is encoded as the existence of a continuous $h : E^* \to \mathbb{R}$ whose cast to EReal equals $(f+j)^*$ everywhere. The paper derives this from the inf-convolution formula $(f+j)^* = f^* \,\square\, j^*$ ; that formula is not part of this statement.

Preamble

import Mathlib
import Definitions.Def_RockafellarMaxMono_Shared_ProperConvex
import Definitions.Def_RockafellarMaxMono_Shared_Conj
import Definitions.Def_RockafellarMaxMono_Shared_HalfSqNorm

Formal statement

namespace RockafellarMaxMono.Maximality

theorem conj_add_halfSqNorm_finite_continuous {E : Type*} [NormedAddCommGroup E]
    [NormedSpace ℝ E] [CompleteSpace E] (f : E → EReal) (hf : Shared.ProperConvex f)
    (hlsc : LowerSemicontinuous f) :
    ∃ h : StrongDual ℝ E → ℝ, Continuous h ∧
      ∀ x' : StrongDual ℝ E, Shared.conj (fun y => f y + Shared.halfSqNorm y) 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

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 topology. 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.

Two imported objects appear, not shown here:

$q$ is Shared.halfSqNorm. The name suggests $q(y) = \tfrac12\|y\|^2$ .
$g^*$ is Shared.conj g. The name suggests the Fenchel conjugate.

Let $g = f + q$ , meaning $g(y) = f(y) + q(y)$ with extended-real addition.

Claim. There is a function $h : E^* \to \mathbb{R}$ , continuous for the norm topology on $E^*$ , such that for every $x^* \in E^*$ ,

g^*(x^*) = h(x^*).

So $g^*$ is finite everywhere on $E^*$ (never $\pm\infty$ ) and is norm-continuous as a real-valued function.

Degenerate cases. If $E = \{0\}$ , the claim reduces to $g^*(0)$ being a finite real number.

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

§3, p. 213 — (f+j)∗(f+j)^*(f+j)∗ is finite and continuous throughout E∗E^*E∗

§3, p. 213 — $(f+j)^$ is finite and continuous throughout $E^$