On this page

The log-determinant barrier

GaussianAnalysis.convex.logdet_barrierlibrary/convex/logdet_barrier.v904 lines36 lemmas and theorems, 12 definitionssource

Imports 3 library modules and 22 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.algebra.vector, mathcomp.algebra.interval, mathcomp.classical.boolp, mathcomp.classical.classical_sets, mathcomp.classical.functions, mathcomp.reals.reals, mathcomp.classical.set_interval, mathcomp.analysis.topology_theory.topology, mathcomp.analysis.normedtype_theory.normedtype, mathcomp.analysis.sequences, mathcomp.analysis.derive, mathcomp.analysis.realfun, mathcomp.analysis.exp, mathcomp.algebra.ring_tactic, mathcomp.algebra.field_tactic, mathcomp.algebra.arithmetic_tactic

Imported by 2

Required by 16 files of the paper proofs

-ln det is a self-concordant barrier with parameter n on the trace slices of the cone of positive definite n x n matrices (Nesterov-Nemirovskii, Proposition 5.4.5), and -ln det (A - m I) - ln det (M I - A) is a 2n-self-concordant barrier on the matrices of trace n with m I < A < M I. This is Lemma 2.8 of Koehler and Sohn (arXiv 2608.27372). Matrices are seen as row vectors of size n * n through mxvec, so that self_concordant.v applies; the inner product of mxvec A and mxvec B is the Frobenius product mxdot A B.

`posdefmx A`	A is symmetric positive definite: 0 < x A x^T for every row vector x != 0
`pd_slice n s`	the matrices A (as mxvec A) that are positive definite with trace s
`logdet_barrier n x`	- ln (det (vec_mx x)), for x : 'rV[R]_(n * n)
`pd_slice2 n m M`	the matrices A (as mxvec A) of trace n with A - m I and M I - A positive definite
`logdet_barrier2 n m M x`	- ln det (A - m I) - ln det (M I - A) + n ln ((1 - m) (M - 1)), with A = vec_mx x
`sym_traceless n`	the subspace of the mxvec of the symmetric matrices of trace 0
`logsum l c t`	c - sum_i ln (1 + t l_i), for l : 'rV[R]_k

Main results:

logdet_line: for A positive definite and U symmetric, -ln det (A + t U) = c - sum_i ln (1 + t l_i) whenever A + t U is positive definite, which happens exactly when every 1 + t l_i is positive; tr (A^-1 U) and tr ((A^-1 U)^2) are the sums of the l_i and of their squares (simultaneous diagonalization, congruence_diag).
logsum_sc_barrier: a function that is c - sum_i ln (1 + t l_i), i < k, along every line through D, and whose first and second derivatives at each point are a linear and a bilinear form, is a k-self-concordant barrier on D.
rel_open_convex_pd_slice, logdet_sc_barrier: pd_slice n s is convex and relatively open with directions sym_traceless n, and logdet_barrier n is an n-self-concordant barrier on it.
logdet_barrier_ge0, logdet_barrier_one: logdet_barrier n >= 0 on pd_slice n n, with value 0 at the identity (det A <= (tr A / n)^n).
rel_open_convex_pd_slice2, logdet2_sc_barrier: for all m and M, pd_slice2 n m M is convex and relatively open with directions sym_traceless n, and logdet_barrier2 n m M is a 2n-self-concordant barrier on it.
logdet_barrier2_ge0, logdet_barrier2_one: if m < 1 < M, then logdet_barrier2 n m M >= 0 on pd_slice2 n m M, with value 0 at the identity.

Main results

Results	Statement
posdefmxpd_slicelogdet_barrierpd_slice2logdet_barrier2sym_tracelesssym_tracelessP	Matrices as row vectors through `mxvec`: `pd_slice n s` is the set of the positive definite `n x n` matrices of trace `s`, `logdet_barrier n x = - ln det (vec_mx x)`, `pd_slice2 n m M` is the set of the matrices `A` of trace `n` with `m I < A < M I`, `logdet_barrier2 n m M x = - ln det (A - m I) - ln det (M I - A) + n ln ((1 - m) (M - 1))`, and `sym_traceless n` is the subspace of the symmetric matrices of trace 0.
logdet_linecongruence_diag	For `A` positive definite and `U` symmetric there are `G` invertible and reals `l_i` with `A = G^T G` and `U = G^T diag(l) G`; hence `-ln det (A + t U) = c - sum_i ln (1 + t l_i)` whenever `A + t U` is positive definite, which happens exactly when every `1 + t l_i` is positive, and `tr (A^-1 U) = sum_i l_i`, `tr ((A^-1 U)^2) = sum_i l_i^2`.
logsum_sc_barrier	A function that equals `c - sum_(i < k) ln (1 + t l_i)` along every line through `D` (with `D` convex and relatively open, the `l_i` and `c` depending on the line), and whose first and second derivatives at each point of `D` are a linear and a bilinear form, is a `k`-self-concordant barrier on `D`.
logdet_sc_barrierrel_open_convex_pd_slicelogdet_barrier_ge0logdet_barrier_one	Lemma 2.8 of Koehler and Sohn, one-sided (Nesterov-Nemirovskii, Proposition 5.4.5): `pd_slice n s` is convex and relatively open with directions `sym_traceless n`, and `logdet_barrier n` is an `n`-self-concordant barrier on it. On `pd_slice n n` it is nonnegative (`det A <= (tr A / n)^n`), with value 0 at the identity.
logdet2_sc_barrierrel_open_convex_pd_slice2logdet_barrier2_ge0logdet_barrier2_one	Lemma 2.8 of Koehler and Sohn, two-sided: `pd_slice2 n m M` is convex and relatively open with directions `sym_traceless n`, and `logdet_barrier2 n m M` is a `2n`-self-concordant barrier on it; if `m < 1 < M` it is nonnegative there, with value 0 at the identity.

Declarations48 exported

sectionlogdet_definitions

Context {R : realType}.

definition posdefmx main result source, line 73

Type

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

Definition

Definition posdefmx n (A : 'M[R]_n) : Prop :=
  A \is symmetricmx /\ forall x : 'rV[R]_n, x != 0 -> 0 < mxdot x (x *m A).

Main result, as the README states it

Matrices as row vectors through mxvec: pd_slice n s is the set of the positive definite n x n matrices of trace s, logdet_barrier n x = - ln det (vec_mx x), pd_slice2 n m M is the set of the matrices A of trace n with m I < A < M I, logdet_barrier2 n m M x = - ln det (A - m I) - ln det (M I - A) + n ln ((1 - m) (M - 1)), and sym_traceless n is the subspace of the symmetric matrices of trace 0.

Used by 15 declarations in 3 files

this file: pd_slice, pd_slice2, posdefmx_spectral, posdefmx_congruence, congruence_diag, logdet_line, posdefmx_ge, posdefmx_convex, posdefmx_open, rel_open_convex_pd_slice2, posdefmx_scalar
GaussianAnalysis.convex.minimizers: vspace_orthonormal, posdefmx_unit, quad_response
GaussianAnalysis.convex.ls_insertion: ins_hessian_pd

definition pd_slice main result source, line 76

Type

forall {R : realType} (n : nat), R -> set 'rV_(n * n)

Definition

Definition pd_slice n (s : R) : set 'rV[R]_(n * n) :=
  [set x | posdefmx (vec_mx x) /\ \tr (vec_mx x) = s].

Main result

Stated in the README together with posdefmx.

Used by 4 declarations in 1 file

this file: rel_open_convex_pd_slice, logdet_sc_barrier, pd_slice_one, logdet_barrier_ge0

definition logdet_barrier main result source, line 79

Type

forall {R : realType} (n : nat), 'rV_(n * n) -> R

Definition

Definition logdet_barrier n (x : 'rV[R]_(n * n)) : R := - ln (\det (vec_mx x)).

Main result

Stated in the README together with posdefmx.

Used by 3 declarations in 1 file

this file: logdet_sc_barrier, logdet_barrier_one, logdet_barrier_ge0

definition pd_slice2 main result source, line 81

Type

forall {R : realType} (n : nat), R -> R -> set 'rV_(n * n)

Definition

Definition pd_slice2 n (m M : R) : set 'rV[R]_(n * n) :=
  [set x | posdefmx (vec_mx x - m%:M) /\ posdefmx (M%:M - vec_mx x) /\
           \tr (vec_mx x) = n%:R].

Main result

Stated in the README together with posdefmx.

Used by 4 declarations in 1 file

this file: rel_open_convex_pd_slice2, logdet2_sc_barrier, pd_slice2_one, logdet_barrier2_ge0

definition logdet_barrier2 main result source, line 85

Type

forall {R : realType} (n : nat), R -> R -> 'rV_(n * n) -> R

Definition

Definition logdet_barrier2 n (m M : R) (x : 'rV[R]_(n * n)) : R :=
  - ln (\det (vec_mx x - m%:M)) - ln (\det (M%:M - vec_mx x)) +
  n%:R * ln ((1 - m) * (M - 1)).

Main result

Stated in the README together with posdefmx.

Used by 3 declarations in 1 file

this file: logdet2_sc_barrier, logdet_barrier2_one, logdet_barrier2_ge0

Arguments pd_slice {R} n s.
Arguments logdet_barrier {R} n x.
Arguments pd_slice2 {R} n m M.
Arguments logdet_barrier2 {R} n m M x.

sectionmxvec_facts

Context {R : realType}.

lemma mxdot_mxvec source, line 100

forall {R : realType} [m n : nat] (A B : 'M_(m, n)), mxdot (mxvec A) (mxvec B) = mxdot A B

mxvec is an isometry for the Frobenius products.

Statement as written in the source

Lemma mxdot_mxvec m n (A B : 'M[R]_(m, n)) :
  mxdot (mxvec A) (mxvec B) = mxdot A B.

Used by 1 declaration in 1 file

this file: frobenius_mxvec

lemma frobenius_mxvec source, line 108

forall {R : realType} [m n : nat] (A : 'M_(m, n)), frobenius (mxvec A) = frobenius A

Statement as written in the source

Lemma frobenius_mxvec m n (A : 'M[R]_(m, n)) :
  frobenius (mxvec A) = frobenius A.

Used by 1 declaration in 1 file

this file: frobenius_vec_mx

sectionposdef

Context {R : realType}.
Implicit Types n : nat.

lemma posdefmx_spectral source, line 120

forall {R : realType} [n : nat] [A : 'M_n],
posdefmx A ->
exists2 P : 'M_n,
  P \is orthogonalmx &
  exists2 d : 'rV_n, A = P^T *m diag_mx d *m P & forall i : 'I_n, 0 < d 0 i

The spectral decomposition of a positive definite matrix has positive eigenvalues.

Statement as written in the source

Lemma posdefmx_spectral n (A : 'M[R]_n) : posdefmx A ->
  exists2 P : 'M[R]_n, P \is orthogonalmx &
    exists2 d : 'rV[R]_n, A = P^T *m diag_mx d *m P & forall i, 0 < d 0 i.

Used by 5 declarations in 2 files

this file: congruence_diag, posdefmx_ge, logdet_barrier_ge0
GaussianAnalysis.convex.minimizers: vspace_orthonormal, posdefmx_unit

lemma posdefmx_congruence source, line 142

forall {R : realType} [n : nat] [G : 'M_n] (c : 'rV_n),
G \in unitmx -> posdefmx (G^T *m diag_mx c *m G) <-> (forall i : 'I_n, 0 < c 0 i)

G^T diag(c) G with G invertible is positive definite exactly when the c_i are positive.

Statement as written in the source

Lemma posdefmx_congruence n (G : 'M[R]_n) (c : 'rV[R]_n) : G \in unitmx ->
  posdefmx (G^T *m diag_mx c *m G) <-> forall i, 0 < c 0 i.

Used by 2 declarations in 1 file

this file: logdet_line, logdet_barrier2_ge0

lemma det_congruence source, line 177

forall {R : realType} [n : nat] (G : 'M_n) (c : 'rV_n),
\det (G^T *m diag_mx c *m G) = \det G ^+ 2 * \prod_i c 0 i

Statement as written in the source

Lemma det_congruence n (G : 'M[R]_n) (c : 'rV[R]_n) :
  \det (G^T *m diag_mx c *m G) = \det G ^+ 2 * \prod_i c 0 i.

Used by 4 declarations in 2 files

this file: logdet_line, logdet_barrier_ge0, logdet_barrier2_ge0
GaussianAnalysis.convex.minimizers: posdefmx_unit

lemma congruence_diag main result source, line 183

forall {R : realType} [n : nat] [A U : 'M_n],
posdefmx A ->
U \is symmetricmx ->
exists (G : 'M_n) (l : 'rV_n), [/\ G \in unitmx, A = G^T *m G & U = G^T *m diag_mx l *m G]

Simultaneous diagonalization by congruence: for A positive definite and U symmetric, A = G^T G and U = G^T diag(l) G with G invertible.

Main result

Stated in the README together with logdet_line.

Statement as written in the source

Lemma congruence_diag n (A U : 'M[R]_n) : posdefmx A -> U \is symmetricmx ->
  exists (G : 'M[R]_n) (l : 'rV[R]_n),
    [/\ G \in unitmx, A = G^T *m G & U = G^T *m diag_mx l *m G].

Used by 1 declaration in 1 file

this file: logdet_line

sectionlogdet_line

Context {R : realType}.
Implicit Types n : nat.

lemma ln_prod source, line 237

forall {R : realType} [k : nat] [F : 'I_k -> R],
(forall i : 'I_k, 0 < F i) -> 0 < \prod_i F i /\ ln (\prod_i F i) = \sum_i ln (F i)

Statement as written in the source

Lemma ln_prod k (F : 'I_k -> R) : (forall i, 0 < F i) ->
  0 < \prod_i F i /\ ln (\prod_i F i) = \sum_i ln (F i).

Used by 4 declarations in 2 files

this file: logdet_line, logdet_barrier_ge0, logdet_barrier2_ge0
GaussianAnalysis.convex.minimizers: posdefmx_unit

lemma logdet_line main result source, line 249

forall {R : realType} [n : nat] [A U : 'M_n],
posdefmx A ->
U \is symmetricmx ->
exists (c : R) (l : 'rV_n),
  [/\ forall t : R, posdefmx (A + t *: U) <-> (forall i : 'I_n, 0 < 1 + t * l 0 i),
      forall t : R,
      posdefmx (A + t *: U) -> - ln (\det (A + t *: U)) = c - \sum_i ln (1 + t * l 0 i),
      \tr (invmx A *m U) = \sum_i l 0 i
    & \tr (invmx A *m U *m invmx A *m U) = \sum_i l 0 i ^+ 2]

Along a line through a positive definite A in a symmetric direction U, -ln det (A + t U) = c - sum_i ln (1 + t l_i), where l is the spectrum of U relative to A; A + t U is positive definite exactly when every 1 + t l_i is positive, and tr (A^-1 U) and tr ((A^-1 U)^2) are the sums of the l_i and of their squares.

Main result, as the README states it

For A positive definite and U symmetric there are G invertible and reals l_i with A = G^T G and U = G^T diag(l) G; hence -ln det (A + t U) = c - sum_i ln (1 + t l_i) whenever A + t U is positive definite, which happens exactly when every 1 + t l_i is positive, and tr (A^-1 U) = sum_i l_i, tr ((A^-1 U)^2) = sum_i l_i^2.

Statement as written in the source

Lemma logdet_line n (A U : 'M[R]_n) : posdefmx A -> U \is symmetricmx ->
  exists (c : R) (l : 'rV[R]_n),
  [/\ forall t : R, posdefmx (A + t *: U) <-> (forall i, 0 < 1 + t * l 0 i),
      forall t : R, posdefmx (A + t *: U) ->
        - ln (\det (A + t *: U)) = c - \sum_i ln (1 + t * l 0 i),
      \tr (invmx A *m U) = \sum_i l 0 i &
      \tr (invmx A *m U *m invmx A *m U) = \sum_i l 0 i ^+ 2].

Used by 2 declarations in 1 file

this file: logdet_sc_barrier, logdet2_sc_barrier

sectionlogsum

Context {R : realType} (k : nat) (l : 'rV[R]_k) (c : R).

definition logsum source, line 301

Type

forall {R : realType} [k : nat], 'rV_k -> R -> R -> R

Definition

Definition logsum (t : R) : R := c - \sum_i ln (1 + t * l 0 i).

The function c - sum_i ln (1 + t l_i) and its first three derivatives.

Used by 4 declarations in 1 file

this file: logsum_derive, logsum_blowup, logsum_sc_barrier, logdet2_sc_barrier

definition logsum1 source, line 302

Type

forall {R : realType} [k : nat], 'rV_k -> R -> R

Definition

Definition logsum1 (t : R) : R := - \sum_i l 0 i / (1 + t * l 0 i).

Used by 3 declarations in 1 file

this file: logsum_derive, logsum_bp, logsum_sc_barrier

definition logsum2 source, line 303

Type

forall {R : realType} [k : nat], 'rV_k -> R -> R

Definition

Definition logsum2 (t : R) : R := \sum_i (l 0 i / (1 + t * l 0 i)) ^+ 2.

Used by 5 declarations in 1 file

this file: logsum_derive, logsum2_ge0, logsum_sc, logsum_bp, logsum_sc_barrier

definition logsum3 source, line 304

Type

forall {R : realType} [k : nat], 'rV_k -> R -> R

Definition

Definition logsum3 (t : R) : R := - 2 * \sum_i (l 0 i / (1 + t * l 0 i)) ^+ 3.

Used by 3 declarations in 1 file

this file: logsum_derive, logsum_sc, logsum_sc_barrier

lemma logsum_derive source, line 306

forall {R : realType} [k : nat] [l : 'rV_k] (c : R) [t : R],
(forall i : 'I_k, 0 < 1 + t * l 0 i) ->
[/\ is_derive t 1 (logsum l c) (logsum1 l t), is_derive t 1 (logsum1 l) (logsum2 l t)
  & is_derive t 1 (logsum2 l) (logsum3 l t)]

Statement as written in the source

Lemma logsum_derive (t : R) : (forall i, 0 < 1 + t * l 0 i) ->
  [/\ is_derive t 1 logsum (logsum1 t), is_derive t 1 logsum1 (logsum2 t) &
      is_derive t 1 logsum2 (logsum3 t)].

Used by 1 declaration in 1 file

this file: logsum_sc_barrier

lemma logsum2_ge0 source, line 348

forall {R : realType} [k : nat] (l : 'rV_k) (t : R), 0 <= logsum2 l t

Statement as written in the source

Lemma logsum2_ge0 (t : R) : 0 <= logsum2 t.

Used by 1 declaration in 1 file

this file: logsum_sc_barrier

lemma logsum_sc source, line 351

forall {R : realType} [k : nat] (l : 'rV_k) (t : R),
logsum3 l t ^+ 2 <= 4 * logsum2 l t ^+ 3

Statement as written in the source

Lemma logsum_sc (t : R) : logsum3 t ^+ 2 <= 4%:R * logsum2 t ^+ 3.

Used by 1 declaration in 1 file

this file: logsum_sc_barrier

lemma logsum_bp source, line 375

forall {R : realType} [k : nat] (l : 'rV_k) (t : R), logsum1 l t ^+ 2 <= k%:R * logsum2 l t

Statement as written in the source

Lemma logsum_bp (t : R) : logsum1 t ^+ 2 <= k%:R * logsum2 t.

Used by 1 declaration in 1 file

this file: logsum_sc_barrier

lemma logsum_blowup source, line 385

forall {R : realType} [k : nat] [l : 'rV_k] (c : R),
(forall t : join_Num_POrderNmodule_between_Algebra_BaseAddUMagma_and_Order_Preorder R,
 0 <= t < 1 -> forall i : 'I_k, 0 < 1 + t * l 0 i) ->
~ (forall i : 'I_k, 0 < 1 + l 0 i) -> logsum l c t @[t --> (1 : R)^'-] --> +oo

Statement as written in the source

Lemma logsum_blowup : (forall t, 0 <= t < 1 -> forall i, 0 < 1 + t * l 0 i) ->
  ~ (forall i, 0 < 1 + l 0 i) -> logsum t @[t --> (1 : R)^'-] --> +oo.

Used by 1 declaration in 1 file

this file: logsum_sc_barrier

sectionsym_traceless

Context {R : realType}.
Implicit Types n : nat.

definition symtr_map source, line 425

Type

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

Definition

Definition symtr_map n (h : 'rV[R]_(n * n)) : 'rV[R]_(n * n) :=
  mxvec (vec_mx h - (vec_mx h)^T + (\tr (vec_mx h))%:M).

The kernel of h |-> mxvec (U - U^T + (tr U) I), U = vec_mx h, is the set of the mxvec of the symmetric matrices of trace 0.

Used by 3 declarations in 1 file

this file: symtr_map_is_linear, symtr_lin, sym_tracelessP

lemma symtr_map_is_linear source, line 428

forall {R : realType} [n : nat], linear (symtr_map (n:=n))

Statement as written in the source

Lemma symtr_map_is_linear n : linear (@symtr_map n).

Used by 1 declaration in 1 file

this file: symtr_lin

definition symtr_lin source, line 439

Type

forall {R : realType} (n : nat), {linear 'rV_(n * n) -> 'rV_(n * n)}

Definition

Definition symtr_lin n : {linear 'rV[R]_(n * n) -> 'rV[R]_(n * n)} :=
  HB.pack (@symtr_map n)
    (GRing.isLinear.Build _ _ _ _ (@symtr_map n) (@symtr_map_is_linear n)).

Used by 1 declaration in 1 file

this file: sym_traceless

definition sym_traceless main result source, line 443

Type

forall {R : realType} (n : nat), {vspace 'rV_(n * n)}

Definition

Definition sym_traceless n : {vspace 'rV[R]_(n * n)} :=
  lker (linfun (symtr_lin n)).

Main result

Stated in the README together with posdefmx.

Used by 6 declarations in 1 file

this file: sym_tracelessP, dim_sym_traceless, rel_open_convex_pd_slice, rel_open_convex_pd_slice2, logdet_sc_barrier, logdet2_sc_barrier

lemma sym_tracelessP main result source, line 446

forall {R : realType} [n : nat] (h : 'rV_(n * n)),
h \in sym_traceless n <-> vec_mx h \is symmetricmx /\ \tr (vec_mx h) = 0

Main result

Stated in the README together with posdefmx.

Statement as written in the source

Lemma sym_tracelessP n (h : 'rV[R]_(n * n)) :
  h \in sym_traceless n <-> vec_mx h \is symmetricmx /\ \tr (vec_mx h) = 0.

Used by 4 declarations in 1 file

this file: rel_open_convex_pd_slice, rel_open_convex_pd_slice2, logdet_sc_barrier, logdet2_sc_barrier

lemma dim_sym_traceless source, line 463

forall {R : realType} (n : nat), (\dim (sym_traceless n) <= n * n)%N

Statement as written in the source

Lemma dim_sym_traceless n : (\dim (sym_traceless n) <= n * n)%N.

sectionpd_slice

Context {R : realType}.
Implicit Types n : nat.

lemma posdefmx_ge source, line 476

forall {R : realType} [n : nat] [A : 'M_n],
posdefmx A -> exists2 b : R, 0 < b & forall x : 'rV_n, b * mxdot x x <= mxdot x (x *m A)

A positive definite matrix dominates b I for some b > 0.

Statement as written in the source

Lemma posdefmx_ge n (A : 'M[R]_n) : posdefmx A ->
  exists2 b : R, 0 < b & forall x : 'rV[R]_n, b * mxdot x x <= mxdot x (x *m A).

Used by 1 declaration in 1 file

this file: posdefmx_open

lemma posdefmx_convex source, line 491

forall {R : realType} [n : nat] [A B : 'M_n] [t : R],
posdefmx A -> posdefmx B -> 0 <= t <= 1 -> posdefmx (A + t *: (B - A))

Statement as written in the source

Lemma posdefmx_convex n (A B : 'M[R]_n) (t : R) : posdefmx A -> posdefmx B ->
  0 <= t <= 1 -> posdefmx (A + t *: (B - A)).

Used by 2 declarations in 1 file

this file: rel_open_convex_pd_slice, rel_open_convex_pd_slice2

lemma posdefmx_open source, line 503

forall {R : realType} [n : nat] [A : 'M_n],
posdefmx A ->
exists2 e : R,
  0 < e & forall U : 'M_n, U \is symmetricmx -> frobenius U < e -> posdefmx (A + U)

The positive definite matrices form an open set.

Statement as written in the source

Lemma posdefmx_open n (A : 'M[R]_n) : posdefmx A ->
  exists2 e : R, 0 < e & forall U, U \is symmetricmx -> frobenius U < e ->
    posdefmx (A + U).

Used by 2 declarations in 1 file

this file: rel_open_convex_pd_slice, rel_open_convex_pd_slice2

lemma frobenius_vec_mx source, line 525

forall {R : realType} [n : nat] (h : 'rV_(n * n)), frobenius (vec_mx h) <= n%:R * `|h|

Statement as written in the source

Lemma frobenius_vec_mx n (h : 'rV[R]_(n * n)) :
  frobenius (vec_mx h) <= n%:R * `|h|.

Used by 2 declarations in 1 file

this file: rel_open_convex_pd_slice, rel_open_convex_pd_slice2

lemma rel_open_convex_pd_slice main result source, line 534

forall {R : realType} (n : nat) (s : R), rel_open_convex (sym_traceless n) (pd_slice n s)

Main result

Stated in the README together with logdet_sc_barrier.

Statement as written in the source

Lemma rel_open_convex_pd_slice n (s : R) :
  rel_open_convex (sym_traceless n) (pd_slice n s).

Used by 1 declaration in 1 file

this file: logdet_sc_barrier

lemma rel_open_convex_pd_slice2 main result source, line 561

forall {R : realType} (n : nat) (m M : R),
rel_open_convex (sym_traceless n) (pd_slice2 n m M)

Main result

Stated in the README together with logdet2_sc_barrier.

Statement as written in the source

Lemma rel_open_convex_pd_slice2 n (m M : R) :
  rel_open_convex (sym_traceless n) (pd_slice2 n m M).

Used by 1 declaration in 1 file

this file: logdet2_sc_barrier

sectionlogsum_barrier

Context {R : realType} {N : nat}.

lemma logsum_sc_barrier main result source, line 612

forall {R : realType} {N : nat} [V : {vspace 'rV_N}] [D : set 'rV_N] 
  [B : 'rV_N -> R] [k : nat],
rel_open_convex V D ->
(forall z : 'rV_N,
 D z ->
 exists (L : 'rV_N -> R) (Q : 'rV_N -> 'rV_N -> R),
   [/\ forall (c : R) (u v : 'rV_N), L (c *: u + v) = c * L u + L v,
       forall (c : R) (u v w : 'rV_N), Q (c *: u + v) w = c * Q u w + Q v w,
       forall (c : R) (u v w : 'rV_N), Q w (c *: u + v) = c * Q w u + Q w v
     & forall h : 'rV_N,
       h \in V ->
       exists (c : R) (l : 'rV_k),
         [/\ forall t : R, D (z + t *: h) <-> (forall i : 'I_k, 0 < 1 + t * l 0 i),
             forall t : R, D (z + t *: h) -> B (z + t *: h) = logsum l c t,
             L h = - \sum_i l 0 i
           & Q h h = \sum_i l 0 i ^+ 2]]) ->
sc_barrier V D k%:R B

A function that is c - sum_i ln (1 + t l_i) along every line through D, with first and second derivatives at each point of D given by a linear and a bilinear form, is a k-self-concordant barrier on D.

Main result, as the README states it

A function that equals c - sum_(i < k) ln (1 + t l_i) along every line through D (with D convex and relatively open, the l_i and c depending on the line), and whose first and second derivatives at each point of D are a linear and a bilinear form, is a k-self-concordant barrier on D.

Statement as written in the source

Lemma logsum_sc_barrier (V : {vspace 'rV[R]_N}) (D : set 'rV[R]_N)
    (B : 'rV[R]_N -> R) k :
  rel_open_convex V D ->
  (forall z, D z -> exists (L : 'rV[R]_N -> R) (Q : 'rV[R]_N -> 'rV[R]_N -> R),
    [/\ forall (c : R) (u v : 'rV[R]_N), L (c *: u + v) = c * L u + L v,
        forall (c : R) (u v w : 'rV[R]_N),
          Q (c *: u + v) w = c * Q u w + Q v w,
        forall (c : R) (u v w : 'rV[R]_N),
          Q w (c *: u + v) = c * Q w u + Q w v &
        forall h, h \in V -> exists (c : R) (l : 'rV[R]_k),
          [/\ forall t, D (z + t *: h) <-> (forall i, 0 < 1 + t * l 0 i),
              forall t, D (z + t *: h) -> B (z + t *: h) = logsum l c t,
              L h = - \sum_i l 0 i & Q h h = \sum_i l 0 i ^+ 2]]) ->
  sc_barrier V D k%:R B.

Used by 2 declarations in 1 file

this file: logdet_sc_barrier, logdet2_sc_barrier

sectionlogdet_barrier_theorems

Context {R : realType}.
Implicit Types n : nat.

lemma tr_form_linear source, line 689

forall {R : realType} [n : nat] (P : 'M_n) (c : R) (u v : 'rV_(n * n)),
\tr (P *m vec_mx (c *: u + v)) = c * \tr (P *m vec_mx u) + \tr (P *m vec_mx v)

The trace forms that give the first two derivatives of -ln det are linear.

Statement as written in the source

Lemma tr_form_linear n (P : 'M[R]_n) (c : R) (u v : 'rV[R]_(n * n)) :
  \tr (P *m vec_mx (c *: u + v)) =
  c * \tr (P *m vec_mx u) + \tr (P *m vec_mx v).

Used by 2 declarations in 1 file

this file: logdet_sc_barrier, logdet2_sc_barrier

lemma tr_form2_linearl source, line 694

forall {R : realType} [n : nat] (P : 'M_n) (c : R) (u v w : 'rV_(n * n)),
\tr (P *m vec_mx (c *: u + v) *m P *m vec_mx w) =
c * \tr (P *m vec_mx u *m P *m vec_mx w) + \tr (P *m vec_mx v *m P *m vec_mx w)

Statement as written in the source

Lemma tr_form2_linearl n (P : 'M[R]_n) (c : R) (u v w : 'rV[R]_(n * n)) :
  \tr (P *m vec_mx (c *: u + v) *m P *m vec_mx w) =
  c * \tr (P *m vec_mx u *m P *m vec_mx w) +
  \tr (P *m vec_mx v *m P *m vec_mx w).

Used by 2 declarations in 1 file

this file: logdet_sc_barrier, logdet2_sc_barrier

lemma tr_form2_linearr source, line 702

forall {R : realType} [n : nat] (P : 'M_n) (c : R) (u v w : 'rV_(n * n)),
\tr (P *m vec_mx w *m P *m vec_mx (c *: u + v)) =
c * \tr (P *m vec_mx w *m P *m vec_mx u) + \tr (P *m vec_mx w *m P *m vec_mx v)

Statement as written in the source

Lemma tr_form2_linearr n (P : 'M[R]_n) (c : R) (u v w : 'rV[R]_(n * n)) :
  \tr (P *m vec_mx w *m P *m vec_mx (c *: u + v)) =
  c * \tr (P *m vec_mx w *m P *m vec_mx u) +
  \tr (P *m vec_mx w *m P *m vec_mx v).

Used by 2 declarations in 1 file

this file: logdet_sc_barrier, logdet2_sc_barrier

theorem logdet_sc_barrier main result source, line 710

forall {R : realType} (n : nat) (s : R),
sc_barrier (sym_traceless n) (pd_slice n s) n%:R (logdet_barrier n)

Lemma 2.8 of Koehler and Sohn, one-sided: -ln det is an n-self-concordant barrier on every trace slice of the positive definite cone.

Main result, as the README states it

Lemma 2.8 of Koehler and Sohn, one-sided (Nesterov-Nemirovskii, Proposition 5.4.5): pd_slice n s is convex and relatively open with directions sym_traceless n, and logdet_barrier n is an n-self-concordant barrier on it. On pd_slice n n it is nonnegative (det A <= (tr A / n)^n), with value 0 at the identity.

Statement as written in the source

Theorem logdet_sc_barrier n (s : R) :
  sc_barrier (sym_traceless n) (pd_slice n s) n%:R (logdet_barrier n).

theorem logdet2_sc_barrier main result source, line 735

forall {R : realType} (n : nat) (m M : R),
sc_barrier (sym_traceless n) (pd_slice2 n m M) (2 * n)%:R (logdet_barrier2 n m M)

Lemma 2.8 of Koehler and Sohn, two-sided.

Main result, as the README states it

Lemma 2.8 of Koehler and Sohn, two-sided: pd_slice2 n m M is convex and relatively open with directions sym_traceless n, and logdet_barrier2 n m M is a 2n-self-concordant barrier on it; if m < 1 < M it is nonnegative there, with value 0 at the identity.

Statement as written in the source

Theorem logdet2_sc_barrier n (m M : R) :
  sc_barrier (sym_traceless n) (pd_slice2 n m M) (2 * n)%:R
    (logdet_barrier2 n m M).

lemma posdefmx_scalar source, line 785

forall {R : realType} (n : nat) [a : R], 0 < a -> posdefmx (a%:M : 'M_n)

Statement as written in the source

Lemma posdefmx_scalar n (a : R) : 0 < a -> posdefmx (a%:M : 'M[R]_n).

Used by 2 declarations in 1 file

this file: pd_slice_one, pd_slice2_one

lemma pd_slice_one source, line 791

forall {R : realType} (n : nat), pd_slice n n%:R (mxvec (1%:M : 'M_n))

Statement as written in the source

Lemma pd_slice_one n : pd_slice n n%:R (mxvec (1%:M : 'M[R]_n)).

lemma logdet_barrier_one main result source, line 797

forall {R : realType} (n : nat), logdet_barrier n (mxvec (1%:M : 'M_n)) = 0

Main result

Stated in the README together with logdet_sc_barrier.

Statement as written in the source

Lemma logdet_barrier_one n : logdet_barrier n (mxvec (1%:M : 'M[R]_n)) = 0.

lemma logdet_barrier_ge0 main result source, line 801

forall {R : realType} [n : nat] [x : 'rV_(n * n)],
pd_slice n n%:R x -> 0 <= logdet_barrier n x

det A <= (tr A / n)^n, in logarithmic form.

Main result

Stated in the README together with logdet_sc_barrier.

Statement as written in the source

Lemma logdet_barrier_ge0 n (x : 'rV[R]_(n * n)) : pd_slice n n%:R x ->
  0 <= logdet_barrier n x.

lemma ln_sub_ge source, line 820

forall {R : realType} [a b : R], 0 < a -> 0 < b -> 1 - b / a <= ln a - ln b

Statement as written in the source

Lemma ln_sub_ge (a b : R) : 0 < a -> 0 < b -> 1 - b / a <= ln a - ln b.

Used by 1 declaration in 1 file

this file: logdet_barrier2_ge0

lemma pd_slice2_one source, line 829

forall {R : realType} (n : nat) [m M : R],
m < 1 < M -> pd_slice2 n m M (mxvec (1%:M : 'M_n))

Statement as written in the source

Lemma pd_slice2_one n (m M : R) : m < 1 < M ->
  pd_slice2 n m M (mxvec (1%:M : 'M[R]_n)).

lemma logdet_barrier2_one main result source, line 838

forall {R : realType} (n : nat) [m M : R],
m < 1 < M -> logdet_barrier2 n m M (mxvec (1%:M : 'M_n)) = 0

Main result

Stated in the README together with logdet2_sc_barrier.

Statement as written in the source

Lemma logdet_barrier2_one n (m M : R) : m < 1 < M ->
  logdet_barrier2 n m M (mxvec (1%:M : 'M[R]_n)) = 0.

lemma logdet_barrier2_ge0 main result source, line 848

forall {R : realType} [n : nat] [m M : R] [x : 'rV_(n * n)],
m < 1 < M -> pd_slice2 n m M x -> 0 <= logdet_barrier2 n m M x

Main result

Stated in the README together with logdet2_sc_barrier.

Statement as written in the source

Lemma logdet_barrier2_ge0 n (m M : R) (x : 'rV[R]_(n * n)) : m < 1 < M ->
  pd_slice2 n m M x -> 0 <= logdet_barrier2 n m M x.

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.