noncomputable def ERealFunction.proximalObjective {H : Type u} [NormedAddCommGroup H] (f : H → ↑(Set.Ioi ⊥)) (x : H) : H → EReal

The unit proximal objective at x, whose minimizers are the proximal points of f at x.

def ERealFunction.proximalPoints {H : Type u} [NormedAddCommGroup H] (f : H → ↑(Set.Ioi ⊥)) (x : H) : Set H

Definition 12.23: the proximal points of f at x are the minimizers of the regularized objective y ↦ f y + (1 / 2) ‖x - y‖^2.

@[reducible, inline]

abbrev ERealFunction.IsProxPoint {H : Type u} [NormedAddCommGroup H] (f : H → ↑(Set.Ioi ⊥)) (x p : H) : Prop

Definition 12.23: p is a proximal point of f at x when it belongs to the argmin set of the regularized objective at x.

theorem ERealFunction.isProxPoint_iff_moreauEnvelope_eq {H : Type u} [NormedAddCommGroup H] (f : H → ↑(Set.Ioi ⊥)) (x p : H) : IsProxPoint f x p ↔ {}^[⟨1, ⋯⟩]f x = ↑(f p) + ↑(1 / 2 * ‖x - p‖ ^ 2)

A point is proximal exactly when it realizes the value of the unit Moreau envelope.

def ERealFunction.HasUniqueProxPoint {H : Type u} [NormedAddCommGroup H] (f : H → ↑(Set.Ioi ⊥)) : Prop

A function has a unique proximal point at every base point when the regularized objective y ↦ f y + (1 / 2) ‖x - y‖^2 admits a unique minimizer for every x.

noncomputable def ERealFunction.proximityOperator {H : Type u} [NormedAddCommGroup H] (f : H → ↑(Set.Ioi ⊥)) (hf : HasUniqueProxPoint f) : H → H

The proximity operator attached to a function with unique proximal points sends x to its unique proximal point.

theorem ERealFunction.proximityOperator_isProxPoint {H : Type u} [NormedAddCommGroup H] (f : H → ↑(Set.Ioi ⊥)) (hf : HasUniqueProxPoint f) (x : H) : IsProxPoint f x (proximityOperator f hf x)

The value of the proximity operator is a proximal point.

theorem ERealFunction.eq_proximityOperator_of_isProxPoint {H : Type u} [NormedAddCommGroup H] (f : H → ↑(Set.Ioi ⊥)) (hf : HasUniqueProxPoint f) {x p : H} (hp : IsProxPoint f x p) : p = proximityOperator f hf x

Any proximal point at x coincides with the value of the proximity operator at x.