Papers With

← All papers
First page of Nonmaximal sums of maximally monotone operators under Rockafellar's constraint qualification

Nonmaximal sums of maximally monotone operators under Rockafellar's constraint qualification

Weifeng Yang

cs.LG Sep 9, 2026 · v2 math.FA
formalization analysis
Read PDF arXiv abstract Code
TL;DR
Formalizes in Lean the c0 counterexample to Rockafellar's sum conjecture and the general pullback lemma, with code available on GitHub.
Abstract
We construct counterexamples to Rockafellar's sum conjecture in which two maximally monotone operators satisfy the interior-domain condition but their sum is not maximally monotone. We give one counterexample on $c_0$ and another on $\ell^1$ with its usual norm. We establish a general construction theorem that computes the entire monotone polar of a class of graphs, gives a necessary and sufficient condition for their maximal monotonicity, and shows how a positive rank-one perturbation yields a nonmaximal sum under this condition. We verify the theorem's hypotheses and its maximality criterion on $c_0$, thereby obtaining a counterexample to the conjecture. Furthermore, we construct a bounded linear surjection from $\ell^1$ onto $c_0$ and use it to obtain the counterexample on $\ell^1$. Lean formalizations of the $c_0$ counterexample and the pullback lemma are also provided.
Problem

Rockafellar's sum theorem guarantees maximal monotonicity of a sum of maximally monotone operators in reflexive Banach spaces under an interior-domain condition. Whether this condition alone suffices on arbitrary Banach spaces (the unrestricted sum question) was open.

Approach

A general construction theorem is established that computes the entire monotone polar of a class of graphs, giving a necessary and sufficient condition for their maximal monotonicity. Adding an everywhere-defined positive rank-one operator is shown to yield a nonmaximal sum under the interior-domain condition. The hypotheses and maximality criterion are verified on c0, and a bounded linear surjection from ℓ1 onto c0 transfers the result. Lean formalizations of the c0 counterexample and the pullback lemma are provided.

Results

Explicit counterexamples to Rockafellar's sum conjecture are constructed on c0 and on standard ℓ1: two maximally monotone operators satisfy the interior-domain condition yet their sum is not maximally monotone. A finite radial bound is proved for one operator in each pair.