The gradient formulas of Moreau's theorem

For f closed proper convex on a finite-dimensional inner product space and w z = ½‖z‖², the Moreau envelope f □ w is finite everywhere and differentiable everywhere, with

∇(f □ w) z = z - prox (z | f), ∇(f* □ w) z = prox (z | f).

So the two halves of Moreau's splitting z = prox (z | f) + prox (z | f*) are the gradients of the two envelopes. The splitting itself is in Optimization/Prox.lean; what is added here is that ∂(f □ w) z is a single point, and a convex function with a one-point subdifferential at z is differentiable there.

Main results

• subgradient_infConv_quadFn — ∂(f □ w) z = {prox (z | f*)}.
• hasGradientAt_infConv_quadFn, hasGradientAt_infConv_conj_quadFn, gradient_infConv_quadFn, gradient_infConv_conj_quadFn — the gradient formulas (Theorem 31.5 in [^1]), in HasGradientAt form and in terms of Mathlib's gradient.
• closedProperConvexFn_infConv_quadFn — the Moreau envelope is finite everywhere, hence closed proper convex.
• conj_infConv_quadFn — (f □ w)* = f* + w, since conjugation turns □ into + and w* = w.

Implementation notes

No relative-interior or exactness hypothesis is needed: the conjugate of an infimal convolution is used in its unconditional direction, and the constraint qualification for the subgradient sum rule is supplied by w being finite and continuous.

References

[^1]: R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §31.

The Moreau envelope is closed proper convex

theorem Tdaf.ConvexAnalysis.dom_infConv_quadFn {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} (hf : ClosedProperConvexFn f) : dom (infConv f (quadFn (innerₗ E))) = Set.univ

The Moreau envelope is finite everywhere.

theorem Tdaf.ConvexAnalysis.closedProperConvexFn_infConv_quadFn {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} (hf : ClosedProperConvexFn f) : ClosedProperConvexFn (infConv f (quadFn (innerₗ E)))

Finite everywhere and convex, hence closed.

theorem Tdaf.ConvexAnalysis.conj_infConv_quadFn {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (f : E → EReal) : conj (innerₗ E) (infConv f (quadFn (innerₗ E))) = conj (innerₗ E) f + quadFn (innerₗ E)

The conjugate of a Moreau envelope: (f □ w)* = f* + w, since w* = w.

The gradient formulas

theorem Tdaf.ConvexAnalysis.subgradient_infConv_quadFn {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} (hf : ClosedProperConvexFn f) (z : E) : subgradient (innerₗ E) (infConv f (quadFn (innerₗ E))) z = {prox (innerₗ E) (conj (innerₗ E) f) z}

The subdifferential of a Moreau envelope is a single point: ∂(f □ w) z = {prox (z | f*)}. Conjugate inversion turns y ∈ ∂(f □ w) z into z ∈ ∂(f* + w) y, the sum rule splits that as ∂f* y + {y}, and what is left, z - y ∈ ∂f* y, characterises prox (z | f*).

theorem Tdaf.ConvexAnalysis.prox_conj_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} (hf : ClosedProperConvexFn f) (z : E) : prox (innerₗ E) (conj (innerₗ E) f) z = z - prox (innerₗ E) f z

The two proximal points add up to z, written here as a formula for the second.

theorem Tdaf.ConvexAnalysis.hasGradientAt_infConv_quadFn {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} (hf : ClosedProperConvexFn f) (z : E) : HasGradientAt (infConv f (quadFn (innerₗ E))) ((InnerProductSpace.toDual ℝ E) (prox (innerₗ E) (conj (innerₗ E) f) z)) z

prox (z | f*) = ∇(f □ w) z: the subdifferential is a single point, so the envelope is differentiable there.

theorem Tdaf.ConvexAnalysis.hasGradientAt_infConv_conj_quadFn {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} (hf : ClosedProperConvexFn f) (z : E) : HasGradientAt (infConv (conj (innerₗ E) f) (quadFn (innerₗ E))) ((InnerProductSpace.toDual ℝ E) (prox (innerₗ E) f z)) z

prox (z | f) = ∇(f* □ w) z. The previous statement applied to f*, using prox (z | f**) = z - prox (z | f*) = prox (z | f).

theorem Tdaf.ConvexAnalysis.gradient_infConv_quadFn {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} (hf : ClosedProperConvexFn f) (z : E) : gradient (fun (u : E) => (infConv f (quadFn (innerₗ E)) u).toReal) z = z - prox (innerₗ E) f z

∇(f □ w) z = z - prox (z | f).

theorem Tdaf.ConvexAnalysis.gradient_infConv_conj_quadFn {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} (hf : ClosedProperConvexFn f) (z : E) : gradient (fun (u : E) => (infConv (conj (innerₗ E) f) (quadFn (innerₗ E)) u).toReal) z = prox (innerₗ E) f z

∇(f* □ w) z = prox (z | f).

theorem Tdaf.ConvexAnalysis.differentiableAtFn_infConv_quadFn {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} (hf : ClosedProperConvexFn f) (z : E) : DifferentiableAtFn (infConv f (quadFn (innerₗ E))) z

The Moreau envelope is differentiable everywhere.