After Definition 2.1, p. 539 — nonnegativity and separation of the Bregman distance

Proved

ChenTeboullePMD.Rate.bregman_nonneg

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

bregman-distancebregman-functionconvex-optimizationp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $\psi$ be a Bregman function with open zone $S$ . For $x\in\bar S$ and $y\in S$ , its distance satisfies

D_\psi(x,y)\ge0,\qquad D_\psi(x,y)=0\ \Longleftrightarrow\ x=y.

This supplies the sign and equality case used throughout the PMD analysis.

Formalization Note The covector derivative defining $D_\psi$ is evaluated at $y\in S$ , where $\psi$ is continuously differentiable. The ambient space is a real normed space; finite dimensionality is unnecessary for this remark.

Preamble

import Mathlib
import Definitions.Def_BeckTeboulleMD_EMDA_Setting
import Definitions.Def_ChenTeboullePMD_Rate_Setting

Formal statement

namespace ChenTeboullePMD.Rate

open BeckTeboulleMD.EMDA

/-- Remark after Definition 2.1, p. 539. -/
theorem bregman_nonneg {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    (S : Set E) (ψ : E → ℝ) (hψ : IsBregmanFunction S ψ) :
    ∀ x ∈ closure S, ∀ y ∈ S,
      0 ≤ bregman ψ x y ∧ (bregman ψ x y = 0 ↔ x = y) := by sorry

end ChenTeboullePMD.Rate

Source

Chen & Teboulle, Convergence analysis of a proximal-like minimization algorithm using Bregman functions, SIAM J. Optim. 3 (1993), p. 539, paragraph after Definition 2.1

Human review

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

View graph