GaussianAnalysisRocq library documentation
Main resultsGlossary
On this page
GaussianAnalysismatrixtrace_projection

The maximizer of a trace-penalized quadratic on a closed convex set

GaussianAnalysis.matrix.trace_projectionlibrary/matrix/trace_projection.v443 lines28 lemmas and theorems, 3 definitionssource
Imports 3 library modules and 14 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.algebra.ring_tactic, mathcomp.algebra.field_tactic, mathcomp.algebra.arithmetic_tactic

Required by 2 files of the paper proofs

For c > -1 and real n x n matrices H and S, let trace_quad c H S = 2 <H, S> - |S|_F^2 - (c / n) (tr S)^2, with the Frobenius product <., .> and norm |.|_F of matrix/euclidean.v. With A = trace_scale c, that is A S = S + (c / n) tr(S) I, the quadratic part is <S, A S> = |S|_F^2 + (c / n) (tr S)^2. Since (tr S)^2 <= n |S|_F^2, it is coercive: <S, A S> >= min(1, 1 + c) |S|_F^2. So trace_quad c H is strictly concave, and it has a unique maximizer X(H) on every nonempty closed convex set K of matrices. Since trace_quad c H S = <H, A^-1 H> - <S - A^-1 H, A (S - A^-1 H)>, X(H) is the nearest point of K to A^-1 H = H - (c / (1 + c)) (tr H / n) I for the scalar product <S, A T> = <S, T> + (c / n) tr S tr T, with A^-1 = trace_scale (- c / (1 + c)). It is not the nearest point of K to H: for K the whole space, X(H) = A^-1 H. X(H) is computed by the projection of convex/moreau.v. U = trace_scale (sqrt (1 + c) - 1) multiplies the component of a matrix along the identity by sqrt (1 + c) and fixes the matrices of trace 0; U U = A, and X(H) = U^-1 Pi_{U K}(U^-1 H), with Pi_{U K} the Frobenius projection onto U K. The definition applies U^-1 = trace_scale (1 / sqrt (1 + c) - 1) to H, projects onto U K in the coordinates of mxvec, and applies U^-1 to the result.

In what follows, K is a set of n x n matrices that is closed in the coordinates of mxvec, convex and nonempty, c > -1 and X = trace_argmax K c H.

trace_scale a SS + a (tr S / n) I
trace_quad c H S2 <H, S> - |S|_F^2 - (c / n) (tr S)^2
trace_argmax K c Hthe maximizer of trace_quad c H on K

Main results

ResultsStatement
trace_scaletrace_scaleKtrace_scale_adjmxtrace_scalemxtrace_sqr_letrace_pen_getrace_quad_expand
trace_scale a S = S + a (tr S / n) I multiplies the component of S along the identity by 1 + a: trace_scale a (trace_scale b S) = trace_scale ((1 + a) (1 + b) - 1) S, it is self-adjoint for the Frobenius product, and tr (trace_scale a S) = (1 + a) tr S. (tr S)^2 / n <= |S|_F^2, so |S|_F^2 + (c / n) (tr S)^2 >= min(1, 1 + c) |S|_F^2 for every real c. trace_quad c H S = 2 <H, S> - |S|_F^2 - (c / n) (tr S)^2 has an exact second-order expansion at every X.
trace_argmaxtrace_argmaxPtrace_argmax_eqtrace_argmax_getrace_argmax_unique
For c > -1 and a nonempty convex set K of n x n matrices, closed in the coordinates of mxvec, trace_quad c H has a unique maximizer X = trace_argmax K c H on K. X is the only point of K with <H - X - (c / n) tr(X) I, S - X> <= 0 for every S in K, and trace_quad c H S + min(1, 1 + c) |S - X|_F^2 <= trace_quad c H X for S in K. Proved by the projection of convex/moreau.v after trace_scale (sqrt (1 + c) - 1), which turns the quadratic part into |.|_F^2.
trace_argmax_lipschitztrace_argmax0trace_argmax_normtrace_argmax_conetrace_argmax_conj
With the same hypotheses, |X(H) - X(H')|_F <= |H - H'|_F / min(1, 1 + c). If 0 is in K, then X(0) = 0 and |X(H)|_F <= |H|_F / min(1, 1 + c). If K is a cone, then <H, X> = |X|_F^2 + (c / n) (tr X)^2 = trace_quad c H X. If K is invariant under the conjugations S |-> P S P^T by orthogonal matrices, then X(Q H Q^T) = Q X(H) Q^T for every orthogonal Q.

Declarations31 exported, 11 local

lemma, theoremdefinitioninstancelocal
sectiontrace_facts
Context {R : realType}.
lemma mxdot1l source, line 84 
forall {R : realType} [n : nat] (A : 'M_n), mxdot 1%:M A = \tr A
Statement as written in the source
Lemma mxdot1l n (A : 'M[R]_n) : mxdot 1%:M A = \tr A.
Used by 3 declarations in 1 file
lemma mxtrace_divK source, line 87 
forall {R : realType} [n : nat] (A : 'M_n), \tr A / n%:R * n%:R = \tr A
Statement as written in the source
Lemma mxtrace_divK n (A : 'M[R]_n) : \tr A / n%:R * n%:R = \tr A.
Used by 1 declaration in 1 file
lemma mxtrace_sqr_le main result source, line 94 
forall {R : realType} [n : nat] (A : 'M_n), \tr A ^+ 2 / n%:R <= mxdot A A

Cauchy-Schwarz for the Frobenius product with the identity.

Main result

Stated in the README together with trace_scale.

Statement as written in the source
Lemma mxtrace_sqr_le n (A : 'M[R]_n) : \tr A ^+ 2 / n%:R <= mxdot A A.
Used by 1 declaration in 1 file
lemma trace_pen_ge main result source, line 102 
forall {R : realType} [n : nat] (c : R) (A : 'M_n),
minr 1 (1 + c) * mxdot A A <= mxdot A A + c / n%:R * \tr A ^+ 2

The coercivity of the quadratic part, for every real c.

Main result

Stated in the README together with trace_scale.

Statement as written in the source
Lemma trace_pen_ge n (c : R) (A : 'M[R]_n) :
  Num.min 1 (1 + c) * mxdot A A <= mxdot A A + c / n%:R * \tr A ^+ 2.
Used by 2 declarations in 1 file
lemma mxtraceB source, line 116 
forall {R : realType} [n : nat] (A B : 'M_n), \tr (A - B) = \tr A - \tr B
Statement as written in the source
Lemma mxtraceB n (A B : 'M[R]_n) : \tr (A - B) = \tr A - \tr B.
Used by 2 declarations in 1 file
lemma mxdot_conjmx source, line 119 
forall {R : realType} [n : nat] [Q : 'M_n] (A B : 'M_n),
Q \is orthogonalmx -> mxdot (Q *m A *m Q^T) (Q *m B *m Q^T) = mxdot A B
Statement as written in the source
Lemma mxdot_conjmx n (Q A B : 'M[R]_n) : Q \is orthogonalmx ->
  mxdot (Q *m A *m Q^T) (Q *m B *m Q^T) = mxdot A B.
Used by 1 declaration in 1 file
lemma mxtrace_conj source, line 126 
forall {R : realType} [n : nat] [Q : 'M_n] (A : 'M_n),
Q \is orthogonalmx -> \tr (Q *m A *m Q^T) = \tr A
Statement as written in the source
Lemma mxtrace_conj n (Q A : 'M[R]_n) : Q \is orthogonalmx ->
  \tr (Q *m A *m Q^T) = \tr A.
Used by 1 declaration in 1 file
sectiontrace_scale
Context {R : realType} {n : nat}.
Implicit Types (a b c k : R) (H S T X : 'M[R]_n).
definition trace_scale main result source, line 137
Type
forall {R : realType} {n : nat}, R -> 'M_n -> 'M_n
Definition
Definition trace_scale a S : 'M[R]_n := S + (a * (\tr S / n%:R)) *: 1%:M.

Multiplies the component of S along the identity by 1 + a.

Main result, as the README states it

trace_scale a S = S + a (tr S / n) I multiplies the component of S along the identity by 1 + a: trace_scale a (trace_scale b S) = trace_scale ((1 + a) (1 + b) - 1) S, it is self-adjoint for the Frobenius product, and tr (trace_scale a S) = (1 + a) tr S. (tr S)^2 / n <= |S|_F^2, so |S|_F^2 + (c / n) (tr S)^2 >= min(1, 1 + c) |S|_F^2 for every real c. trace_quad c H S = 2 <H, S> - |S|_F^2 - (c / n) (tr S)^2 has an exact second-order expansion at every X.

Used by 25 declarations in 1 file
definition trace_quad source, line 139
Type
forall {R : realType} {n : nat}, R -> 'M_n -> 'M_n -> R
Definition
Definition trace_quad c H S : R :=
  2 * mxdot H S - mxdot S S - c / n%:R * \tr S ^+ 2.
Used by 4 declarations in 1 file
definition trace_argmax main result source, line 142
Type
forall {R : realType} {n : nat}, set 'M_n -> R -> 'M_n -> 'M_n
Definition
Definition trace_argmax (K : set 'M[R]_n) c H : 'M[R]_n :=
  trace_scale ((Num.sqrt (1 + c))^-1 - 1) (vec_mx (proj
    [set v | K (trace_scale ((Num.sqrt (1 + c))^-1 - 1) (vec_mx v))]
    (mxvec (trace_scale ((Num.sqrt (1 + c))^-1 - 1) H)))).
Main result, as the README states it

For c > -1 and a nonempty convex set K of n x n matrices, closed in the coordinates of mxvec, trace_quad c H has a unique maximizer X = trace_argmax K c H on K. X is the only point of K with <H - X - (c / n) tr(X) I, S - X> <= 0 for every S in K, and trace_quad c H S + min(1, 1 + c) |S - X|_F^2 <= trace_quad c H X for S in K. Proved by the projection of convex/moreau.v after trace_scale (sqrt (1 + c) - 1), which turns the quadratic part into |.|_F^2.

Used by 9 declarations in 1 file
lemma trace_scaleD source, line 147 
forall {R : realType} {n : nat} (a : R) (S T : 'M_n),
trace_scale a (S + T) = trace_scale a S + trace_scale a T
Statement as written in the source
Lemma trace_scaleD a S T :
  trace_scale a (S + T) = trace_scale a S + trace_scale a T.
Used by 2 declarations in 1 file
lemma trace_scaleZ source, line 151 
forall {R : realType} {n : nat} (a k : R) (S : 'M_n),
trace_scale a (k *: S) = k *: trace_scale a S
Statement as written in the source
Lemma trace_scaleZ a k S : trace_scale a (k *: S) = k *: trace_scale a S.
Used by 2 declarations in 1 file
lemma trace_scaleN source, line 157 
forall {R : realType} {n : nat} (a : R) (S : 'M_n), trace_scale a (- S) = - trace_scale a S
Statement as written in the source
Lemma trace_scaleN a S : trace_scale a (- S) = - trace_scale a S.
Used by 1 declaration in 1 file
lemma trace_scaleB source, line 160 
forall {R : realType} {n : nat} (a : R) (S T : 'M_n),
trace_scale a (S - T) = trace_scale a S - trace_scale a T
Statement as written in the source
Lemma trace_scaleB a S T :
  trace_scale a (S - T) = trace_scale a S - trace_scale a T.
Used by 2 declarations in 1 file
lemma trace_scale0 source, line 164 
forall {R : realType} {n : nat} (a : R), trace_scale a 0 = 0
Statement as written in the source
Lemma trace_scale0 a : trace_scale a 0 = 0.
Used by 1 declaration in 1 file
lemma trace_scale_id source, line 167 
forall {R : realType} {n : nat} (S : 'M_n), trace_scale 0 S = S
Statement as written in the source
Lemma trace_scale_id S : trace_scale 0 S = S.
Used by 2 declarations in 1 file
lemma mxtrace_scale main result source, line 170 
forall {R : realType} {n : nat} (a : R) (S : 'M_n), \tr (trace_scale a S) = (1 + a) * \tr S
Main result

Stated in the README together with trace_scale.

Statement as written in the source
Lemma mxtrace_scale a S : \tr (trace_scale a S) = (1 + a) * \tr S.
Used by 1 declaration in 1 file
lemma trace_scaleK main result source, line 176 
forall {R : realType} {n : nat} (a b : R) (S : 'M_n),
trace_scale a (trace_scale b S) = trace_scale ((1 + a) * (1 + b) - 1) S
Main result

Stated in the README together with trace_scale.

Statement as written in the source
Lemma trace_scaleK a b S :
  trace_scale a (trace_scale b S) = trace_scale ((1 + a) * (1 + b) - 1) S.
Used by 3 declarations in 1 file
lemma mxdot_trace_scalel source, line 183 
forall {R : realType} {n : nat} (a : R) (S T : 'M_n),
mxdot (trace_scale a S) T = mxdot S T + a / n%:R * (\tr S * \tr T)
Statement as written in the source
Lemma mxdot_trace_scalel a S T :
  mxdot (trace_scale a S) T = mxdot S T + a / n%:R * (\tr S * \tr T).
Used by 4 declarations in 1 file
lemma trace_scale_adj main result source, line 187 
forall {R : realType} {n : nat} (a : R) (S T : 'M_n),
mxdot (trace_scale a S) T = mxdot S (trace_scale a T)
Main result

Stated in the README together with trace_scale.

Statement as written in the source
Lemma trace_scale_adj a S T :
  mxdot (trace_scale a S) T = mxdot S (trace_scale a T).
Used by 1 declaration in 1 file
lemma trace_scale_conj source, line 194 
forall {R : realType} {n : nat} (a : R) [Q : 'M_n] (S : 'M_n),
Q \is orthogonalmx -> trace_scale a (Q *m S *m Q^T) = Q *m trace_scale a S *m Q^T
Statement as written in the source
Lemma trace_scale_conj a Q S : Q \is orthogonalmx ->
  trace_scale a (Q *m S *m Q^T) = Q *m trace_scale a S *m Q^T.
Used by 1 declaration in 1 file
lemma trace_quad_expand main result source, line 202 
forall {R : realType} {n : nat} (c : R) (H S0 X : 'M_n),
trace_quad c H S0 =
trace_quad c H X + 2 * mxdot (H - trace_scale c X) (S0 - X) -
(mxdot (S0 - X) (S0 - X) + c / n%:R * \tr (S0 - X) ^+ 2)

The second-order expansion of trace_quad c H at X.

Main result

Stated in the README together with trace_scale.

Statement as written in the source
Lemma trace_quad_expand c H S X :
  trace_quad c H S = trace_quad c H X +
    2 * mxdot (H - trace_scale c X) (S - X) -
    (mxdot (S - X) (S - X) + c / n%:R * \tr (S - X) ^+ 2).
Used by 1 declaration in 1 file
sectiontrace_argmax
Context {R : realType} {n : nat}.
Variable K : set 'M[R]_n.
Hypothesis Kc : closed [set v : 'rV[R]_(n * n) | K (vec_mx v)].
Hypothesis Kn : K !=set0.
Hypothesis Kcvx : forall (S T : 'M[R]_n) (t : R), K S -> K T -> 0 <= t <= 1 ->
  K (S + t *: (T - S)).
Variable c : R.
Hypothesis c1 : -1 < c.
Implicit Types (H S T X Y : 'M[R]_n).
Local Notation sc := (Num.sqrt (1 + c)).
Local Notation Uc := (trace_scale (sc - 1)).
Local Notation Vc := (trace_scale (sc^-1 - 1)).
Local Notation KU := [set v : 'rV[R]_(n * n) | K (Vc (vec_mx v))].
Local Notation Mv := (1%:M + ((sc^-1 - 1) / n%:R) *:
  ((mxvec (1%:M : 'M[R]_n))^T *m mxvec (1%:M : 'M[R]_n))).
let sc_gt0 section-local source, line 231 
Let sc_gt0 : 0 < sc.
Used by 2 declarations in 1 file
let UV section-local source, line 234 
Let UV S : Uc (Vc S) = S.
Used by 3 declarations in 1 file
let VU section-local source, line 242 
Let VU S : Vc (Uc S) = S.
Used by 3 declarations in 1 file
let UU section-local source, line 250 
Let UU S : Uc (Uc S) = trace_scale c S.
Used by 1 declaration in 1 file
let mxdot_vecE section-local source, line 257 
Let mxdot_vecE (A B : 'M[R]_n) : mxdot (mxvec A) (mxvec B) = mxdot A B.
Used by 2 declarations in 1 file
let mxtrace_vec_mx section-local source, line 265 
Let mxtrace_vec_mx (v : 'rV[R]_(n * n)) :
  \tr (vec_mx v) = mxdot v (mxvec 1%:M).
Used by 1 declaration in 1 file
let Vvec section-local source, line 270 
Let Vvec (v : 'rV[R]_(n * n)) : mxvec (Vc (vec_mx v)) = v *m Mv.

In the coordinates of mxvec, Vc is the right multiplication by Mv.

Used by 1 declaration in 1 file
let KU_closed section-local source, line 277 
Let KU_closed : closed KU.
Used by 2 declarations in 1 file
let KU_n0 section-local source, line 284 
Let KU_n0 : KU !=set0.
Used by 2 declarations in 1 file
let KU_convex section-local source, line 287 
Let KU_convex (x y : 'rV[R]_(n * n)) (t : R) : KU x -> KU y -> 0 <= t <= 1 ->
  KU (x + t *: (y - x)).
Used by 2 declarations in 1 file
let vi_transfer section-local source, line 295 
Let vi_transfer H X S :
  mxdot (mxvec (Vc H) - mxvec (Uc X)) (mxvec (Uc S) - mxvec (Uc X)) =
  mxdot (H - trace_scale c X) (S - X).

The variational inequality of the projection, read on matrices.

Used by 2 declarations in 1 file
theorem trace_argmaxP main result source, line 308 
forall {R : realType} {n : nat} [K : set 'M_n],
closed [set v | K (vec_mx v)] ->
K !=set0 ->
(forall (S T : 'M_n) (t : R), K S -> K T -> 0 <= t <= 1 -> K (S + t *: (T - S))) ->
forall [c : R],
-1 < c ->
forall H : 'M_n,
K (trace_argmax K c H) /\
(forall S : 'M_n,
 K S -> mxdot (H - trace_scale c (trace_argmax K c H)) (S - trace_argmax K c H) <= 0)

The maximizer is in K and satisfies the variational inequality <H - X - (c / n) tr(X) I, S - X> <= 0 for every S in K.

Main result

Stated in the README together with trace_argmax.

Statement as written in the source
Theorem trace_argmaxP H : K (trace_argmax K c H) /\
  forall S, K S ->
    mxdot (H - trace_scale c (trace_argmax K c H)) (S - trace_argmax K c H)
      <= 0.
Used by 5 declarations in 1 file
lemma trace_argmax_eq main result source, line 322 
forall {R : realType} {n : nat} [K : set 'M_n],
closed [set v | K (vec_mx v)] ->
K !=set0 ->
(forall (S T : 'M_n) (t : R), K S -> K T -> 0 <= t <= 1 -> K (S + t *: (T - S))) ->
forall [c : R],
-1 < c ->
forall [H Y : 'M_n],
K Y ->
(forall S : 'M_n, K S -> mxdot (H - trace_scale c Y) (S - Y) <= 0) ->
trace_argmax K c H = Y

The variational inequality characterizes the maximizer.

Main result

Stated in the README together with trace_argmax.

Statement as written in the source
Lemma trace_argmax_eq H Y : K Y ->
  (forall S, K S -> mxdot (H - trace_scale c Y) (S - Y) <= 0) ->
  trace_argmax K c H = Y.
Used by 2 declarations in 1 file
lemma trace_argmax_ge main result source, line 338 
forall {R : realType} {n : nat} [K : set 'M_n],
closed [set v | K (vec_mx v)] ->
K !=set0 ->
(forall (S T : 'M_n) (t : R), K S -> K T -> 0 <= t <= 1 -> K (S + t *: (T - S))) ->
forall [c : R],
-1 < c ->
forall (H : 'M_n) [S : 'M_n],
K S ->
trace_quad c H S + minr 1 (1 + c) * mxdot (S - trace_argmax K c H) (S - trace_argmax K c H) <=
trace_quad c H (trace_argmax K c H)

The maximizer beats every point of K by min(1, 1 + c) |S - X|_F^2.

Main result

Stated in the README together with trace_argmax.

Statement as written in the source
Lemma trace_argmax_ge H S : K S ->
  trace_quad c H S + Num.min 1 (1 + c) *
    mxdot (S - trace_argmax K c H) (S - trace_argmax K c H) <=
  trace_quad c H (trace_argmax K c H).
Used by 1 declaration in 1 file
lemma trace_argmax_unique main result source, line 350 
forall {R : realType} {n : nat} [K : set 'M_n],
closed [set v | K (vec_mx v)] ->
K !=set0 ->
(forall (S T : 'M_n) (t : R), K S -> K T -> 0 <= t <= 1 -> K (S + t *: (T - S))) ->
forall [c : R],
-1 < c ->
forall [H Y : 'M_n],
K Y ->
(forall S : 'M_n, K S -> trace_quad c H S <= trace_quad c H Y) -> trace_argmax K c H = Y
Main result

Stated in the README together with trace_argmax.

Statement as written in the source
Lemma trace_argmax_unique H Y : K Y ->
  (forall S, K S -> trace_quad c H S <= trace_quad c H Y) ->
  trace_argmax K c H = Y.
lemma trace_argmax_lipschitz main result source, line 362 
forall {R : realType} {n : nat} [K : set 'M_n],
closed [set v | K (vec_mx v)] ->
K !=set0 ->
(forall (S T : 'M_n) (t : R), K S -> K T -> 0 <= t <= 1 -> K (S + t *: (T - S))) ->
forall [c : R],
-1 < c ->
forall H H' : 'M_n,
frobenius (trace_argmax K c H - trace_argmax K c H') <= frobenius (H - H') / minr 1 (1 + c)
Main result, as the README states it

With the same hypotheses, |X(H) - X(H')|_F <= |H - H'|_F / min(1, 1 + c). If 0 is in K, then X(0) = 0 and |X(H)|_F <= |H|_F / min(1, 1 + c). If K is a cone, then <H, X> = |X|_F^2 + (c / n) (tr X)^2 = trace_quad c H X. If K is invariant under the conjugations S |-> P S P^T by orthogonal matrices, then X(Q H Q^T) = Q X(H) Q^T for every orthogonal Q.

Statement as written in the source
Lemma trace_argmax_lipschitz H H' :
  frobenius (trace_argmax K c H - trace_argmax K c H') <=
  frobenius (H - H') / Num.min 1 (1 + c).
Used by 1 declaration in 1 file
lemma trace_argmax0 main result source, line 389 
forall {R : realType} {n : nat} [K : set 'M_n],
closed [set v | K (vec_mx v)] ->
K !=set0 ->
(forall (S T : 'M_n) (t : R), K S -> K T -> 0 <= t <= 1 -> K (S + t *: (T - S))) ->
forall [c : R], -1 < c -> K 0 -> trace_argmax K c 0 = 0
Main result

Stated in the README together with trace_argmax_lipschitz.

Statement as written in the source
Lemma trace_argmax0 : K 0 -> trace_argmax K c 0 = 0.
Used by 1 declaration in 1 file
lemma trace_argmax_norm main result source, line 395 
forall {R : realType} {n : nat} [K : set 'M_n],
closed [set v | K (vec_mx v)] ->
K !=set0 ->
(forall (S T : 'M_n) (t : R), K S -> K T -> 0 <= t <= 1 -> K (S + t *: (T - S))) ->
forall [c : R],
-1 < c ->
forall H : 'M_n, K 0 -> frobenius (trace_argmax K c H) <= frobenius H / minr 1 (1 + c)
Main result

Stated in the README together with trace_argmax_lipschitz.

Statement as written in the source
Lemma trace_argmax_norm H : K 0 ->
  frobenius (trace_argmax K c H) <= frobenius H / Num.min 1 (1 + c).
lemma trace_argmax_cone main result source, line 403 
forall {R : realType} {n : nat} [K : set 'M_n],
closed [set v | K (vec_mx v)] ->
K !=set0 ->
(forall (S T : 'M_n) (t : R), K S -> K T -> 0 <= t <= 1 -> K (S + t *: (T - S))) ->
forall [c : R],
-1 < c ->
forall H : 'M_n,
(forall (S : 'M_n) (k : R), K S -> 0 <= k -> K (k *: S)) ->
mxdot H (trace_argmax K c H) =
mxdot (trace_argmax K c H) (trace_argmax K c H) + c / n%:R * \tr (trace_argmax K c H) ^+ 2 /\
trace_quad c H (trace_argmax K c H) = mxdot H (trace_argmax K c H)

On a cone, the value of the maximum is <H, X>.

Main result

Stated in the README together with trace_argmax_lipschitz.

Statement as written in the source
Lemma trace_argmax_cone H :
  (forall S (k : R), K S -> 0 <= k -> K (k *: S)) ->
  mxdot H (trace_argmax K c H) =
    mxdot (trace_argmax K c H) (trace_argmax K c H) +
    c / n%:R * \tr (trace_argmax K c H) ^+ 2 /\
  trace_quad c H (trace_argmax K c H) = mxdot H (trace_argmax K c H).
lemma trace_argmax_conj main result source, line 426 
forall {R : realType} {n : nat} [K : set 'M_n],
closed [set v | K (vec_mx v)] ->
K !=set0 ->
(forall (S T : 'M_n) (t : R), K S -> K T -> 0 <= t <= 1 -> K (S + t *: (T - S))) ->
forall [c : R],
-1 < c ->
forall (H : 'M_n) [Q : 'M_n],
(forall P S : 'M_n, P \is orthogonalmx -> K S -> K (P *m S *m P^T)) ->
Q \is orthogonalmx -> trace_argmax K c (Q *m H *m Q^T) = Q *m trace_argmax K c H *m Q^T

Equivariance under the orthogonal conjugations, from uniqueness.

Main result

Stated in the README together with trace_argmax_lipschitz.

Statement as written in the source
Lemma trace_argmax_conj H Q :
  (forall P S, P \is orthogonalmx -> K S -> K (P *m S *m P^T)) ->
  Q \is orthogonalmx ->
  trace_argmax K c (Q *m H *m Q^T) = Q *m trace_argmax K c H *m Q^T.
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.