Proximal mappings, and maximal monotonicity of the subdifferential #
For f closed proper convex and w x = ½ B x x, the infimum defining the Moreau envelope
(f □ w) z is attained at exactly one point, the proximal point prox (z | f), and the
minimiser is characterised by z - x ∈ ∂f x. That is the attainment and uniqueness half of
Moreau's decomposition; Optimization/Moreau.lean has the identity (f □ w) + (f* □ w) = w,
and Optimization/MoreauGradient.lean the gradient formulas.
Two corollaries follow from the same monotonicity argument. Proximation is nonexpansive, so
(x, x*) ↦ x + x* is a homeomorphism of the graph of ∂f onto the space, and ∂f is a maximal
monotone mapping — maximal among monotone relations, which is a different statement from the
maximal cyclic monotonicity of a subdifferential.
Main definitions #
moreauObj B f z— the objectivex ↦ f x + w (z - x), whose infimum is(f □ w) z.prox B f z— the proximal point: the unique minimiser ofmoreauObj B f z, or0when there is none.
Main results #
subgradient_quadFn_sub—∂(w (z - ·)) x = {x - z};recessionFn_quadFn_sub—w (z - ·)recedes in no direction but0.argmin_moreauObj_nonempty,mem_argmin_moreauObj_iff,existsUnique_sub_mem_subgradient,prox_eq_iff— the minimum exists, is unique, and solvesz - x ∈ ∂f x(Theorem 31.5 in [^1]);prox_add_prox_conj—z = prox (z | f) + prox (z | f*).pairingNorm_prox_sub_le,dist_prox_prox_le,lipschitzWith_prox— proximation is nonexpansive.subgradientRelHomeomorph— the graph of∂fis homeomorphic toE;isMaximalMonotoneRel_subgradientRel—∂fis maximal monotone.
Implementation notes #
Everything runs through the pairing B, never through the ambient norm, so prox is available on
product spaces carrying no InnerProductSpace instance; the norm enters only in continuous_prox.
prox is a Classical choice from the minimum set, with value 0 where that set is empty; the
standing hypothesis ClosedProperConvexFn f makes the set a singleton. Finite-dimensionality is
used only for attainment of the minimum.
References #
[^1]: R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §31.
The Moreau objective and the subdifferential of the quadratic #
The objective x ↦ f x + w (z - x), whose infimum over x is the envelope (f □ w) z.
Equations
- Tdaf.ConvexAnalysis.moreauObj B f z = f + fun (x : E) => Tdaf.ConvexAnalysis.quadFn B (z - x)
Instances For
x - z is a subgradient of u ↦ w (z - u) at x; the defect in the inequality is
½ B (u - x) (u - x).
The subdifferential of the translated quadratic is a singleton: ∂(w (z - ·)) x = {x - z}.
Testing at the point y + z forces ½ B ((z - x) + y) ((z - x) + y) ≤ 0.
The subdifferential of the quadratic is the identity: ∂w x = {x}.
u ↦ w (z - u) is closed proper convex: it is finite, convex and continuous.
The translated quadratic recedes in no direction: (w (z - ·))0⁺ y = +∞ for y ≠ 0.
Testing q (x + a • y) ≤ q x + a ν at x = z gives ½ a² B y y ≤ a ν for every a ≥ 0, which
fails for large a since B y y > 0.
Uniqueness of the proximal point: at most one x satisfies z - x ∈ ∂f x. Monotonicity
of ∂f gives 0 ≤ B (x₁ - x₂) (-(x₁ - x₂)), and definiteness finishes.
The proximal mapping prox (z | f): the point at which x ↦ f x + w (z - x) attains its
minimum, and 0 where no minimum exists — which for closed proper convex f never happens.
Equations
- Tdaf.ConvexAnalysis.prox B f z = Classical.epsilon fun (x : E) => x ∈ Tdaf.ConvexAnalysis.argmin (Tdaf.ConvexAnalysis.moreauObj B f z)
Instances For
The constraint qualification: w (z - ·) is finite and continuous, so the conjugate of
f + w (z - ·) splits and the subgradient sum rule applies.
The same at the origin: the conjugate of f + w splits.
The Moreau objective of a closed proper convex function is closed proper convex.
The Moreau objective has no direction of recession. Its recession function splits as
f0⁺ + (w (z - ·))0⁺, where the second term is +∞ off the origin.
Attainment: the infimum defining (f □ w) z is attained, because f + w (z - ·) is
closed proper convex with recession cone {0}.
The characterisation of the minimiser: x minimises f + w (z - ·) exactly when
z - x ∈ ∂f x. Fermat's rule, the sum rule and subgradient_quadFn_sub.
There is exactly one x with z = x + x* and x* ∈ ∂f x.
prox B f z minimises the Moreau objective.
The splitting z = x + x* with x* ∈ ∂f x exists, at x = prox (z | f).
That splitting determines prox.
Attainment and uniqueness in one statement: prox (z | f) = x exactly when z - x ∈ ∂f x.
The minimum set of the Moreau objective is {prox (z | f)}.
The envelope is the value of the objective at the proximal point.
The conjugate of a closed proper convex function is closed proper convex.
Moreau's decomposition of a point: z splits as prox (z | f) + prox (z | f*). Conjugate
inversion turns ∂f into ∂f*, so the second half of z = x + x* is prox (z | f*).
The graph of ∂f is homeomorphic to the space #
Proximation is nonexpansive in the norm the pairing induces. Monotonicity of ∂f gives
B (x₁ - x₂) (x₁ - x₂) ≤ B (x₁ - x₂) (z₁ - z₂), and Cauchy–Schwarz finishes.
prox is Lipschitz, hence continuous. The constant is 1 only for the pairing norm; in the
ambient norm it is the ratio of the two equivalence constants between the norms.
(x, x*) ↦ x + x* is a homeomorphism of the graph of ∂f onto E. It is bijective because
every z splits uniquely, continuous because addition is, and its inverse
z ↦ (prox (z | f), z - prox (z | f)) is continuous because prox is nonexpansive.
Equations
- One or more equations did not get rendered due to their size.
Instances For
∂f is maximal monotone #
The subdifferential of a closed proper convex function is maximal monotone. Given (y, y*)
monotonically related to the whole graph, the unique splitting of y + y* produces (x, x*) in
the graph with x + x* = y + y*; then y - x = -(y* - x*), so the monotonicity inequality reads
0 ≤ -|y - x|².
The inner-product case #
For innerₗ E the pairing norm is the norm itself, so proximation is nonexpansive on the nose.
The distance between two proximal points is at most the distance between the two points.
prox is nonexpansive in an inner-product space.