Moreau decomposition

TheoremVariational characterization of projection onto a convex cone#✓fully proved

Variational characterization of the projection onto a cone with complete carrier: p is the projection of x iff the residual pairs nonpositively with the cone and is orthogonal to p. The ambient space need not be complete.

theorem convexProjection_eq_iff (C : PointedCone ℝ E) (hC : IsComplete (C : Set E))
    (x p : E) (hp : p ∈ C) :
    convexProjection (C : Set E) x = p ↔
      (∀ y ∈ C, ⟪x - p, y⟫_ℝ ≤ 0) ∧ ⟪x - p, p⟫_ℝ = 0

Uses 3 · Used by 3

Statement usesNearest-point projection onto a convex set

Proof usesNearest points coincide with the convex projection · Variational inequality for the convex projection

Used byVariational characterization determines the cone projection · Cone projection residual pairs nonpositively with the cone · Cone projection residual is orthogonal to the projection

TheoremCone projection residual pairs nonpositively with the cone#✓fully proved

The residual of the cone projection pairs nonpositively with every point of the cone.

theorem convexProjection_inner_le_zero (C : PointedCone ℝ E)
    (hC : IsComplete (C : Set E)) (x y : E) (hy : y ∈ C) :
    ⟪x - convexProjection (C : Set E) x, y⟫_ℝ ≤ 0

Uses 3 · Used by 1

Statement usesNearest-point projection onto a convex set

Proof usesVariational characterization of projection onto a convex cone · The convex projection lies in the set

Used byCone projection residual lies in the negative polar

TheoremCone projection residual is orthogonal to the projection#✓fully proved

The residual of the cone projection is orthogonal to the projection.

theorem convexProjection_inner_self (C : PointedCone ℝ E) (hC : IsComplete (C : Set E))
    (x : E) :
    ⟪x - convexProjection (C : Set E) x, convexProjection (C : Set E) x⟫_ℝ = 0

Uses 3 · Used by 2

Statement usesNearest-point projection onto a convex set

Proof usesVariational characterization of projection onto a convex cone · The convex projection lies in the set

Used byMoreau decomposition, polar form · Moreau decomposition

TheoremVariational characterization determines the cone projection#✓fully proved

A point satisfying the cone variational characterization is the projection.

theorem convexProjection_eq_of_forall_inner_le_zero (C : PointedCone ℝ E)
    (hC : IsComplete (C : Set E)) {x p : E} (hp : p ∈ C)
    (h1 : ∀ y ∈ C, ⟪x - p, y⟫_ℝ ≤ 0) (h2 : ⟪x - p, p⟫_ℝ = 0) :
    convexProjection (C : Set E) x = p

Uses 2 · Used by 1

Statement usesNearest-point projection onto a convex set

Proof usesVariational characterization of projection onto a convex cone

Used byMoreau decomposition, polar form

DefinitionNegative polar cone#✓fully proved

The negative polar is the standard dual cone of the negated set. Continuity makes its carrier closed without requiring completeness of the ambient space.

def polarCone (K : Set E) : ProperCone ℝ E where
  toSubmodule := PointedCone.dual (innerₗ E) (-K)
  isClosed' := PointedCone.isClosed_dual fun x => (innerSL ℝ x).continuous

Used by 6

Used byMoreau decomposition, polar form · Membership in the negative polar cone · Moreau decomposition · Negative polar agrees with the inner dual of the negated cone · Bipolar theorem for closed convex cones · Cone projection residual lies in the negative polar

TheoremMembership in the negative polar cone#✓fully proved

Membership in the negative polar uses the nonpositive inner-product convention.

theorem mem_polarCone {K : Set E} {y : E} :
    y ∈ polarCone K ↔ ∀ x ∈ K, ⟪x, y⟫_ℝ ≤ 0

Uses 1 · Used by 3

Statement usesNegative polar cone

Used byMoreau decomposition, polar form · Bipolar theorem for closed convex cones · Cone projection residual lies in the negative polar

TheoremCone projection residual lies in the negative polar#✓fully proved

The residual of a cone projection lies in its negative polar.

theorem sub_convexProjection_mem_polarCone (C : PointedCone ℝ E)
    (hC : IsComplete (C : Set E)) (x : E) :
    x - convexProjection (C : Set E) x ∈ polarCone (C : Set E)

Uses 4 · Used by 1

Statement usesNegative polar cone · Nearest-point projection onto a convex set

Proof usesCone projection residual pairs nonpositively with the cone · Membership in the negative polar cone

Used byMoreau decomposition, polar form

TheoremNegative polar agrees with the inner dual of the negated cone#✓fully proved

In a complete ambient space, the negative polar agrees with Mathlib's inner dual of the negated carrier.

theorem polarCone_eq_innerDual_neg (K : Set E) :
    polarCone K = ProperCone.innerDual (-K)

Uses 1

Statement usesNegative polar cone

TheoremMoreau decomposition, polar form#✓fully proved

The cone projection's residual is the projection onto its negative polar. This accepts a Mathlib proper cone directly.

theorem convexProjection_polarCone (C : ProperCone ℝ E) (x : E) :
    convexProjection (polarCone (C : Set E)) x = x - convexProjection (C : Set E) x

Uses 7 · Used by 1

Statement usesNegative polar cone · Nearest-point projection onto a convex set

Proof usesVariational characterization determines the cone projection · Cone projection residual is orthogonal to the projection · Membership in the negative polar cone · Cone projection residual lies in the negative polar · The convex projection lies in the set

Used byMoreau decomposition

TheoremMoreau decomposition#✓fully proved

A point is the sum of its projections onto a proper cone and its negative polar, and the projections are orthogonal.

theorem moreau_decomposition (C : ProperCone ℝ E) (x : E) :
    x = convexProjection (C : Set E) x + convexProjection (polarCone (C : Set E)) x ∧
      ⟪convexProjection (C : Set E) x, convexProjection (polarCone (C : Set E)) x⟫_ℝ = 0

Uses 4

Statement usesNegative polar cone · Nearest-point projection onto a convex set

Proof usesCone projection residual is orthogonal to the projection · Moreau decomposition, polar form

TheoremBipolar theorem for closed convex cones#✓fully proved

The negative bipolar of a proper cone is itself, by Mathlib's inner-dual bipolar theorem.

theorem polarCone_polarCone (C : ProperCone ℝ E) :
    polarCone (polarCone (C : Set E) : Set E) = C

Uses 2

Statement usesNegative polar cone

Proof usesMembership in the negative polar cone

11 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.