Prove2Me

(3.1) — sum rule ∂(f+j)(x)=∂f(x)+∂j(x)\partial(f+j)(x) = \partial f(x) + \partial j(x)

Proved
RockafellarMaxMono.Maximality.subdiff_add_halfSqNorm

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

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

Let EE be a real Banach space, let ff be a lower semicontinuous proper convex function on EE, and let j(x)=12∥x∥2j(x) = \tfrac12\|x\|^2. Then

∂(f+j)(x)=∂f(x)+∂j(x)for every x∈E,\partial(f+j)(x) = \partial f(x) + \partial j(x) \qquad \text{for every } x \in E ,

where the right-hand side is the Minkowski sum {x1∗+x2∗∣x1∗∈∂f(x), x2∗∈∂j(x)}\{x_1^* + x_2^* \mid x_1^* \in \partial f(x),\ x_2^* \in \partial j(x)\} in E∗E^*.

The sum rule holds here because jj is finite and continuous everywhere. In the proof of Theorem A it transfers information about ∂(f+j)\partial(f+j) back to ∂f\partial f.

Formalization Note The paper prints "∂(f+j)=∂f(x)+∂j(x)\partial(f + j) = \partial f(x) + \partial j(x)", omitting the argument xx on the left; we state the evident reading ∂(f+j)(x)\partial(f+j)(x). f+jf + j is the pointwise sum in (−∞,+∞](-\infty,+\infty]; the set sum uses Mathlib's pointwise addition of sets.

Preamble
import Mathlib
import Definitions.Def_RockafellarMaxMono_Shared_ProperConvex
import Definitions.Def_RockafellarMaxMono_Shared_Subdiff
import Definitions.Def_RockafellarMaxMono_Shared_HalfSqNorm
open Pointwise
Formal statement
namespace RockafellarMaxMono.Maximality

theorem subdiff_add_halfSqNorm {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [CompleteSpace E] (f : E → EReal) (hf : Shared.ProperConvex f) (hlsc : LowerSemicontinuous f) :
    ∀ x : E, Shared.subdiff (fun y => f y + Shared.halfSqNorm y) x = Shared.subdiff f x + Shared.subdiff Shared.halfSqNorm x := by sorry

end RockafellarMaxMono.Maximality
Source
Rockafellar, On the maximal monotonicity of subdifferential mappings, Pacific J. Math. 33 (1970), p. 213, (3.1)
Read-back

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

Setting. EE is a real Banach space and E∗E^* is its continuous dual. The function f:E→R‾f : E \to \overline{\mathbb{R}} has two hypotheses:

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

Two imported objects appear, not shown here:

  • qq is Shared.halfSqNorm. The name suggests q(y)=12∥y∥2q(y) = \tfrac12\|y\|^2.
  • ∂g(x)⊆E∗\partial g(x) \subseteq E^* is Shared.subdiff. The name suggests the subdifferential.

Claim. For every x∈Ex \in E,

∂(f+q)(x)  =  ∂f(x)+∂q(x)  =  { a+b:a∈∂f(x), b∈∂q(x) }.\partial\bigl(f + q\bigr)(x) \;=\; \partial f(x) + \partial q(x) \;=\; \{\,a + b : a \in \partial f(x),\ b \in \partial q(x)\,\}.

The sum f+qf + q is taken pointwise, y↦f(y)+q(y)y \mapsto f(y) + q(y), using extended-real addition. The right-hand side is the Minkowski sum of subsets of E∗E^*.

Degenerate cases. If ∂f(x)=∅\partial f(x) = \varnothing or ∂q(x)=∅\partial q(x) = \varnothing, the Minkowski sum is empty, so the claim says ∂(f+q)(x)=∅\partial(f + q)(x) = \varnothing. In the sum f+qf + q, the convention (−∞)+(+∞)=−∞(-\infty) + (+\infty) = -\infty applies wherever those values occur. If E={0}E = \{0\}, the claim reduces to an identity about the single point 0∈E∗={0}0 \in E^* = \{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