Proximal point selector

Definition

KLSModular_FunctionalInequalities_Analysis_Convex_Proximal

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

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

For $f:E\to\mathbb{R}$ and $z\in E$ , proximalPoint f z is the classical choice of a point $x$ satisfying $f(x)+\langle z-x,y-x\rangle\le f(y)$ for every $y\in E$ , selected by Classical.epsilon. This expresses the resolvent condition $z-x\in\partial f(x)$ ; existence and uniqueness for convex finite-dimensional functions are discussed by the surrounding development rather than assumed in this definition.

Original module imports

import FunctionalInequalities.Analysis.Convex.Subgradient

Original declaration excerpt

Shown in the original module context.

def proximalPoint {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (f : E → ℝ) (z : E) : E :=
  Classical.epsilon fun x => ∀ y, f x + ⟪z - x, y - x⟫ ≤ f y

Module navigation

Direct project imports: Analysis/Convex/Subgradient.

Theorems in source order:

Project result: The KLS conjecture.

Original module · FunctionalInequalities.Analysis.Convex.Proximal · Frozen source 408915f.

Definition code

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Convex_Subgradient

noncomputable section
open MeasureTheory Set
open scoped RealInnerProductSpace
section LT12D2ProximalPoint
open Set
open scoped RealInnerProductSpace
namespace FunctionalInequalities
namespace Analysis
section InnerProduct
variable {E : Type*}
variable [NormedAddCommGroup E] [InnerProductSpace ℝ E]
/-- The **proximal point** (resolvent of the subdifferential) of `f` at `z`: a point `x` such that
`z − x` is a subgradient of `f` at `x`, i.e. the minimiser of `x ↦ f x + ½‖x − z‖²` (weak Letwin route,
Alexandrov's theorem). For convex `f` on a finite-dimensional space it exists and is unique. -/
def proximalPoint {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (f : E → ℝ) (z : E) : E :=
  Classical.epsilon fun x => ∀ y, f x + ⟪z - x, y - x⟫ ≤ f y
end InnerProduct
end Analysis
end FunctionalInequalities
end LT12D2ProximalPoint

Source

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

View graph