Helper for Theorem 6.63: the outer penalized objective whose unique minimizer is the scaled
proximal point of f at x.
Instances For
Evaluating the outer penalty from Theorem 6.63 gives the expected sum of f and the
(μ + 1)⁻¹ quadratic term.
Helper for Theorem 6.63: adding a finite real constant commutes with the infimum defining a Moreau envelope.
Helper for Theorem 6.63: the affine point minimizing the inner quadratic subproblem lies on the
segment from x to y, and its displacement from y is the expected scaled copy of x - y.
Helper for Theorem 6.63: the same affine interpolation point has displacement from x
equal to the textbook weight 1 / (μ + 1) times y - x.
Helper for Theorem 6.63: after evaluating the inner quadratic minimizer, the two endpoint
quadratic terms collapse to the single outer penalty ‖x - y‖² / (2 (μ + 1)).
Helper for Theorem 6.63: the cross term in the completed-square expansion vanishes because the inner quadratic minimizer satisfies the first-order balance equation.
Helper for Theorem 6.63: the remaining quadratic term after completing the square has
coefficient (μ + 1) / (2 μ).
Helper for Theorem 6.63: the affine transport sends the textbook candidate
lineMap x y (1 / (μ + 1)) back to y.
Helper for Theorem 6.63: the affine transport T v = x + (μ + 1) • (v - x) converts the
residual displacement from lineMap x y (1 / (μ + 1)) into the direct displacement from y.
Helper for Theorem 6.63: after the affine transport T, the residual Moreau-envelope
coefficient is exactly the completed-square coefficient (μ + 1) / (2 μ).
Helper for Theorem 6.63: the two-stage quadratic objective in the Moreau-envelope proof is a
completed square centered at lineMap x y (1 / (μ + 1)).
Helper for Theorem 6.63: minimizing the scaled proximal objective is equivalent to minimizing
the outer penalty y ↦ f y + ‖x - y‖² / (2 μ).
Helper for Theorem 6.63: scaling the outer penalty by μ + 1 turns it into the proximal
objective of the scaled function ((μ + 1) • f) at x.
Helper for Theorem 6.63: on the effective domain of g, the proximal objective has the
expected real-valued form g.toReal + (1 / 2) ‖z - x‖².
Helper for Theorem 6.63: every translated quadratic penalty with a nonnegative coefficient is convex as an extended-real-valued function.
Helper for Theorem 6.63: adding the quadratic penalty keeps a proper closed convex function proper, closed, and convex.
Helper for Theorem 6.63: for fixed y, the two-stage Moreau integrand equals the outer
penalty plus the transported residual kernel.
Helper for Theorem 6.63: the proximal objective of the Moreau envelope is the Moreau envelope
of the outer penalty after the affine transport v ↦ x + (μ + 1) • (v - x).
Helper for Theorem 6.63: the outer penalty is the positive inverse scaling of the proximal
objective of ((μ + 1) • f) at x.
Helper for Theorem 6.63: the outer penalty remains proper, closed, and convex under the same
owner hypotheses as f.
Helper for Theorem 6.63: a minimizer of the outer penalty remains a minimizer after Moreau smoothing, because the smoothing infimum is attained at the same point.
Helper for Theorem 6.63: if a Moreau-envelope minimizer already attains the unique minimum value of the outer function, then the envelope minimizer is the unique outer minimizer.
Helper for Theorem 6.63: if the outer penalty has the unique minimizer u, then every
minimizer of its Moreau envelope is also u.
Helper for Theorem 6.63: applying lineMap to the transported point
x + (μ + 1) • (v - x) recovers v.
Helper for Theorem 6.63: once the scaled proximal point of f at x is the singleton {u},
the proximal set of the Moreau envelope is the singleton at the transported point
lineMap x u (1 / (μ + 1)).
Theorem 6.63: if f is a proper closed convex extended-real-valued function, then at every
point x there is a unique proximal point u of the scaled function (μ + 1) f, and the
proximal set of the Moreau envelope M[μ, f] at x is the singleton containing
lineMap x u (1 / (μ + 1)). This is the chapter's set-valued rendering of the textbook formula
prox_{M_f^μ}(x) = x + (1 / (μ + 1)) (prox_{(μ + 1) f}(x) - x), stated without promoting a
chosen proximal point to primitive data.
If the proximal set of the scaled function (μ + 1) f at x is the singleton {u}, then
the proximal set of the Moreau envelope at x is the singleton containing
lineMap x u (1 / (μ + 1)), equivalently the weighted average
x + (1 / (μ + 1)) • (u - x). Under the same non-⊥ hypothesis and μ > 0, this is the
chapter's singleton-valued rendering of the textbook identity
prox_{M_f^μ}(x) = (μ x + u) / (μ + 1).