On this page

Projections onto closed convex sets and Moreau's decomposition

GaussianAnalysis.convex.moreaulibrary/convex/moreau.v335 lines15 lemmas and theorems, 2 definitionssource

Imports 2 library modules and 15 external

External: HB.structures, mathcomp.classical.all_ssreflect_compat, mathcomp.algebra.algebraic_hierarchy.ssralg, mathcomp.algebra.numeric_hierarchy.ssrnum, mathcomp.algebra.matrix, mathcomp.classical.boolp, mathcomp.classical.classical_sets, mathcomp.classical.functions, mathcomp.reals.reals, mathcomp.analysis.topology_theory.topology, mathcomp.analysis.normedtype_theory.normedtype, mathcomp.analysis.derive, mathcomp.algebra.ring_tactic, mathcomp.algebra.field_tactic, mathcomp.algebra.arithmetic_tactic

Imported by 5

Required by 9 files of the paper proofs

Lemma 5.1 of Koehler and Sohn (arXiv 2608.27372, lines 4894-4921; Bauschke and Combettes, section 6.3) in 'rV[R]_N with the Frobenius inner product <x, y> = mxdot x y and |x|^2 = mxdot x x. K is a nonempty closed convex set and C a nonempty closed convex cone: x + t (y - x) is in K for x, y in K and 0 <= t <= 1, and a y is in C for y in C and a >= 0.

`proj K z`	the nearest point of K to z, if it exists (xget)
`polar C`	the polar cone [set u \| <u, y> <= 0 for every y in C]

proj_exists: a nonempty closed set has a nearest point to every z.
proj_variational: p in K is nearest to z iff <z - p, y - p> <= 0 for every y in K; the nearest point is unique (proj_unique), and projP gives K (proj K z) and the variational inequality.
proj_nonexpansive: |proj K z - proj K z'| <= |z - z'|.
cone_projP: p = proj C z iff p is in C, z - p is in polar C and <z - p, p> = 0.
moreau, Lemma 5.1: z = proj C z + proj (polar C) z with <proj C z, proj (polar C) z> = 0, hence (moreau_norm) |z|^2 = |proj C z|^2 + |proj (polar C) z|^2.
cone_proj_support, (eq:cone-projection-support): sup_(y in C, |y| <= 1) <z, y> = |proj C z|.

Main results

Results	Statement
proj_existsproj_variationalprojPproj_uniqueproj_nonexpansive	Projections in `'rV[R]_N` with the Frobenius inner product: a nonempty closed set has a nearest point to every `z` (compactness of the closed bounded sets); for `K` closed, convex and nonempty, `p` in `K` is nearest to `z` iff `<z - p, y - p> <= 0` for every `y` in `K`, the nearest point `proj K z` is unique, and `\|proj K z - proj K z'\| <= \|z - z'\|`.
moreaumoreau_normcone_projPcone_proj_supportpolar	Lemma 5.1 of Koehler and Sohn (Moreau's decomposition): for a closed convex cone `C`, `z = proj C z + proj (polar C) z` with the two parts orthogonal, so `\|z\|^2 = \|proj C z\|^2 + \|proj (polar C) z\|^2`; `p` in `C` is `proj C z` iff `z - p` is in the polar cone and orthogonal to `p`; and `sup_(y in C, \|y\| <= 1) <z, y> = \|proj C z\|`.

Declarations17 exported

sectionprojection

Context {R : realType} {N : nat}.
Implicit Types (K C : set 'rV[R]_N) (x y z p q u : 'rV[R]_N).

definition proj source, line 50

Type

forall {R : realType} {N : nat}, set 'rV_N -> 'rV_N -> 'rV_N

Definition

Definition proj K z : 'rV[R]_N := xget 0 [set p | K p /\
  forall y, K y -> mxdot (z - p) (z - p) <= mxdot (z - y) (z - y)].

Used by 16 declarations in 5 files

GaussianAnalysis.matrix.nuclear: range_duality
GaussianAnalysis.matrix.condition_cone: cond_support_proj, cond_support_sqr, cond_supportZ
GaussianAnalysis.matrix.trace_projection: trace_argmax, trace_argmaxP
GaussianAnalysis.comparison.cone_escape: cone_sup_proj, cgmt_aux_tr_cone_zero, cgmt_aux_tr_cone_ge
this file: projP, proj_eq, proj_nonexpansive, cone_projP, moreau, moreau_norm, cone_proj_support

definition polar main result source, line 53

Type

forall {R : realType} {N : nat}, set 'rV_N -> set 'rV_N

Definition

Definition polar C : set 'rV[R]_N := [set u | forall y, C y -> mxdot u y <= 0].

Main result

Stated in the README together with moreau.

Used by 8 declarations in 2 files

GaussianAnalysis.matrix.condition_cone: cond_support_sqr
this file: polar_closed, polar_convex, polar0, cone_projP, moreau, moreau_norm, cone_proj_support

lemma continuous_dist2 source, line 55

forall {R : realType} {N : nat} [z : 'rV_N],
continuous (fun y : 'rV_N => mxdot (z - y) (z - y))

Statement as written in the source

Lemma continuous_dist2 z :
  continuous (fun y : 'rV[R]_N => mxdot (z - y) (z - y)).

Used by 1 declaration in 1 file

this file: proj_exists

lemma le0_small source, line 70

forall {R : realType} [a b : R], (forall t : R, 0 < t <= 1 -> a <= t * b) -> a <= 0

A bound by t b for every 0 < t <= 1 is a bound by 0.

Statement as written in the source

Lemma le0_small (a b : R) : (forall t : R, 0 < t <= 1 -> a <= t * b) ->
  a <= 0.

Used by 2 declarations in 2 files

GaussianAnalysis.comparison.cgmt: escape_inf_minimax
this file: proj_variational

lemma proj_exists main result source, line 87

forall {R : realType} {N : nat} [K : set 'rV_N] (z : 'rV_N),
closed K ->
K !=set0 ->
exists2 p : 'rV_N,
  K p & forall y : 'rV_N, K y -> mxdot (z - p) (z - p) <= mxdot (z - y) (z - y)

A nonempty closed set has a nearest point to every z.

Main result, as the README states it

Projections in 'rV[R]_N with the Frobenius inner product: a nonempty closed set has a nearest point to every z (compactness of the closed bounded sets); for K closed, convex and nonempty, p in K is nearest to z iff <z - p, y - p> <= 0 for every y in K, the nearest point proj K z is unique, and |proj K z - proj K z'| <= |z - z'|.

Statement as written in the source

Lemma proj_exists K z : closed K -> K !=set0 -> exists2 p, K p &
  forall y, K y -> mxdot (z - p) (z - p) <= mxdot (z - y) (z - y).

Used by 1 declaration in 1 file

this file: projP

sectionconvex_projection

Context {R : realType} {N : nat}.
Variable K : set 'rV[R]_N.
Hypotheses (Kc : closed K) (K0 : K !=set0).
Hypothesis Kcvx : forall x y (t : R), K x -> K y -> 0 <= t <= 1 ->
  K (x + t *: (y - x)).

lemma proj_variational main result source, line 132

forall {R : realType} {N : nat} [K : set 'rV_N],
(forall (x y : 'rV_N) (t : R), K x -> K y -> 0 <= t <= 1 -> K (x + t *: (y - x))) ->
forall (z : 'rV_N) [p : 'rV_N],
K p ->
(forall y : 'rV_N, K y -> mxdot (z - p) (z - p) <= mxdot (z - y) (z - y)) <->
(forall y : 'rV_N, K y -> mxdot (z - p) (y - p) <= 0)

The variational characterization of the nearest point.

Main result

Stated in the README together with proj_exists.

Statement as written in the source

Lemma proj_variational (z p : 'rV[R]_N) : K p ->
  (forall y, K y -> mxdot (z - p) (z - p) <= mxdot (z - y) (z - y)) <->
  (forall y, K y -> mxdot (z - p) (y - p) <= 0).

Used by 2 declarations in 2 files

GaussianAnalysis.matrix.condition_cone: cond_support_sqr
this file: projP

lemma proj_unique main result source, line 158

forall {R : realType} {N : nat} [K : set 'rV_N] [z p q : 'rV_N],
K p ->
K q ->
(forall y : 'rV_N, K y -> mxdot (z - p) (y - p) <= 0) ->
(forall y : 'rV_N, K y -> mxdot (z - q) (y - q) <= 0) -> p = q

Main result

Stated in the README together with proj_exists.

Statement as written in the source

Lemma proj_unique (z p q : 'rV[R]_N) : K p -> K q ->
  (forall y, K y -> mxdot (z - p) (y - p) <= 0) ->
  (forall y, K y -> mxdot (z - q) (y - q) <= 0) -> p = q.

Used by 1 declaration in 1 file

this file: proj_eq

lemma projP main result source, line 170

forall {R : realType} {N : nat} [K : set 'rV_N],
closed K ->
K !=set0 ->
(forall (x y : 'rV_N) (t : R), K x -> K y -> 0 <= t <= 1 -> K (x + t *: (y - x))) ->
forall z : 'rV_N,
K (proj K z) /\ (forall y : 'rV_N, K y -> mxdot (z - proj K z) (y - proj K z) <= 0)

Main result

Stated in the README together with proj_exists.

Statement as written in the source

Lemma projP (z : 'rV[R]_N) : K (proj K z) /\
  forall y, K y -> mxdot (z - proj K z) (y - proj K z) <= 0.

Used by 9 declarations in 4 files

GaussianAnalysis.matrix.nuclear: range_duality
GaussianAnalysis.matrix.condition_cone: cond_support_sqr, cond_supportZ
GaussianAnalysis.matrix.trace_projection: trace_argmaxP
this file: proj_eq, proj_nonexpansive, cone_projP, moreau, cone_proj_support

lemma proj_eq source, line 181

forall {R : realType} {N : nat} [K : set 'rV_N],
closed K ->
K !=set0 ->
(forall (x y : 'rV_N) (t : R), K x -> K y -> 0 <= t <= 1 -> K (x + t *: (y - x))) ->
forall [z p : 'rV_N],
K p -> (forall y : 'rV_N, K y -> mxdot (z - p) (y - p) <= 0) -> proj K z = p

Statement as written in the source

Lemma proj_eq (z p : 'rV[R]_N) : K p ->
  (forall y, K y -> mxdot (z - p) (y - p) <= 0) -> proj K z = p.

Used by 4 declarations in 3 files

GaussianAnalysis.matrix.condition_cone: cond_supportZ
GaussianAnalysis.matrix.trace_projection: trace_argmax_eq
this file: cone_projP, moreau

lemma proj_nonexpansive main result source, line 188

forall {R : realType} {N : nat} [K : set 'rV_N],
closed K ->
K !=set0 ->
(forall (x y : 'rV_N) (t : R), K x -> K y -> 0 <= t <= 1 -> K (x + t *: (y - x))) ->
forall z z' : 'rV_N, frobenius (proj K z - proj K z') <= frobenius (z - z')

Main result

Stated in the README together with proj_exists.

Statement as written in the source

Lemma proj_nonexpansive (z z' : 'rV[R]_N) :
  frobenius (proj K z - proj K z') <= frobenius (z - z').

sectioncone_projection

Context {R : realType} {N : nat}.
Variable C : set 'rV[R]_N.
Hypotheses (Cc : closed C) (C0 : C 0).
Hypothesis Ccvx : forall x y (t : R), C x -> C y -> 0 <= t <= 1 ->
  C (x + t *: (y - x)).
Hypothesis Ccone : forall y (a : R), C y -> 0 <= a -> C (a *: y).

lemma polar_closed source, line 215

forall {R : realType} {N : nat} [C : set 'rV_N], closed (polar C)

Statement as written in the source

Lemma polar_closed : closed (polar C).

Used by 2 declarations in 1 file

this file: moreau, cone_proj_support

lemma polar_convex source, line 233

forall {R : realType} {N : nat} [C : set 'rV_N] [x y : 'rV_N] [t : R],
polar C x -> polar C y -> 0 <= t <= 1 -> polar C (x + t *: (y - x))

Statement as written in the source

Lemma polar_convex x y (t : R) : polar C x -> polar C y -> 0 <= t <= 1 ->
  polar C (x + t *: (y - x)).

Used by 2 declarations in 1 file

this file: moreau, cone_proj_support

lemma polar0 source, line 242

forall {R : realType} {N : nat} [C : set 'rV_N], polar C 0

Statement as written in the source

Lemma polar0 : polar C 0.

Used by 2 declarations in 1 file

this file: moreau, cone_proj_support

lemma cone_projP main result source, line 247

forall {R : realType} {N : nat} [C : set 'rV_N],
closed C ->
C 0 ->
(forall (x y : 'rV_N) (t : R), C x -> C y -> 0 <= t <= 1 -> C (x + t *: (y - x))) ->
(forall (y : 'rV_N) (a : R), C y -> 0 <= a -> C (a *: y)) ->
forall (z : 'rV_N) [p : 'rV_N],
C p -> proj C z = p <-> polar C (z - p) /\ mxdot (z - p) p = 0

p is the projection of z onto C iff z - p is in the polar cone and is orthogonal to p.

Main result

Stated in the README together with moreau.

Statement as written in the source

Lemma cone_projP (z p : 'rV[R]_N) : C p ->
  proj C z = p <-> polar C (z - p) /\ mxdot (z - p) p = 0.

Used by 1 declaration in 1 file

this file: moreau

theorem moreau main result source, line 266

forall {R : realType} {N : nat} [C : set 'rV_N],
closed C ->
C 0 ->
(forall (x y : 'rV_N) (t : R), C x -> C y -> 0 <= t <= 1 -> C (x + t *: (y - x))) ->
(forall (y : 'rV_N) (a : R), C y -> 0 <= a -> C (a *: y)) ->
forall z : 'rV_N,
z = proj C z + proj (polar C) z /\ mxdot (proj C z) (proj (polar C) z) = 0

Lemma 5.1 of Koehler and Sohn.

Main result, as the README states it

Lemma 5.1 of Koehler and Sohn (Moreau's decomposition): for a closed convex cone C, z = proj C z + proj (polar C) z with the two parts orthogonal, so |z|^2 = |proj C z|^2 + |proj (polar C) z|^2; p in C is proj C z iff z - p is in the polar cone and orthogonal to p; and sup_(y in C, |y| <= 1) <z, y> = |proj C z|.

Statement as written in the source

Theorem moreau (z : 'rV[R]_N) :
  z = proj C z + proj (polar C) z /\
  mxdot (proj C z) (proj (polar C) z) = 0.

Used by 3 declarations in 2 files

GaussianAnalysis.matrix.condition_cone: cond_support_sqr
this file: moreau_norm, cone_proj_support

lemma moreau_norm main result source, line 284

forall {R : realType} {N : nat} [C : set 'rV_N],
closed C ->
C 0 ->
(forall (x y : 'rV_N) (t : R), C x -> C y -> 0 <= t <= 1 -> C (x + t *: (y - x))) ->
(forall (y : 'rV_N) (a : R), C y -> 0 <= a -> C (a *: y)) ->
forall z : 'rV_N,
mxdot z z = mxdot (proj C z) (proj C z) + mxdot (proj (polar C) z) (proj (polar C) z)

Main result

Stated in the README together with moreau.

Statement as written in the source

Lemma moreau_norm (z : 'rV[R]_N) :
  mxdot z z = mxdot (proj C z) (proj C z) +
              mxdot (proj (polar C) z) (proj (polar C) z).

Used by 1 declaration in 1 file

GaussianAnalysis.matrix.condition_cone: cond_support_sqr

theorem cone_proj_support main result source, line 294

forall {R : realType} {N : nat} [C : set 'rV_N],
closed C ->
C 0 ->
(forall (x y : 'rV_N) (t : R), C x -> C y -> 0 <= t <= 1 -> C (x + t *: (y - x))) ->
(forall (y : 'rV_N) (a : R), C y -> 0 <= a -> C (a *: y)) ->
forall z : 'rV_N,
sup [set mxdot z y | y in [set y | C y /\ mxdot y y <= 1]] = frobenius (proj C z)

(eq:cone-projection-support)

Main result

Stated in the README together with moreau.

Statement as written in the source

Theorem cone_proj_support (z : 'rV[R]_N) :
  sup [set mxdot z y | y in [set y | C y /\ mxdot y y <= 1]] =
  frobenius (proj C z).

Used by 2 declarations in 2 files

GaussianAnalysis.matrix.condition_cone: cond_support_proj
GaussianAnalysis.comparison.cone_escape: cone_sup_proj

Generated from commit 9046883 (tag phase12) of the ellipsoid fitting repository. Signatures are printed by Rocq 9.1.1; links in the source statements come from the compiled .glob files. The source links open the files on GitHub at this commit, in the now-public repository.