The Proximal Map Is One-Lipschitz

Proved

FunctionalInequalities.Analysis.lipschitzWith_proximalPoint_readable

by Lazyfill · Oct 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This formalizes the nonexpansiveness property of the proximal map.

Let $E$ be a finite-dimensional real inner-product space and let $f:E\to\mathbb R$ be convex on all of $E$ . For the Lean definition proximalPoint f, the map is $1$ -Lipschitz:

\|\operatorname{prox}_f(z)-\operatorname{prox}_f(w)\|\le \|z-w\|\qquad(z,w\in E).

Equivalently, proximalPoint f is LipschitzWith 1. This declaration supplies a global continuity estimate used by later almost-everywhere differentiability arguments.

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis. Shown in its original module context. Proof omitted.

theorem lipschitzWith_proximalPoint {f : E → ℝ} (hconv : ConvexOn ℝ univ f) :
    LipschitzWith 1 (proximalPoint f)

Module navigation

Module: Analysis/Convex/Proximal.

Supporting theorems: exists_subgradient_slope_le_inner_add.

Next: hasFDerivAt_half_sq_sub_moreau.

Source excerpt, lines 162–163 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Convex_Proximal

open Set
variable {E : Type*}
variable [NormedAddCommGroup E] [InnerProductSpace ℝ E]
variable [FiniteDimensional ℝ E]

Formal statement


theorem FunctionalInequalities.Analysis.lipschitzWith_proximalPoint_readable {f : E → ℝ} (hconv : ConvexOn ℝ univ f) :
    LipschitzWith 1 (proximalPoint f) := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/Convex/Proximal.lean#L161-L178 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.Convex.Proximal`, declaration `FunctionalInequalities.Analysis.lipschitzWith_proximalPoint`; the repository is private at upload time).

View graph