Proposition 2.8(i) — $\operatorname{zer}(M+S)$ is a closed convex subset of $\mathcal P\times\mathcal D$

Proved

MonoSkew.Main.proposition_2_8_i

by mikedeng1 · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

dualitymonotone-operatorsp2o-batch-pfp2bp2o-gran-per-chapterp2o-plan-paperp2o-v1primal-dual

In the setting of Problems 1.1 and 1.2 ( $A$ , $B$ maximally monotone, $L$ bounded linear, $z\in\mathcal H$ , $r\in\mathcal G$ , $M$ and $S$ as in (1.8) on $\mathcal K=\mathcal H\oplus\mathcal G$ ), the set

\operatorname{zer}(M+S)=\{(x,v)\in\mathcal K\mid 0\in M(x,v)+S(x,v)\}

is a closed convex subset of $\mathcal P\times\mathcal D$ , where $\mathcal P$ and $\mathcal D$ are the solution sets of the primal inclusion (1.2) and the dual inclusion (1.3).

Thus every zero of the monotone+skew operator yields a primal solution and a dual solution at once.

Formalization Note "Closed" is in the norm topology of $\mathcal K$ = WithLp 2 (H × G); "subset of $\mathcal P\times\mathcal D$ " is stated componentwise: every $(x,v)\in\operatorname{zer}(M+S)$ has $x\in\mathcal P$ and $v\in\mathcal D$ .

Preamble

import Mathlib
import Definitions.Def_ThreeOpSplitting_Convergence_MonotoneOperators
import Definitions.Def_ThreeOpSplitting_Convergence_WeakConvergence
import Definitions.Def_DouglasRachfordPPA_GenDR_Operators
import Definitions.Def_MonoSkew_Main_Basic

open InnerProductSpace Filter Topology
open ThreeOpSplitting.Convergence DouglasRachfordPPA.GenDR

Formal statement

namespace MonoSkew.Main

/-- Proposition 2.8(i) (p. 8): in the setting of Problems 1.1 and 1.2, `zer(M + S)` is a closed
convex subset of `𝒫 × 𝒟`. -/
theorem proposition_2_8_i {H G : Type*}
    [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
    [NormedAddCommGroup G] [InnerProductSpace ℝ G] [CompleteSpace G]
    (A : H → Set H) (B : G → Set G) (hA : IsMaximalMonotone A) (hB : IsMaximalMonotone B)
    (L : H →L[ℝ] G) (z : H) (r : G) :
    IsClosed (zer (addSingle (opM A B z r) (opS L))) ∧
    Convex ℝ (zer (addSingle (opM A B z r) (opS L))) ∧
    ∀ p ∈ zer (addSingle (opM A B z r) (opS L)),
      p.fst ∈ primalSet A B L z r ∧ p.snd ∈ dualSet A B L z r := by sorry

end MonoSkew.Main

Source

Briceño-Arias and Combettes, A Monotone+Skew Splitting Model for Composite Monotone Inclusions in Duality, arXiv:1011.5517v1, p. 8, Proposition 2.8(i)

Human review

Endorsed by Shuze Chen · Oct 7, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 7, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Proposition 2.8(i) — zer⁡(M+S)\operatorname{zer}(M+S)zer(M+S) is a closed convex subset of P×D\mathcal P\times\mathcal DP×D

Proposition 2.8(i) — $\operatorname{zer}(M+S)$ is a closed convex subset of $\mathcal P\times\mathcal D$