Moreau's decomposition

For a space paired with itself by a symmetric positive definite form B whose quadratic form is continuous, the quadratic w z = ½ B z z is its own conjugate, and infimal convolution with it splits w between a closed proper convex function and its conjugate:

(f □ w) + (f* □ w) = w.

This is the identity half of Moreau's decomposition. Attainment, uniqueness and the prox operator are in Optimization/Prox.lean, which needs finite dimensions; the gradient formulas are in Optimization/MoreauGradient.lean.

Main definitions

• quadFn B — w z = ½ B z z, as an EReal-valued function.

Main results

• conj_quadFn — the quadratic is self-conjugate under its own pairing.
• conj_quadFn_sub — (w (z - ·))* y = B z y + w y.
• moreau_add — Moreau's decomposition: (f □ w) z + (f* □ w) z = w z (Theorem 31.5 in [^1]).
• infConv_quadFn_ne_top, infConv_quadFn_ne_bot — both Moreau envelopes are finite.
• mem_subgradient_iff_infConv_eq — the Kuhn–Tucker conditions attached to a splitting z = x + y.

Implementation notes

The identity is ⨅ φ = -φ* 0 applied to φ = f + w (z - ·), with the conjugate of that sum split at the origin. The constraint qualification is continuity of w (z - ·) rather than a relative-interior condition, so no finite-dimensionality is needed. Everything goes through B and never through the norm, so the theorem applies verbatim on a product space carrying prodPairing (innerₗ U) (innerₗ X) and no InnerProductSpace instance; the inner-product case is recovered by quadFn_innerL.

References

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

The quadratic w z = ½ B z z

noncomputable def Tdaf.ConvexAnalysis.quadFn {E : Type u_1} [AddCommGroup E] [Module ℝ E] (B : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) : E → EReal

The quadratic w z = ½ B z z, EReal-valued so that it lives alongside conj and infConv.

Equations

• Tdaf.ConvexAnalysis.quadFn B z = ↑((B z) z / 2)

theorem Tdaf.ConvexAnalysis.quadFn_apply {E : Type u_1} [AddCommGroup E] [Module ℝ E] {B : E →ₗ[ℝ] E →ₗ[ℝ] ℝ} (z : E) : quadFn B z = ↑((B z) z / 2)

theorem Tdaf.ConvexAnalysis.quadFn_ne_bot {E : Type u_1} [AddCommGroup E] [Module ℝ E] {B : E →ₗ[ℝ] E →ₗ[ℝ] ℝ} (z : E) : quadFn B z ≠ ⊥

theorem Tdaf.ConvexAnalysis.quadFn_ne_top {E : Type u_1} [AddCommGroup E] [Module ℝ E] {B : E →ₗ[ℝ] E →ₗ[ℝ] ℝ} (z : E) : quadFn B z ≠ ⊤

@[simp]

theorem Tdaf.ConvexAnalysis.quadFn_neg {E : Type u_1} [AddCommGroup E] [Module ℝ E] {B : E →ₗ[ℝ] E →ₗ[ℝ] ℝ} (z : E) : quadFn B (-z) = quadFn B z

theorem Tdaf.ConvexAnalysis.quadFn_zero_sub {E : Type u_1} [AddCommGroup E] [Module ℝ E] {B : E →ₗ[ℝ] E →ₗ[ℝ] ℝ} : (fun (u : E) => quadFn B (0 - u)) = quadFn B

The quadratic translated to the origin is the quadratic: w (0 - ·) = w.

theorem Tdaf.ConvexAnalysis.convexFn_quadFn_sub {E : Type u_1} [AddCommGroup E] [Module ℝ E] {B : E →ₗ[ℝ] E →ₗ[ℝ] ℝ} [IsInnerPairing B] (z : E) : ConvexFn fun (x : E) => quadFn B (z - x)

x ↦ w (z - x) is convex: the defect is ½ a b B (u - v) (u - v) ≥ 0.

theorem Tdaf.ConvexAnalysis.convexFn_quadFn {E : Type u_1} [AddCommGroup E] [Module ℝ E] {B : E →ₗ[ℝ] E →ₗ[ℝ] ℝ} [IsInnerPairing B] : ConvexFn (quadFn B)

w is a convex function.

theorem Tdaf.ConvexAnalysis.proper_quadFn_sub {E : Type u_1} [AddCommGroup E] [Module ℝ E] {B : E →ₗ[ℝ] E →ₗ[ℝ] ℝ} (z : E) : Proper fun (x : E) => quadFn B (z - x)

x ↦ w (z - x) is proper: it is finite everywhere.

theorem Tdaf.ConvexAnalysis.conj_quadFn {E : Type u_1} [AddCommGroup E] [Module ℝ E] {B : E →ₗ[ℝ] E →ₗ[ℝ] ℝ} [IsInnerPairing B] (y : E) : conj B (quadFn B) y = quadFn B y

The quadratic is self-conjugate under its own pairing: w* = w. The supremum ⨆ x (B x y - ½ B x x) has defect ½ B (x - y) (x - y) and is attained at x = y.

theorem Tdaf.ConvexAnalysis.conj_quadFn_sub {E : Type u_1} [AddCommGroup E] [Module ℝ E] {B : E →ₗ[ℝ] E →ₗ[ℝ] ℝ} [IsInnerPairing B] (z y : E) : conj B (fun (x : E) => quadFn B (z - x)) y = ↑((B z) y) + quadFn B y

The conjugate of a translate of the quadratic: (w (z - ·))* y = B z y + w y. The supremum has defect ½ B ((x - z) - y) ((x - z) - y) and is attained at x = z + y.

The quadratic in a topological space

theorem Tdaf.ConvexAnalysis.continuous_quadFn_sub {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] {B : E →ₗ[ℝ] E →ₗ[ℝ] ℝ} [IsContinuousInnerPairing B] (z : E) : Continuous fun (x : E) => quadFn B (z - x)

x ↦ w (z - x) is continuous: the constraint qualification the theorem uses.

The inner-product instance

@[simp]

theorem Tdaf.ConvexAnalysis.quadFn_innerL {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (z : E) : quadFn (innerₗ E) z = ↑(‖z‖ ^ 2 / 2)

On a real inner-product space the quadratic is ½‖z‖².

Moreau's decomposition

theorem Tdaf.ConvexAnalysis.infConv_quadFn_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {B : E →ₗ[ℝ] E →ₗ[ℝ] ℝ} {f : E → EReal} (hb : ∀ (x : E), f x ≠ ⊥) (z : E) : infConv f (quadFn B) z = ⨅ (x : E), f x + quadFn B (z - x)

The Moreau envelope written out: (f □ w) z = inf_x {f x + w (z - x)}.

theorem Tdaf.ConvexAnalysis.moreau_add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {B : E →ₗ[ℝ] E →ₗ[ℝ] ℝ} [IsContinuousInnerPairing B] [IsCompatiblePairing B] {f : E → EReal} (hf : ClosedProperConvexFn f) (z : E) : infConv f (quadFn B) z + infConv (conj B f) (quadFn B) z = quadFn B z

Moreau's decomposition: infimal convolution with the quadratic splits the quadratic between f and f*. The proof is ⨅ φ = -φ* 0 for φ = f + w (z - ·), with the conjugate of that sum split at the origin; the sign flip y ↦ -y turns ⟨z, y⟩ + w y into w (z - y) - w z.

theorem Tdaf.ConvexAnalysis.infConv_quadFn_ne_top {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {B : E →ₗ[ℝ] E →ₗ[ℝ] ℝ} [IsContinuousInnerPairing B] [IsCompatiblePairing B] {f : E → EReal} (hf : ClosedProperConvexFn f) (z : E) : infConv f (quadFn B) z ≠ ⊤

The Moreau envelope of a closed proper convex function is never +∞. Both infima in the decomposition are real, since their sum is.

theorem Tdaf.ConvexAnalysis.infConv_quadFn_ne_bot {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {B : E →ₗ[ℝ] E →ₗ[ℝ] ℝ} [IsContinuousInnerPairing B] [IsCompatiblePairing B] {f : E → EReal} (hf : ClosedProperConvexFn f) (z : E) : infConv f (quadFn B) z ≠ ⊥

The Moreau envelope never takes -∞.

theorem Tdaf.ConvexAnalysis.infConv_conj_quadFn_ne_top {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {B : E →ₗ[ℝ] E →ₗ[ℝ] ℝ} [IsContinuousInnerPairing B] [IsCompatiblePairing B] {f : E → EReal} (hf : ClosedProperConvexFn f) (z : E) : infConv (conj B f) (quadFn B) z ≠ ⊤

The dual Moreau envelope is finite too.

theorem Tdaf.ConvexAnalysis.infConv_conj_quadFn_ne_bot {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {B : E →ₗ[ℝ] E →ₗ[ℝ] ℝ} [IsContinuousInnerPairing B] [IsCompatiblePairing B] {f : E → EReal} (hf : ClosedProperConvexFn f) (z : E) : infConv (conj B f) (quadFn B) z ≠ ⊥

The dual Moreau envelope never takes -∞.

theorem Tdaf.ConvexAnalysis.mem_subgradient_iff_infConv_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {B : E →ₗ[ℝ] E →ₗ[ℝ] ℝ} [IsContinuousInnerPairing B] [IsCompatiblePairing B] {f : E → EReal} (hf : ClosedProperConvexFn f) {x y z : E} (hz : x + y = z) : y ∈ subgradient B f x ↔ f x + quadFn B y = infConv f (quadFn B) z ∧ conj B f y + quadFn B x = infConv (conj B f) (quadFn B) z

The Kuhn–Tucker conditions for the decomposition: for a splitting z = x + y, the pair (x, y) attains both infima exactly when y ∈ ∂f x. It follows from moreau_add, because (f x + w y) + (f* y + w x) = (f x + f* y) + (w x + w y) while ⟨x, y⟩ + w x + w y = w z, so Fenchel's inequality makes the left side at least w z, which is the sum of the two infima.

That such a splitting exists and is unique is Optimization/Prox.lean.