On this page

The cone of matrices of bounded condition number

GaussianAnalysis.matrix.condition_conelibrary/matrix/condition_cone.v785 lines47 lemmas and theorems, 10 definitionssource

Imports 8 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.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, mathcomp.algebra.arithmetic_tactic

Required by 13 files of the paper proofs

For C >= 1, cond_cone C is the set of the real symmetric n x n matrices Q with t I <= Q <= C t I for some t >= 0: the positive semidefinite matrices of condition number at most C, and 0. It is a closed convex cone. Its distance to a symmetric matrix H and its support function are computed from the spectrum of H: the nearest point of the cone clips the eigenvalues of H to an interval [t, C t] (Tanaka and Nakata, Optim. Lett. 8 (2014)). The optimal t is not needed in closed form: the distance is an infimum over t >= 0 of a sum over the eigenvalues, which is what a limit theorem for random spectra can handle.

itv_dist a b x, clamp a b x: the distance from x to [a, b] and the nearest point; itv_dist_clamp, itv_dist_le (the distance to any point of [a, b] is larger), itv_dist_lipschitz (1-Lipschitz in x), itv_dist_shift (Lipschitz in the endpoints).
cond_coneP: for Q symmetric, Q is in the cone iff its eigenvalues lie in some [t, C t] with t >= 0; cond_cone_quad: for C >= 0, iff Q is symmetric, positive semidefinite and |y|^2 x^T Q x <= C |x|^2 y^T Q y for all x, y; cond_cone0, cond_cone1, cond_coneZ, cond_cone_convex.
cond_cone_vec C, the cone in the coordinates of mxvec: cond_cone_vec_closed, cond_cone_vec0, cond_cone_vec_convex, cond_cone_vecZ, the hypotheses of the cone projection of convex/moreau.v.
cond_cone_dist: for H symmetric and C >= 1, the squared Frobenius distance from H to the cone is cond_dist C H, the infimum over t >= 0 of cond_energy C t H = sum_i dist(lambda_i(H), [t, C t])^2. cond_energy_le (Hoffman-Wielandt) gives the lower bound, cond_clip and cond_clip_energy (the eigenvalues of H clipped to [t, C t]) the upper bound.
cond_support C A, the supremum of <A, Q> over the Q of the cone with |Q|_F <= 1: cond_support_proj, it is the norm of the projection of A onto the cone; cond_support_sqr, for H symmetric and C >= 1, cond_support C H ^ 2 = |H|_F^2 - cond_dist C H (Moreau's decomposition); cond_support_sym, only the symmetric part of A matters; cond_supportZ, cond_energyZ, cond_distZ, the scalings.
cond_energy_mono, cond_dist_itv: when the eigenvalues of H are at most T >= 0, the energy increases on [T, oo) and the infimum may be taken over [0, T].
cond_slice C, the trace slice {Q in the cone | tr Q = n}, a compact convex base of the cone: cond_slice1, cond_slice_spec (eigenvalues in [1/C, C]), cond_slice_t (between t I and C t I with t in [1/C, 1]), cond_slice_form, cond_slice_frobenius (n <= |Q|_F^2 <= C n), cond_cone_slice (every nonzero point of the cone has a positive multiple in the slice); cond_slice_vec, the slice in the coordinates of mxvec: cond_slice_vec_closed, cond_slice_vec_convex, cond_slice_vec_frobenius, cond_cone_vec_slice.

`itv_dist a b x`	the distance from x to the interval [a, b]
`clamp a b x`	the nearest point of [a, b] to x
`cond_cone C`	the symmetric Q with t I <= Q <= C t I, some t >= 0
`cond_cone_vec C`	the same cone in the coordinates of mxvec
`cond_energy C t H`	sum_i itv_dist t (C t) (spec H 0 i) ^ 2
`cond_dist C H`	the infimum of cond_energy C t H over t >= 0
`cond_clip C t H`	H with its eigenvalues clipped to [t, C t]
`cond_support C A`	sup of <A, Q> over the Q of the cone with \|Q\|_F <= 1
`cond_slice C`	the Q of the cone with trace n
`cond_slice_vec C`	the same slice in the coordinates of mxvec

Main results

Results	Statement
cond_conecond_conePcond_cone_quadcond_cone_vec_closedcond_cone_vec_convexcond_cone_vecZ	`cond_cone C` is the set of the symmetric `Q` with `t I <= Q <= C t I` for some `t >= 0`: the positive semidefinite matrices of condition number at most `C`, and `0`. A symmetric `Q` is in it iff its eigenvalues lie in some `[t, C t]` with `t >= 0`; for `C >= 0`, iff `Q` is positive semidefinite with `\|y\|^2 x^T Q x <= C \|x\|^2 y^T Q y` for all `x`, `y`. In the coordinates of `mxvec` it is a closed convex cone, as the cone projection of `convex/moreau.v` asks.
cond_cone_distcond_support_sqrcond_support_projcond_support_symcond_supportZcond_dist_itv	For `C >= 1` and `H` symmetric, the squared Frobenius distance from `H` to `cond_cone C` is `cond_dist C H`, the infimum over `t >= 0` of `sum_i dist(lambda_i(H), [t, C t])^2`: the lower bound by Hoffman-Wielandt, the upper bound by clipping the eigenvalues of `H` to `[t, C t]` (Tanaka and Nakata). The support function, the supremum of `<H, Q>` over the `Q` of the cone with `\|Q\|_F <= 1`, is the norm of the projection of `H` onto the cone, and its square is `\|H\|_F^2 - cond_dist C H` (Moreau's decomposition). Only the symmetric part of a matrix matters, the support function and `cond_dist` scale, and when the eigenvalues of `H` are at most `T >= 0` the infimum over `t` may be taken over `[0, T]`.
cond_slice_tcond_slice_speccond_slice_frobeniuscond_cone_slicecond_slice_vec_closedcond_slice_vec_convexcond_cone_vec_slice	The trace slice `{Q in cond_cone C : tr Q = n}` is a closed convex base of the cone: for `C > 0` and `n >= 1` its matrices satisfy `t I <= Q <= C t I` for some `t` in `[1/C, 1]`, have eigenvalues in `[1/C, C]` and `n <= \|Q\|_F^2 <= C n`, and every nonzero point of the cone has a positive multiple in it.

Declarations57 exported

sectioninterval_distance

Variable R : realType.
Implicit Types a b x y : R.

definition itv_dist source, line 89

Type

forall [R : realType], R -> R -> R -> R

Definition

Definition itv_dist a b x : R := Num.max (a - x) 0 + Num.max (x - b) 0.

The distance from x to the interval [a, b], for a <= b.

Used by 9 declarations in 1 file

this file: itv_dist_ge0, itv_dist_clamp, itv_dist_le, itv_dist_lipschitz, itv_dist_shift, cond_energy, cond_clip_energy, cond_energyZ, cond_energy_mono

definition clamp source, line 92

Type

forall [R : realType], R -> R -> R -> R

Definition

Definition clamp a b x : R := Num.max a (Num.min b x).

The nearest point of [a, b] to x, for a <= b.

Used by 6 declarations in 1 file

this file: clamp_itv, itv_dist_clamp, itv_dist_lipschitz, cond_clip, cond_clip_cone, cond_clip_energy

lemma itv_dist_ge0 source, line 94

forall [R : realType] (a b x : R), 0 <= itv_dist a b x

Statement as written in the source

Lemma itv_dist_ge0 a b x : 0 <= itv_dist a b x.

Used by 1 declaration in 1 file

this file: cond_energy_le

lemma clamp_itv source, line 97

forall [R : realType] [a b : R] (x : R), a <= b -> a <= clamp a b x <= b

Statement as written in the source

Lemma clamp_itv a b x : a <= b -> a <= clamp a b x <= b.

Used by 2 declarations in 1 file

this file: itv_dist_lipschitz, cond_clip_cone

lemma itv_dist_clamp source, line 100

forall [R : realType] [a b : R] (x : R), a <= b -> itv_dist a b x = `|x - clamp a b x|

Statement as written in the source

Lemma itv_dist_clamp a b x : a <= b -> itv_dist a b x = `|x - clamp a b x|.

Used by 2 declarations in 1 file

this file: itv_dist_lipschitz, cond_clip_energy

lemma itv_dist_le source, line 112

forall [R : realType] [a b : R] (x : R) [y : R], a <= y <= b -> itv_dist a b x <= `|x - y|

Statement as written in the source

Lemma itv_dist_le a b x y : a <= y <= b -> itv_dist a b x <= `|x - y|.

Used by 2 declarations in 1 file

this file: itv_dist_lipschitz, cond_energy_le

lemma itv_dist_lipschitz source, line 124

forall [R : realType] [a b : R] (x y : R),
a <= b -> `|itv_dist a b x - itv_dist a b y| <= `|x - y|

Statement as written in the source

Lemma itv_dist_lipschitz a b x y : a <= b ->
  `|itv_dist a b x - itv_dist a b y| <= `|x - y|.

lemma itv_dist_shift source, line 139

forall [R : realType] (a b a' b' x : R),
`|itv_dist a b x - itv_dist a' b' x| <= `|a - a'| + `|b - b'|

Statement as written in the source

Lemma itv_dist_shift a b a' b' x :
  `|itv_dist a b x - itv_dist a' b' x| <= `|a - a'| + `|b - b'|.

sectioncondition_cone

Variable R : realType.
Variable n : nat.
Implicit Types (A H Q : 'M[R]_n) (C t : R).

definition cond_cone main result source, line 169

Type

forall [R : realType] [n : nat], R -> set 'M_n

Definition

Definition cond_cone C : set 'M[R]_n :=
  [set Q | Q \is symmetricmx /\ exists2 t : R, 0 <= t &
     forall x : 'cV[R]_n,
       t * mxdot x x <= mxdot x (Q *m x) <= C * t * mxdot x x].

The cone of the symmetric matrices Q with t I <= Q <= C t I for some t >= 0: the positive semidefinite matrices of condition number at most C, and 0.

Main result, as the README states it

cond_cone C is the set of the symmetric Q with t I <= Q <= C t I for some t >= 0: the positive semidefinite matrices of condition number at most C, and 0. A symmetric Q is in it iff its eigenvalues lie in some [t, C t] with t >= 0; for C >= 0, iff Q is positive semidefinite with |y|^2 x^T Q x <= C |x|^2 y^T Q y for all x, y. In the coordinates of mxvec it is a closed convex cone, as the cone projection of convex/moreau.v asks.

Used by 13 declarations in 1 file

this file: cond_coneP, cond_cone0, cond_cone1, cond_coneZ, cond_cone_convex, cond_cone_quad, cond_cone_vec, cond_clip_cone, cond_energy_le, cond_cone_dist, cond_support, cond_slice, cond_cone_slice

lemma cond_coneP main result source, line 174

forall [R : realType] [n : nat] (C : R) [Q : 'M_n],
Q \is symmetricmx ->
cond_cone C Q <-> (exists2 t : R, 0 <= t & forall i : 'I_n, t <= spec Q 0 i <= C * t)

Main result

Stated in the README together with cond_cone.

Statement as written in the source

Lemma cond_coneP C Q : Q \is symmetricmx ->
  cond_cone C Q <-> exists2 t : R, 0 <= t & forall i, t <= spec Q 0 i <= C * t.

Used by 5 declarations in 1 file

this file: cond_cone_quad, cond_energy_le, cond_slice_t, cond_slice_spec, cond_cone_slice

lemma cond_cone0 source, line 187

forall [R : realType] (n : nat) (C : R), cond_cone C 0

Statement as written in the source

Lemma cond_cone0 C : cond_cone C 0.

Used by 2 declarations in 1 file

this file: cond_cone_vec0, cond_cone_dist

lemma cond_cone1 source, line 193

forall [R : realType] (n : nat) [C : R], 1 <= C -> cond_cone C 1%:M

Statement as written in the source

Lemma cond_cone1 C : 1 <= C -> cond_cone C 1%:M.

Used by 1 declaration in 1 file

this file: cond_slice1

lemma cond_coneZ source, line 200

forall [R : realType] [n : nat] [C a : R] [Q : 'M_n],
0 <= a -> cond_cone C Q -> cond_cone C (a *: Q)

Statement as written in the source

Lemma cond_coneZ C (a : R) Q : 0 <= a -> cond_cone C Q -> cond_cone C (a *: Q).

Used by 2 declarations in 1 file

this file: cond_cone_vecZ, cond_cone_slice

lemma cond_cone_convex source, line 210

forall [R : realType] [n : nat] [C : R] [Q1 Q2 : 'M_n] [s : R],
cond_cone C Q1 -> cond_cone C Q2 -> 0 <= s <= 1 -> cond_cone C (Q1 + s *: (Q2 - Q1))

Statement as written in the source

Lemma cond_cone_convex C Q1 Q2 (s : R) : cond_cone C Q1 -> cond_cone C Q2 ->
  0 <= s <= 1 -> cond_cone C (Q1 + s *: (Q2 - Q1)).

Used by 1 declaration in 1 file

this file: cond_cone_vec_convex

lemma cond_cone_quad main result source, line 230

forall [R : realType] [n : nat] [C : R] (Q : 'M_n),
0 <= C ->
cond_cone C Q <->
[/\ Q \is symmetricmx, forall x : 'cV_n, 0 <= mxdot x (Q *m x)
  & forall x y : 'cV_n, mxdot y y * mxdot x (Q *m x) <= C * mxdot x x * mxdot y (Q *m y)]

Main result

Stated in the README together with cond_cone.

Statement as written in the source

Lemma cond_cone_quad C Q : 0 <= C ->
  cond_cone C Q <-> [/\ Q \is symmetricmx,
    forall x : 'cV[R]_n, 0 <= mxdot x (Q *m x) &
    forall x y : 'cV[R]_n,
      mxdot y y * mxdot x (Q *m x) <= C * mxdot x x * mxdot y (Q *m y)].

Used by 1 declaration in 1 file

this file: cond_cone_vec_closed

definition cond_cone_vec source, line 269

Type

forall [R : realType] [n : nat], R -> set 'rV_(n * n)

Definition

Definition cond_cone_vec C : set 'rV[R]_(n * n) :=
  [set v | cond_cone C (vec_mx v)].

The cone in the coordinates of mxvec, where moreau.v applies.

Used by 10 declarations in 1 file

this file: cond_cone_vec_closed, cond_cone_vec0, cond_cone_vec_convex, cond_cone_vecZ, cond_support_vec, cond_support_proj, cond_support_sqr, cond_supportZ, cond_slice_vec_closed, cond_cone_vec_slice

lemma mxdot_quad_vec source, line 272

forall [R : realType] [n : nat] (x : 'cV_n) (v : 'rV_(n * n)),
mxdot x (vec_mx v *m x) = mxdot v (mxvec (x *m x^T))

Statement as written in the source

Lemma mxdot_quad_vec (x : 'cV[R]_n) (v : 'rV[R]_(n * n)) :
  mxdot x (vec_mx v *m x) = mxdot v (mxvec (x *m x^T)).

Used by 1 declaration in 1 file

this file: cond_cone_vec_closed

lemma continuous_mxdotv source, line 278

forall [R : realType] [n : nat] [c : 'rV_(n * n)], continuous ((mxdot (n:=n * n))^~ c)

Statement as written in the source

Lemma continuous_mxdotv (c : 'rV[R]_(n * n)) :
  continuous (fun v : 'rV[R]_(n * n) => mxdot v c).

Used by 2 declarations in 1 file

this file: cond_cone_vec_closed, cond_slice_vec_closed

lemma cond_cone_vec_closed main result source, line 288

forall [R : realType] [n : nat] [C : R], 0 <= C -> closed (cond_cone_vec C)

Main result

Stated in the README together with cond_cone.

Statement as written in the source

Lemma cond_cone_vec_closed C : 0 <= C -> closed (cond_cone_vec C).

Used by 4 declarations in 1 file

this file: cond_support_proj, cond_support_sqr, cond_supportZ, cond_slice_vec_closed

lemma cond_cone_vec0 source, line 332

forall [R : realType] (n : nat) (C : R), cond_cone_vec C 0

Statement as written in the source

Lemma cond_cone_vec0 C : cond_cone_vec C 0.

Used by 3 declarations in 1 file

this file: cond_support_proj, cond_support_sqr, cond_supportZ

lemma cond_cone_vec_convex main result source, line 335

forall [R : realType] [n : nat] [C : R] [x y : 'rV_(n * n)] [s : R],
cond_cone_vec C x -> cond_cone_vec C y -> 0 <= s <= 1 -> cond_cone_vec C (x + s *: (y - x))

Main result

Stated in the README together with cond_cone.

Statement as written in the source

Lemma cond_cone_vec_convex C (x y : 'rV[R]_(n * n)) (s : R) :
  cond_cone_vec C x -> cond_cone_vec C y -> 0 <= s <= 1 ->
  cond_cone_vec C (x + s *: (y - x)).

Used by 4 declarations in 1 file

this file: cond_support_proj, cond_support_sqr, cond_supportZ, cond_slice_vec_convex

lemma cond_cone_vecZ main result source, line 343

forall [R : realType] [n : nat] [C : R] [y : 'rV_(n * n)] [a : R],
cond_cone_vec C y -> 0 <= a -> cond_cone_vec C (a *: y)

Main result

Stated in the README together with cond_cone.

Statement as written in the source

Lemma cond_cone_vecZ C (y : 'rV[R]_(n * n)) (a : R) :
  cond_cone_vec C y -> 0 <= a -> cond_cone_vec C (a *: y).

Used by 3 declarations in 1 file

this file: cond_support_proj, cond_support_sqr, cond_supportZ

definition cond_energy source, line 351

Type

forall [R : realType] [n : nat], R -> R -> 'M_n -> R

Definition

Definition cond_energy C t H : R :=
  \sum_i itv_dist t (C * t) (spec H 0 i) ^+ 2.

The energy of t: the squared distances from the eigenvalues of H to the interval [t, C t], summed.

Used by 9 declarations in 1 file

this file: cond_dist, cond_energy_ge0, cond_dist_le, cond_dist_ge, cond_clip_energy, cond_energy_le, cond_energyZ, cond_energy_mono, cond_dist_itv

definition cond_dist source, line 356

Type

forall [R : realType] [n : nat], R -> 'M_n -> R

Definition

Definition cond_dist C H : R :=
  inf [set cond_energy C t H | t in [set t : R | 0 <= t]].

Its infimum over t >= 0, the squared distance from H to cond_cone C (cond_cone_dist).

Used by 7 declarations in 1 file

this file: cond_dist_le, cond_dist_ge, cond_dist_ge0, cond_cone_dist, cond_support_sqr, cond_distZ, cond_dist_itv

definition cond_clip source, line 360

Type

forall [R : realType] [n : nat], R -> R -> 'M_n -> 'M_n

Definition

Definition cond_clip C t H : 'M[R]_n :=
  (sym_spectralmx H)^T *m
  diag_mx (\row_i clamp t (C * t) (sym_spectral_diag H 0 i)) *m
  sym_spectralmx H.

The matrix H with its eigenvalues clipped to [t, C t].

Used by 4 declarations in 1 file

this file: cond_clip_cone, cond_clip_energy, cond_cone_dist, cond_support_sqr

lemma cond_energy_ge0 source, line 365

forall [R : realType] [n : nat] (C t : R) (H : 'M_n), 0 <= cond_energy C t H

Statement as written in the source

Lemma cond_energy_ge0 C t H : 0 <= cond_energy C t H.

Used by 3 declarations in 1 file

this file: cond_dist_le, cond_dist_ge0, cond_dist_itv

lemma cond_dist_le source, line 368

forall [R : realType] [n : nat] (C : R) [t : R] (H : 'M_n),
0 <= t -> cond_dist C H <= cond_energy C t H

Statement as written in the source

Lemma cond_dist_le C t H : 0 <= t -> cond_dist C H <= cond_energy C t H.

Used by 4 declarations in 1 file

this file: cond_cone_dist, cond_support_sqr, cond_distZ, cond_dist_itv

lemma cond_dist_ge source, line 374

forall [R : realType] [n : nat] [C : R] [H : 'M_n] [r : R],
(forall t : R, 0 <= t -> r <= cond_energy C t H) -> r <= cond_dist C H

Statement as written in the source

Lemma cond_dist_ge C H (r : R) :
  (forall t, 0 <= t -> r <= cond_energy C t H) -> r <= cond_dist C H.

Used by 5 declarations in 1 file

this file: cond_dist_ge0, cond_cone_dist, cond_support_sqr, cond_distZ, cond_dist_itv

lemma cond_dist_ge0 source, line 381

forall [R : realType] [n : nat] (C : R) (H : 'M_n), 0 <= cond_dist C H

Statement as written in the source

Lemma cond_dist_ge0 C H : 0 <= cond_dist C H.

lemma cond_clip_cone source, line 384

forall [R : realType] [n : nat] [C t : R] (H : 'M_n),
1 <= C -> 0 <= t -> cond_cone C (cond_clip C t H)

Statement as written in the source

Lemma cond_clip_cone C t H : 1 <= C -> 0 <= t -> cond_cone C (cond_clip C t H).

Used by 2 declarations in 1 file

this file: cond_cone_dist, cond_support_sqr

lemma cond_clip_energy source, line 400

forall [R : realType] [n : nat] [C t : R] [H : 'M_n],
1 <= C ->
0 <= t ->
H \is symmetricmx -> mxdot (H - cond_clip C t H) (H - cond_clip C t H) = cond_energy C t H

Statement as written in the source

Lemma cond_clip_energy C t H : 1 <= C -> 0 <= t -> H \is symmetricmx ->
  mxdot (H - cond_clip C t H) (H - cond_clip C t H) = cond_energy C t H.

Used by 2 declarations in 1 file

this file: cond_cone_dist, cond_support_sqr

lemma cond_energy_le source, line 416

forall [R : realType] [n : nat] [C : R] [H Q : 'M_n],
H \is symmetricmx ->
cond_cone C Q -> exists2 t : R, 0 <= t & cond_energy C t H <= mxdot (H - Q) (H - Q)

Statement as written in the source

Lemma cond_energy_le C H Q : H \is symmetricmx -> cond_cone C Q ->
  exists2 t : R, 0 <= t & cond_energy C t H <= mxdot (H - Q) (H - Q).

Used by 2 declarations in 1 file

this file: cond_cone_dist, cond_support_sqr

theorem cond_cone_dist main result source, line 427

forall [R : realType] [n : nat] [C : R] [H : 'M_n],
1 <= C ->
H \is symmetricmx -> inf [set mxdot (H - Q) (H - Q) | Q in cond_cone C] = cond_dist C H

The squared distance from H to the cone.

Main result, as the README states it

For C >= 1 and H symmetric, the squared Frobenius distance from H to cond_cone C is cond_dist C H, the infimum over t >= 0 of sum_i dist(lambda_i(H), [t, C t])^2: the lower bound by Hoffman-Wielandt, the upper bound by clipping the eigenvalues of H to [t, C t] (Tanaka and Nakata). The support function, the supremum of <H, Q> over the Q of the cone with |Q|_F <= 1, is the norm of the projection of H onto the cone, and its square is |H|_F^2 - cond_dist C H (Moreau's decomposition). Only the symmetric part of a matrix matters, the support function and cond_dist scale, and when the eigenvalues of H are at most T >= 0 the infimum over t may be taken over [0, T].

Statement as written in the source

Theorem cond_cone_dist C H : 1 <= C -> H \is symmetricmx ->
  inf [set mxdot (H - Q) (H - Q) | Q in cond_cone C] = cond_dist C H.

lemma mxdot_vec_mx source, line 440

forall [R : realType] [n : nat] (u v : 'rV_(n * n)),
mxdot (vec_mx u) (vec_mx v) = mxdot u v

Statement as written in the source

Lemma mxdot_vec_mx (u v : 'rV[R]_(n * n)) :
  mxdot (vec_mx u) (vec_mx v) = mxdot u v.

Used by 3 declarations in 1 file

this file: cond_support_vec, cond_support_sqr, cond_slice_vec_frobenius

definition cond_support source, line 445

Type

forall [R : realType] [n : nat], R -> 'M_n -> R

Definition

Definition cond_support C A : R :=
  sup [set mxdot A Q | Q in [set Q | cond_cone C Q /\ mxdot Q Q <= 1]].

The support function of the cone on the Frobenius unit ball.

Used by 6 declarations in 1 file

this file: cond_support_vec, cond_support_proj, cond_support_ge0, cond_support_sqr, cond_support_sym, cond_supportZ

lemma cond_support_vec source, line 448

forall [R : realType] [n : nat] (C : R) (h : 'rV_(n * n)),
sup [set mxdot h v | v in [set v | cond_cone_vec C v /\ mxdot v v <= 1]] =
cond_support C (vec_mx h)

Statement as written in the source

Lemma cond_support_vec C (h : 'rV[R]_(n * n)) :
  sup [set mxdot h v | v in [set v | cond_cone_vec C v /\ mxdot v v <= 1]] =
  cond_support C (vec_mx h).

Used by 1 declaration in 1 file

this file: cond_support_proj

lemma cond_support_proj main result source, line 461

forall [R : realType] [n : nat] [C : R] (h : 'rV_(n * n)),
0 <= C -> cond_support C (vec_mx h) = frobenius (proj (cond_cone_vec C) h)

The support function is the norm of the projection onto the cone.

Main result

Stated in the README together with cond_cone_dist.

Statement as written in the source

Lemma cond_support_proj C (h : 'rV[R]_(n * n)) : 0 <= C ->
  cond_support C (vec_mx h) = frobenius (proj (cond_cone_vec C) h).

Used by 3 declarations in 1 file

this file: cond_support_ge0, cond_support_sqr, cond_supportZ

lemma cond_support_ge0 source, line 469

forall [R : realType] [n : nat] [C : R] (A : 'M_n), 0 <= C -> 0 <= cond_support C A

Statement as written in the source

Lemma cond_support_ge0 C A : 0 <= C -> 0 <= cond_support C A.

theorem cond_support_sqr main result source, line 477

forall [R : realType] [n : nat] [C : R] [H : 'M_n],
1 <= C -> H \is symmetricmx -> cond_support C H ^+ 2 = mxdot H H - cond_dist C H

The support function in terms of the spectrum: by Moreau's decomposition, its square is |H|^2 minus the squared distance from H to the cone, and by cond_cone_dist that distance is cond_dist C H.

Main result

Stated in the README together with cond_cone_dist.

Statement as written in the source

Theorem cond_support_sqr C H : 1 <= C -> H \is symmetricmx ->
  cond_support C H ^+ 2 = mxdot H H - cond_dist C H.

lemma cond_support_sym main result source, line 514

forall [R : realType] [n : nat] (C : R) (A : 'M_n),
cond_support C A = cond_support C (2^-1 *: (A + A^T))

Only the symmetric part of A matters.

Main result

Stated in the README together with cond_cone_dist.

Statement as written in the source

Lemma cond_support_sym C A :
  cond_support C A = cond_support C (2^-1 *: (A + A^T)).

lemma cond_supportZ main result source, line 524

forall [R : realType] [n : nat] [C c : R] (A : 'M_n),
0 <= C -> 0 <= c -> cond_support C (c *: A) = c * cond_support C A

Main result

Stated in the README together with cond_cone_dist.

Statement as written in the source

Lemma cond_supportZ C (c : R) A : 0 <= C -> 0 <= c ->
  cond_support C (c *: A) = c * cond_support C A.

lemma cond_energyZ source, line 550

forall [R : realType] [n : nat] (C : R) [c : R] (t : R) [H : 'M_n],
0 <= c -> H \is symmetricmx -> cond_energy C (c * t) (c *: H) = c ^+ 2 * cond_energy C t H

Statement as written in the source

Lemma cond_energyZ C (c t : R) H : 0 <= c -> H \is symmetricmx ->
  cond_energy C (c * t) (c *: H) = c ^+ 2 * cond_energy C t H.

Used by 1 declaration in 1 file

this file: cond_distZ

lemma cond_distZ source, line 561

forall [R : realType] [n : nat] (C : R) [c : R] [H : 'M_n],
0 < c -> H \is symmetricmx -> cond_dist C (c *: H) = c ^+ 2 * cond_dist C H

Statement as written in the source

Lemma cond_distZ C (c : R) H : 0 < c -> H \is symmetricmx ->
  cond_dist C (c *: H) = c ^+ 2 * cond_dist C H.

lemma cond_energy_mono source, line 579

forall [R : realType] [n : nat] [C : R] [H : 'M_n] [t s : R],
1 <= C ->
0 <= t ->
(forall i : 'I_n, spec H 0 i <= t) -> t <= s -> cond_energy C t H <= cond_energy C s H

Beyond the largest eigenvalue the energy increases, so the infimum may be taken over a compact interval.

Statement as written in the source

Lemma cond_energy_mono C H t s : 1 <= C -> 0 <= t ->
  (forall i, spec H 0 i <= t) -> t <= s ->
  cond_energy C t H <= cond_energy C s H.

Used by 1 declaration in 1 file

this file: cond_dist_itv

lemma cond_dist_itv main result source, line 593

forall [R : realType] [n : nat] [C : R] [H : 'M_n] [T : R],
1 <= C ->
0 <= T ->
(forall i : 'I_n, spec H 0 i <= T) ->
cond_dist C H = inf [set cond_energy C t H | t in [set t | 0 <= t <= T]]

Main result

Stated in the README together with cond_cone_dist.

Statement as written in the source

Lemma cond_dist_itv C H (T : R) : 1 <= C -> 0 <= T ->
  (forall i, spec H 0 i <= T) ->
  cond_dist C H = inf [set cond_energy C t H | t in [set t | 0 <= t <= T]].

definition cond_slice source, line 615

Type

forall [R : realType] [n : nat], R -> set 'M_n

Definition

Definition cond_slice C : set 'M[R]_n :=
  [set Q | cond_cone C Q /\ \tr Q = n%:R].

The trace slice: a compact convex base of the cone.

Used by 7 declarations in 1 file

this file: cond_slice1, cond_slice_t, cond_slice_spec, cond_slice_form, cond_slice_frobenius, cond_cone_slice, cond_slice_vec

lemma cond_slice1 source, line 618

forall [R : realType] (n : nat) [C : R], 1 <= C -> cond_slice C 1%:M

Statement as written in the source

Lemma cond_slice1 C : 1 <= C -> cond_slice C 1%:M.

lemma cond_slice_t main result source, line 622

forall [R : realType] [n : nat] [C : R] [Q : 'M_n],
0 < C ->
(0 < n)%N ->
cond_slice C Q ->
exists2 t : R,
  C^-1 <= t <= 1 & forall x : 'cV_n, t * mxdot x x <= mxdot x (Q *m x) <= C * t * mxdot x x

A matrix of the slice is between t I and C t I for some t in [1/C, 1].

Main result, as the README states it

The trace slice {Q in cond_cone C : tr Q = n} is a closed convex base of the cone: for C > 0 and n >= 1 its matrices satisfy t I <= Q <= C t I for some t in [1/C, 1], have eigenvalues in [1/C, C] and n <= |Q|_F^2 <= C n, and every nonzero point of the cone has a positive multiple in it.

Statement as written in the source

Lemma cond_slice_t C Q : 0 < C -> (0 < n)%N -> cond_slice C Q ->
  exists2 t : R, C^-1 <= t <= 1 &
    forall x : 'cV[R]_n, t * mxdot x x <= mxdot x (Q *m x) <= C * t * mxdot x x.

lemma cond_slice_spec main result source, line 648

forall [R : realType] [n : nat] [C : R] [Q : 'M_n],
0 < C -> cond_slice C Q -> forall i : 'I_n, C^-1 <= spec Q 0 i <= C

Main result

Stated in the README together with cond_slice_t.

Statement as written in the source

Lemma cond_slice_spec C Q : 0 < C -> cond_slice C Q ->
  forall i, C^-1 <= spec Q 0 i <= C.

Used by 2 declarations in 1 file

this file: cond_slice_form, cond_slice_frobenius

lemma cond_slice_form source, line 672

forall [R : realType] [n : nat] [C : R] [Q : 'M_n],
0 < C ->
cond_slice C Q -> forall x : 'cV_n, C^-1 * mxdot x x <= mxdot x (Q *m x) <= C * mxdot x x

Statement as written in the source

Lemma cond_slice_form C Q : 0 < C -> cond_slice C Q ->
  forall x : 'cV[R]_n, C^-1 * mxdot x x <= mxdot x (Q *m x) <= C * mxdot x x.

lemma cond_slice_frobenius main result source, line 683

forall [R : realType] [n : nat] [C : R] [Q : 'M_n],
0 < C -> cond_slice C Q -> n%:R <= mxdot Q Q <= C * n%:R

Main result

Stated in the README together with cond_slice_t.

Statement as written in the source

Lemma cond_slice_frobenius C Q : 0 < C -> cond_slice C Q ->
  n%:R <= mxdot Q Q <= C * n%:R.

Used by 1 declaration in 1 file

this file: cond_slice_vec_frobenius

lemma cond_cone_slice main result source, line 708

forall [R : realType] [n : nat] [C : R] [Q : 'M_n],
cond_cone C Q -> Q != 0 -> 0 < \tr Q /\ cond_slice C ((n%:R / \tr Q) *: Q)

Every nonzero point of the cone has a positive multiple in the slice.

Main result

Stated in the README together with cond_slice_t.

Statement as written in the source

Lemma cond_cone_slice C Q : cond_cone C Q -> Q != 0 ->
  0 < \tr Q /\ cond_slice C ((n%:R / \tr Q) *: Q).

Used by 1 declaration in 1 file

this file: cond_cone_vec_slice

definition cond_slice_vec source, line 730

Type

forall [R : realType] [n : nat], R -> set 'rV_(n * n)

Definition

Definition cond_slice_vec C : set 'rV[R]_(n * n) :=
  [set v | cond_slice C (vec_mx v)].

The slice in the coordinates of mxvec.

Used by 4 declarations in 1 file

this file: cond_slice_vec_closed, cond_slice_vec_convex, cond_slice_vec_frobenius, cond_cone_vec_slice

lemma cond_slice_vec_closed main result source, line 733

forall [R : realType] [n : nat] [C : R], 0 <= C -> closed (cond_slice_vec C)

Main result

Stated in the README together with cond_slice_t.

Statement as written in the source

Lemma cond_slice_vec_closed C : 0 <= C -> closed (cond_slice_vec C).

lemma cond_slice_vec_convex main result source, line 755

forall [R : realType] [n : nat] [C : R] [x y : 'rV_(n * n)] [s : R],
cond_slice_vec C x ->
cond_slice_vec C y -> 0 <= s <= 1 -> cond_slice_vec C (x + s *: (y - x))

Main result

Stated in the README together with cond_slice_t.

Statement as written in the source

Lemma cond_slice_vec_convex C (x y : 'rV[R]_(n * n)) (s : R) :
  cond_slice_vec C x -> cond_slice_vec C y -> 0 <= s <= 1 ->
  cond_slice_vec C (x + s *: (y - x)).

lemma cond_slice_vec_frobenius source, line 764

forall [R : realType] [n : nat] [C : R] [v : 'rV_(n * n)],
0 < C -> cond_slice_vec C v -> n%:R <= mxdot v v <= C * n%:R

Statement as written in the source

Lemma cond_slice_vec_frobenius C (v : 'rV[R]_(n * n)) : 0 < C ->
  cond_slice_vec C v -> n%:R <= mxdot v v <= C * n%:R.

lemma cond_cone_vec_slice main result source, line 770

forall [R : realType] [n : nat] [C : R] [v : 'rV_(n * n)],
cond_cone_vec C v -> v != 0 -> exists2 a : R, 0 < a & cond_slice_vec C (a *: v)

Main result

Stated in the README together with cond_slice_t.

Statement as written in the source

Lemma cond_cone_vec_slice C (v : 'rV[R]_(n * n)) :
  cond_cone_vec C v -> v != 0 ->
  exists2 a : R, 0 < a & cond_slice_vec C (a *: v).

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.