On this page

The nuclear norm and the range duality

GaussianAnalysis.matrix.nuclearlibrary/matrix/nuclear.v409 lines20 lemmas and theorems, 3 definitionssource

Imports 5 library modules and 13 external

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

Imported by 1

GaussianAnalysis.matrix.condition_cone

Required by 11 files of the paper proofs

The nuclear norm of A : 'M[R]_(m, n) is the dual norm of the operator norm for the Frobenius pairing <A, B> = mxdot A B. For a symmetric matrix it is the sum of the absolute values of the eigenvalues.

nuclear_ub, nuclear_le: the supremum; nuclear_ge0, nuclearZ, nuclearN, nuclearD and nuclear_eq0: a norm; mxdot_le_nuclear, the duality inequality |<A, B>| <= opnorm B * nuclear A.
frobenius_le_nuclear and nuclear_le_frobenius: frobenius A <= nuclear A <= sqrt n * frobenius A (frobenius_le_opnorm: frobenius B <= sqrt n * opnorm B); frobenius_sqr_le_nuclear: |A|_F^2 <= opnorm A * nuclear A.
nuclear_outer: nuclear (x x^T) = |x|^2.
nuclear_spectral: for A = P^T diag(d) P with P orthogonal, nuclear A = sum_i |d_i|, attained at P^T diag(sign d_i) P; nuclear_sym: for A symmetric, the supremum may be taken over the symmetric B.
range_duality, Lemma 2.2 of Koehler and Sohn (arXiv 2608.27372, lines 794-826) in the form the paper uses: for W_1, ..., W_k in 'M[R]_n, if |<l, y>| <= M nuclear (coef_adj W l) for every l in 'rV[R]_k, then y = coef_map W D for some D with opnorm D <= M; range_duality_sym: D is symmetric when the W_i are. The proof projects y on the compact convex set {coef_map W D | opnorm D <= M} (proj of library/convex/moreau.v), seen in 'rV[R]_(n * n) through vec_mx (mxdot_vec_mxr): no Slater condition or general convex duality is needed.

`nuclear A`	sup of <A, B> over the B with opnorm B <= 1
`coef_map W D`	the row (<W_i, D>)_i
`coef_adj W l`	sum_i l_i W_i, the adjoint of coef_map W

Main results

Results	Statement
nuclearmxdot_le_nuclearnuclearDnuclear_eq0nuclear_spectralnuclear_outer	The nuclear norm, defined as the dual norm of `opnorm` for the Frobenius pairing: a norm with `\|<A, B>\| <= opnorm B * nuclear A`, `frobenius A <= nuclear A <= sqrt n * frobenius A`, `nuclear (x x^T) = \|x\|^2`, and for `A = P^T diag(d) P` with `P` orthogonal, `nuclear A = sum_i \|d_i\|`.
range_dualityrange_duality_sym	Range duality (Koehler-Sohn Lemma 2.2): for `W_1, ..., W_k` in `'M[R]_n`, if `\|<l, y>\| <= M nuclear (sum_i l_i W_i)` for every `l`, then `y = (<W_i, D>)_i` for some `D` with `opnorm D <= M`, symmetric when the `W_i` are. By the nearest point of `y` in the compact convex image of the operator-norm ball, without a general duality theorem.

Declarations23 exported

sectionnuclear

Variable R : realType.
Implicit Types m n : nat.

definition nuclear main result source, line 56

Type

forall [R : realType] [m n : nat], 'M_(m, n) -> R

Definition

Definition nuclear m n (A : 'M[R]_(m, n)) : R :=
  sup [set mxdot A B | B in [set B : 'M[R]_(m, n) | opnorm B <= 1]].

Main result, as the README states it

The nuclear norm, defined as the dual norm of opnorm for the Frobenius pairing: a norm with |<A, B>| <= opnorm B * nuclear A, frobenius A <= nuclear A <= sqrt n * frobenius A, nuclear (x x^T) = |x|^2, and for A = P^T diag(d) P with P orthogonal, nuclear A = sum_i |d_i|.

Used by 16 declarations in 1 file

this file: nuclear_ub, nuclear_le, nuclear_ge0, mxdot_le_nuclear, nuclearZ, nuclearN, nuclearD, frobenius_sqr_le_nuclear, frobenius_le_nuclear, nuclear_le_frobenius, nuclear_eq0, nuclear_outer, nuclear_spectral, nuclear_sym, range_duality, range_duality_sym

lemma frobenius_le_opnorm source, line 59

forall [R : realType] [m n : nat] (B : 'M_(m, n)),
frobenius B <= Num.ExtraDef.sqrtr n%:R * opnorm B

Statement as written in the source

Lemma frobenius_le_opnorm m n (B : 'M[R]_(m, n)) :
  frobenius B <= Num.sqrt n%:R * opnorm B.

Used by 4 declarations in 1 file

this file: nuclear_has_sup, mxdot_le_nuclear, nuclear_le_frobenius, range_duality

lemma nuclear_has_sup source, line 69

forall [R : realType] [m n : nat] (A : 'M_(m, n)),
has_sup [set mxdot A B | B in [set B | opnorm B <= 1]]

Statement as written in the source

Lemma nuclear_has_sup m n (A : 'M[R]_(m, n)) :
  has_sup [set mxdot A B | B in [set B : 'M[R]_(m, n) | opnorm B <= 1]].

Used by 2 declarations in 1 file

this file: nuclear_ub, nuclear_le

lemma nuclear_ub source, line 79

forall [R : realType] [m n : nat] (A : 'M_(m, n)) [B : 'M_(m, n)],
opnorm B <= 1 -> mxdot A B <= nuclear A

Statement as written in the source

Lemma nuclear_ub m n (A B : 'M[R]_(m, n)) : opnorm B <= 1 -> mxdot A B <= nuclear A.

Used by 5 declarations in 1 file

this file: nuclear_ge0, mxdot_le_nuclear, nuclearD, nuclear_outer, nuclear_spectral

lemma nuclear_le source, line 84

forall [R : realType] [m n : nat] [A : 'M_(m, n)] [b : R],
(forall B : 'M_(m, n), opnorm B <= 1 -> mxdot A B <= b) -> nuclear A <= b

Statement as written in the source

Lemma nuclear_le m n (A : 'M[R]_(m, n)) (b : R) :
  (forall B : 'M[R]_(m, n), opnorm B <= 1 -> mxdot A B <= b) -> nuclear A <= b.

Used by 8 declarations in 1 file

this file: nuclearZ, nuclearD, nuclear_le_frobenius, nuclear_eq0, nuclear_outer, nuclear_spectral, nuclear_sym, range_duality

lemma nuclear_ge0 source, line 91

forall [R : realType] [m n : nat] (A : 'M_(m, n)), 0 <= nuclear A

Statement as written in the source

Lemma nuclear_ge0 m n (A : 'M[R]_(m, n)) : 0 <= nuclear A.

Used by 3 declarations in 1 file

this file: nuclearZ, frobenius_le_nuclear, nuclear_eq0

lemma mxdot_le_nuclear main result source, line 97

forall [R : realType] [m n : nat] (A B : 'M_(m, n)), `|mxdot A B| <= opnorm B * nuclear A

The duality inequality.

Main result

Stated in the README together with nuclear.

Statement as written in the source

Lemma mxdot_le_nuclear m n (A B : 'M[R]_(m, n)) :
  `|mxdot A B| <= opnorm B * nuclear A.

Used by 2 declarations in 1 file

this file: nuclearZ, frobenius_sqr_le_nuclear

lemma nuclearZ source, line 117

forall [R : realType] [m n : nat] (a : R) (A : 'M_(m, n)),
nuclear (a *: A) = `|a| * nuclear A

Statement as written in the source

Lemma nuclearZ m n (a : R) (A : 'M[R]_(m, n)) : nuclear (a *: A) = `|a| * nuclear A.

Used by 1 declaration in 1 file

this file: nuclearN

lemma nuclearN source, line 131

forall [R : realType] [m n : nat] (A : 'M_(m, n)), nuclear (- A) = nuclear A

Statement as written in the source

Lemma nuclearN m n (A : 'M[R]_(m, n)) : nuclear (- A) = nuclear A.

lemma nuclearD main result source, line 134

forall [R : realType] [m n : nat] (A B : 'M_(m, n)),
nuclear (A + B) <= nuclear A + nuclear B

Main result

Stated in the README together with nuclear.

Statement as written in the source

Lemma nuclearD m n (A B : 'M[R]_(m, n)) : nuclear (A + B) <= nuclear A + nuclear B.

lemma frobenius_sqr_le_nuclear source, line 140

forall [R : realType] [m n : nat] (A : 'M_(m, n)), frobenius A ^+ 2 <= opnorm A * nuclear A

Statement as written in the source

Lemma frobenius_sqr_le_nuclear m n (A : 'M[R]_(m, n)) :
  frobenius A ^+ 2 <= opnorm A * nuclear A.

Used by 1 declaration in 1 file

this file: frobenius_le_nuclear

lemma frobenius_le_nuclear source, line 147

forall [R : realType] [m n : nat] (A : 'M_(m, n)), frobenius A <= nuclear A

Statement as written in the source

Lemma frobenius_le_nuclear m n (A : 'M[R]_(m, n)) : frobenius A <= nuclear A.

Used by 1 declaration in 1 file

this file: nuclear_eq0

lemma nuclear_le_frobenius source, line 157

forall [R : realType] [m n : nat] (A : 'M_(m, n)),
nuclear A <= Num.ExtraDef.sqrtr n%:R * frobenius A

Statement as written in the source

Lemma nuclear_le_frobenius m n (A : 'M[R]_(m, n)) :
  nuclear A <= Num.sqrt n%:R * frobenius A.

lemma nuclear_eq0 main result source, line 166

forall [R : realType] [m n : nat] (A : 'M_(m, n)), (nuclear A == 0) = (A == 0)

Main result

Stated in the README together with nuclear.

Statement as written in the source

Lemma nuclear_eq0 m n (A : 'M[R]_(m, n)) : (nuclear A == 0) = (A == 0).

lemma nuclear_outer main result source, line 175

forall [R : realType] [n : nat] (x : 'cV_n), nuclear (x *m x^T) = frobenius x ^+ 2

nuclear (x x^T) = |x|^2.

Main result

Stated in the README together with nuclear.

Statement as written in the source

Lemma nuclear_outer n (x : 'cV[R]_n) : nuclear (x *m x^T) = frobenius x ^+ 2.

lemma nuclear_spectral main result source, line 190

forall [R : realType] [n : nat] [A P : 'M_n] [d : 'rV_n],
P \is orthogonalmx -> A = P^T *m diag_mx d *m P -> nuclear A = \sum_i `|d 0 i|

For a symmetric matrix, the sum of the absolute values of the eigenvalues.

Main result

Stated in the README together with nuclear.

Statement as written in the source

Lemma nuclear_spectral n (A P : 'M[R]_n) (d : 'rV[R]_n) :
  P \is orthogonalmx -> A = P^T *m diag_mx d *m P ->
  nuclear A = \sum_i `|d 0 i|.

lemma nuclear_sym source, line 232

forall [R : realType] [n : nat] [A : 'M_n] [b : R],
A \is symmetricmx ->
(forall B : 'M_n, B \is symmetricmx -> opnorm B <= 1 -> mxdot A B <= b) -> nuclear A <= b

The supremum for a symmetric matrix is attained on the symmetric matrices.

Statement as written in the source

Lemma nuclear_sym n (A : 'M[R]_n) (b : R) : A \is symmetricmx ->
  (forall B : 'M[R]_n, B \is symmetricmx -> opnorm B <= 1 -> mxdot A B <= b) ->
  nuclear A <= b.

sectionrange_duality

Variable R : realType.
Variables (k n : nat) (W : 'I_k -> 'M[R]_n).

definition coef_map source, line 262

Type

forall [R : realType] [k n : nat], ('I_k -> 'M_n) -> 'M_n -> 'rV_k

Definition

Definition coef_map (D : 'M[R]_n) : 'rV[R]_k := \row_i mxdot (W i) D.

L D = (<W_i, D>)_i and its adjoint L^* l = sum_i l_i W_i.

Used by 3 declarations in 1 file

this file: mxdot_coef_map, range_duality, range_duality_sym

definition coef_adj source, line 264

Type

forall [R : realType] [k n : nat], ('I_k -> 'M_n) -> 'rV_k -> 'M_n

Definition

Definition coef_adj (l : 'rV[R]_k) : 'M[R]_n := \sum_i l 0 i *: W i.

Used by 3 declarations in 1 file

this file: mxdot_coef_map, range_duality, range_duality_sym

lemma mxdot_coef_map source, line 266

forall [R : realType] [k n : nat] (W : 'I_k -> 'M_n) (l : 'rV_k) (D : 'M_n),
mxdot l (coef_map W D) = mxdot (coef_adj W l) D

Statement as written in the source

Lemma mxdot_coef_map (l : 'rV[R]_k) (D : 'M[R]_n) :
  mxdot l (coef_map D) = mxdot (coef_adj l) D.

Used by 1 declaration in 1 file

this file: range_duality

lemma mxdot_vec_mxr source, line 273

forall [R : realType] [m p : nat] (A : 'M_(m, p)) (v : 'rV_(m * p)),
mxdot A (vec_mx v) = mxdot (mxvec A) v

Statement as written in the source

Lemma mxdot_vec_mxr m p (A : 'M[R]_(m, p)) (v : 'rV[R]_(m * p)) :
  mxdot A (vec_mx v) = mxdot (mxvec A) v.

Used by 5 declarations in 2 files

this file: range_duality
GaussianAnalysis.matrix.condition_cone: mxdot_quad_vec, cond_cone_vec_closed, mxdot_vec_mx, cond_slice_vec_closed

theorem range_duality main result source, line 284

forall [R : realType] [k n : nat] [W : 'I_k -> 'M_n] [y : 'rV_k] [M : R],
0 <= M ->
(forall l : 'rV_k, `|mxdot l y| <= M * nuclear (coef_adj W l)) ->
exists2 D : 'M_n, opnorm D <= M & coef_map W D = y

Lemma 2.2 of Koehler and Sohn: if |<l, y>| <= M nuclear (L^* l) for every l, then y = L D for some D with opnorm D <= M.

Main result, as the README states it

Range duality (Koehler-Sohn Lemma 2.2): for W_1, ..., W_k in 'M[R]_n, if |<l, y>| <= M nuclear (sum_i l_i W_i) for every l, then y = (<W_i, D>)_i for some D with opnorm D <= M, symmetric when the W_i are. By the nearest point of y in the compact convex image of the operator-norm ball, without a general duality theorem.

Statement as written in the source

Theorem range_duality (y : 'rV[R]_k) (M : R) : 0 <= M ->
  (forall l : 'rV[R]_k, `|mxdot l y| <= M * nuclear (coef_adj l)) ->
  exists2 D : 'M[R]_n, opnorm D <= M & coef_map D = y.

Used by 1 declaration in 1 file

this file: range_duality_sym

corollary range_duality_sym main result source, line 387

forall [R : realType] [k n : nat] [W : 'I_k -> 'M_n] [y : 'rV_k] [M : R],
0 <= M ->
(forall i : 'I_k, W i \is symmetricmx) ->
(forall l : 'rV_k, `|mxdot l y| <= M * nuclear (coef_adj W l)) ->
exists2 D : 'M_n, D \is symmetricmx & opnorm D <= M /\ coef_map W D = y

With symmetric W_i, the preimage can be taken symmetric.

Main result

Stated in the README together with range_duality.

Statement as written in the source

Corollary range_duality_sym (y : 'rV[R]_k) (M : R) : 0 <= M ->
  (forall i, W i \is symmetricmx) ->
  (forall l : 'rV[R]_k, `|mxdot l y| <= M * nuclear (coef_adj l)) ->
  exists2 D : 'M[R]_n, D \is symmetricmx & opnorm D <= M /\ coef_map D = y.

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.