GaussianAnalysisRocq library documentation
Main resultsGlossary
On this page
GaussianAnalysisconvexls_insertion

Inserting one feature in a barrier-regularized least squares problem

GaussianAnalysis.convex.ls_insertionlibrary/convex/ls_insertion.v807 lines39 lemmas and theorems, 12 definitionssource
Imports 7 library modules and 21 external

External: HB.structures, mathcomp.classical.all_ssreflect_compat, mathcomp.algebra.algebraic_hierarchy.ssralg, mathcomp.algebra.numeric_hierarchy.ssrnum, mathcomp.algebra.matrix, mathcomp.algebra.vector, mathcomp.algebra.sesquilinear, 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.derive, mathcomp.analysis.realfun, mathcomp.analysis.exp, mathcomp.algebra.ring_tactic, mathcomp.algebra.field_tactic, mathcomp.algebra.arithmetic_tactic

Imported by 1

The deterministic part of the Lindeberg argument of Koehler and Sohn (arXiv 2608.27372, proof of Theorem 2.9, lines 1637-2116 and 3809-4225). Fix features x_1, ..., x_n in 'rV[R]_N and an index i, a convex set D that is relatively open with directions V, a self-concordant function B >= 0 on D, and lambda, beta, gamma > 0. The leave-one-out objective is

F^(i)(theta, b) = (2 n)^-1 sum_(j <> i) (b - <x_j, theta>)^2
                  + beta (lambda |theta|^2 + b^2) + gamma B theta,

with a minimizer (theta_m, b_m) on D x R (ls_barrier_minimizer). Inserting a feature z at the place i gives the value of the full problem (ls_barrier_value of tuple_set x i z), and the insertion cost is Delta(z) = that value minus F^(i)(theta_m, b_m). Directions of V x R are written in coordinates w = (c, y) in 'rV[R]_(1 + k), for a matrix E whose k rows form an orthonormal basis of V: the direction is (y E, c).

ins_alpha E zthe row (1, - z E^T): <ins_alpha E z, w> is c - <z, y E>, the change of the residual of z
ins_hform ... w w'the Hessian of F^(i) at the minimizer, as a bilinear form of the coordinates
ins_hessian ...its matrix H^(i)
ins_ell ... zl_i(z) = <alpha(z), H^-1 alpha(z)>
ins_r ... zr_i(z) = b_m - <z, theta_m>, the residual
ins_cost ... zDelta_i(z), the insertion cost
ins_c0, ins_v, ins_Tthe coefficients of l_i as a quadratic polynomial

Main results:

  • ins_hessian_pd (Lemma 4.1): H^(i) is positive definite, with w H w^T >= 2 beta (lambda |y|^2 + c^2); ins_form_le: for a linear form w |-> c c_w + <y, h_w>, its squared H^-1 norm is at most c^2 / (2 beta) + |y|^2 / (2 beta lambda).
  • ins_taylor: the inserted objective at (theta_m + h_w, b_m + c_w) exceeds F^(i)(theta_m, b_m) by w H w^T / 2 + (r + <alpha, w>)^2 / (2 n) plus gamma times the third order remainder of B.
  • ins_cost_bounds (2.20): 0 <= Delta(z) <= r(z)^2 / (2 n).
  • ins_cost_upper, ins_cost_lower (Lemma 4.2): if 36 <= n gamma and r(z)^2 <= sqrt (n gamma), then Delta(z) differs from r(z)^2 / (2 (n + l(z))) by at most 2 |r(z)|^3 / (n sqrt (n gamma)).
  • ins_cost_quadratic (Proposition 2.14, (2.23), pointwise): if 36 <= n gamma, then for every z,
    |Delta(z) - r(z)^2 / (2 (n + l(z)))|
  <= (2 + 3 r(z)^4) / (n sqrt (n gamma)).
  • ins_ell_quadratic, ins_c0_bounds, ins_v_bound, ins_T_bounds, ins_T_sym, ins_T_frobenius (the structure behind Proposition 2.16): l(z) = c0 - 2 <v, z> + z T z^T with T symmetric, 0 <= c0 <= 1 / (2 beta), |v|^2 <= k / (4 beta^2 lambda), 0 <= z T z^T <= |z|^2 / (2 beta lambda) and |T|_F^2 <= k / (4 beta^2 lambda^2).
  • ins_size_le (Proposition 2.14, (2.21)): for theta_ref in D, beta (lambda |theta_m|^2 + b_m^2) <= (2 n)^-1 sum_(j <> i) <x_j, theta_ref>^2 + beta lambda |theta_ref|^2 + gamma B theta_ref.

Main results

ResultsStatement
ins_hessian_pdins_taylorins_cost_boundsins_cost_upperins_cost_lowerins_cost_quadratic
Lemmas 4.1 and 4.2 and Proposition 2.14, (2.23), pointwise: for the leave-one-out minimizer of the barrier-regularized problem, the Hessian H in coordinates of V x R is positive definite; the cost Delta(z) of inserting a feature z satisfies 0 <= Delta(z) <= r(z)^2 / (2 n), and if 36 <= n gamma then |Delta(z) - r(z)^2 / (2 (n + l(z)))| <= (2 + 3 r(z)^4) / (n sqrt (n gamma)), with r(z) the residual of z and l(z) = <alpha(z), H^-1 alpha(z)>.
ins_ell_quadraticins_c0_boundsins_v_boundins_T_boundsins_T_frobeniusins_size_le
l(z) = c0 - 2 <v, z> + z T z^T with T symmetric, 0 <= c0 <= 1 / (2 beta), |v|^2 <= k / (4 beta^2 lambda), 0 <= z T z^T <= |z|^2 / (2 beta lambda) and |T|_F^2 <= k / (4 beta^2 lambda^2), k = \dim V; and (2.21): beta (lambda |theta_m|^2 + b_m^2) is at most the leave-one-out objective at (theta_ref, 0).

Declarations51 exported

lemma, theoremdefinitioninstancelocal
sectionmxdot_blocks
Context {R : realType}.
lemma mxdot_row_mx source, line 83 
forall {R : realType} [m n1 n2 : nat] (a c : 'M_(m, n1)) (b d : 'M_(m, n2)),
mxdot (row_mx a b) (row_mx c d) = mxdot a c + mxdot b d
Statement as written in the source
Lemma mxdot_row_mx m n1 n2 (a c : 'M[R]_(m, n1)) (b d : 'M[R]_(m, n2)) :
  mxdot (row_mx a b) (row_mx c d) = mxdot a c + mxdot b d.
Used by 3 declarations in 1 file
sectioninsertion_defs
Context {R : realType} {N : nat}.
Variables (n : nat) (x : n.-tuple 'rV[R]_N) (i : 'I_n).
Variables (lambda beta gamma : R) (M : 'M[R]_N) (k : nat) (E : 'M[R]_(k, N)).
definition ins_alpha source, line 94
Type
forall {R : realType} {N : nat} [k : nat], 'M_(k, N) -> 'rV_N -> 'rV_(1 + k)
Definition
Definition ins_alpha (z : 'rV[R]_N) : 'rV[R]_(1 + k) :=
  row_mx (1%:M : 'M[R]_1) (- (z *m E^T)).
Used by 11 declarations in 1 file
definition ins_c source, line 98
Type
forall {R : realType} [k : nat], 'rV_(1 + k) -> R
Definition
Definition ins_c (w : 'rV[R]_(1 + k)) : R := lsubmx w 0 0.

The direction (h, c) of V x R of the coordinates w = (c, y): h = y E.

Used by 12 declarations in 1 file
definition ins_h source, line 99
Type
forall {R : realType} {N : nat} [k : nat], 'M_(k, N) -> 'rV_(1 + k) -> 'rV_N
Definition
Definition ins_h (w : 'rV[R]_(1 + k)) : 'rV[R]_N := rsubmx w *m E.
Used by 15 declarations in 1 file
definition ins_hform source, line 101
Type
forall {R : realType} {N : nat} [n : nat],
n.-tuple 'rV_N ->
'I_n ->
R -> R -> R -> 'M_N -> forall [k : nat], 'M_(k, N) -> 'rV_(1 + k) -> 'rV_(1 + k) -> R
Definition
Definition ins_hform (w w' : 'rV[R]_(1 + k)) : R :=
  2 * (n%:R *+ 2)^-1 * \sum_(j < n | j != i)
    mxdot (ins_alpha (tnth x j)) w * mxdot (ins_alpha (tnth x j)) w' +
  2 * beta * (lambda * mxdot (ins_h w) (ins_h w') + ins_c w * ins_c w') +
  gamma * mxdot (ins_h w) (ins_h w' *m M).
Used by 7 declarations in 1 file
definition ins_hessian source, line 107
Type
forall {R : realType} {N : nat} [n : nat],
n.-tuple 'rV_N -> 'I_n -> R -> R -> R -> 'M_N -> forall [k : nat], 'M_(k, N) -> 'M_(1 + k)
Definition
Definition ins_hessian : 'M[R]_(1 + k) :=
  \matrix_(p, q) ins_hform (delta_mx 0 p) (delta_mx 0 q).
Used by 15 declarations in 1 file
definition ins_ell source, line 110
Type
forall {R : realType} {N : nat} [n : nat],
n.-tuple 'rV_N -> 'I_n -> R -> R -> R -> 'M_N -> forall [k : nat], 'M_(k, N) -> 'rV_N -> R
Definition
Definition ins_ell (z : 'rV[R]_N) : R :=
  mxdot (ins_alpha z) (ins_alpha z *m invmx ins_hessian).
Used by 7 declarations in 2 files
lemma ins_alphaE source, line 113 
forall {R : realType} {N : nat} [k : nat] (E : 'M_(k, N)) (z : 'rV_N) (w : 'rV_(1 + k)),
mxdot (ins_alpha E z) w = ins_c w - mxdot z (ins_h E w)
Statement as written in the source
Lemma ins_alphaE z w : mxdot (ins_alpha z) w = ins_c w - mxdot z (ins_h w).
Used by 3 declarations in 1 file
lemma ins_c_linear source, line 119 
forall {R : realType} [k : nat] (c : R)
  (w w' : 'rV[R]_(1 + k)),
ins_c (c *: w + w') = c * ins_c w + ins_c w'
Statement as written in the source
Lemma ins_c_linear (c : R) w w' : ins_c (c *: w + w') = c * ins_c w + ins_c w'.
Used by 1 declaration in 1 file
lemma ins_h_linear source, line 122 
forall {R : realType} {N : nat} [k : nat] (E : 'M_(k, N)) (c : R)
  (w w' : 'rV[R]_(1 + k)),
ins_h E (c *: w + w') = c *: ins_h E w + ins_h E w'
Statement as written in the source
Lemma ins_h_linear (c : R) w w' : ins_h (c *: w + w') = c *: ins_h w + ins_h w'.
Used by 1 declaration in 1 file
lemma ins_hform_linearl source, line 125 
forall {R : realType} {N : nat} [n : nat] (x : n.-tuple 'rV_N) 
  (i : 'I_n) (lambda beta gamma : R) (M : 'M_N) [k : nat] (E : 'M_(k, N)) 
  (c : R) (w w' : 'rV[R]_(1 + k))
  (w'' : 'rV_(1 + k)),
ins_hform x i lambda beta gamma M E (c *: w + w') w'' =
c * ins_hform x i lambda beta gamma M E w w'' + ins_hform x i lambda beta gamma M E w' w''
Statement as written in the source
Lemma ins_hform_linearl (c : R) w w' w'' :
  ins_hform (c *: w + w') w'' = c * ins_hform w w'' + ins_hform w' w''.
Used by 1 declaration in 1 file
lemma ins_hformC source, line 140 
forall {R : realType} {N : nat} [n : nat] (x : n.-tuple 'rV_N) 
  (i : 'I_n) (lambda beta gamma : R) [M : 'M_N] [k : nat] (E : 'M_(k, N))
  (w w' : 'rV_(1 + k)),
M \is symmetricmx ->
ins_hform x i lambda beta gamma M E w w' = ins_hform x i lambda beta gamma M E w' w
Statement as written in the source
Lemma ins_hformC w w' : M \is symmetricmx -> ins_hform w w' = ins_hform w' w.
Used by 2 declarations in 1 file
lemma ins_hessianE source, line 149 
forall {R : realType} {N : nat} [n : nat] (x : n.-tuple 'rV_N) 
  (i : 'I_n) (lambda beta gamma : R) [M : 'M_N] [k : nat] (E : 'M_(k, N)) 
  (w : 'rV_(1 + k)),
M \is symmetricmx ->
mxdot w (w *m ins_hessian x i lambda beta gamma M E) =
ins_hform x i lambda beta gamma M E w w
Statement as written in the source
Lemma ins_hessianE w : M \is symmetricmx ->
  mxdot w (w *m ins_hessian) = ins_hform w w.
Used by 4 declarations in 1 file
sectioninsertion
Context {R : realType} {N : nat}.
Variables (V : {vspace 'rV[R]_N}) (D : set 'rV[R]_N) (B : 'rV[R]_N -> R).
Hypotheses (DV : rel_open_convex V D) (scB : sc_function V D B).
Hypothesis B0 : forall z, D z -> 0 <= B z.
Variables (n : nat) (x : n.-tuple 'rV[R]_N) (i : 'I_n).
Variables (lambda beta gamma : R).
Hypotheses (l0 : 0 < lambda) (b0 : 0 < beta) (g0 : 0 < gamma).
Variables (k : nat) (E : 'M[R]_(k, N)).
Hypothesis EE : E *m E^T = 1%:M.
Hypothesis EV : forall v, v \in V <-> exists y, v = y *m E.
Variables (thm : 'rV[R]_N) (bm : R) (M : 'M[R]_N).
Hypothesis Dthm : D thm.
Hypothesis thmin : forall theta b, D theta ->
  ls_barrier_objective x (fun j => j != i) (n%:R *+ 2)^-1 lambda beta gamma B
    thm bm <=
  ls_barrier_objective x (fun j => j != i) (n%:R *+ 2)^-1 lambda beta gamma B
    theta b.
Hypothesis Msym : M \is symmetricmx.
Hypothesis HM : forall h, h \in V -> 'D_h ('D_h B) thm = mxdot h (h *m M).
Local Notation s := ((n%:R *+ 2)^-1 : R).
Local Notation P := (fun j : 'I_n => j != i).
Local Notation F := (ls_barrier_objective x P s lambda beta gamma B).
Local Notation ridge := (ls_ridge x P s lambda beta).
Local Notation H := (ins_hessian x i lambda beta gamma M E).
Local Notation hform := (ins_hform x i lambda beta gamma M E).
Local Notation alpha := (ins_alpha E).
Local Notation ell := (ins_ell x i lambda beta gamma M E).
Local Notation hw := (ins_h E).
Local Notation cw := (@ins_c R k).
definition ins_r source, line 191
Type
forall {R : realType} {N : nat}, 'rV_N -> R -> 'rV_N -> R
Definition
Definition ins_r (z : 'rV[R]_N) : R := bm - mxdot z thm.

The residual of z at the minimizer, and the insertion cost of z.

Used by 5 declarations in 1 file
definition ins_cost source, line 193
Type
forall {R : realType} {N : nat},
set 'rV_N ->
('rV_N -> R) ->
forall [n : nat], n.-tuple 'rV_N -> 'I_n -> R -> R -> R -> 'rV_N -> R -> 'rV_N -> R
Definition
Definition ins_cost (z : 'rV[R]_N) : R :=
  ls_barrier_value (tuple_set x i z) lambda beta D gamma B - F thm bm.
Used by 7 declarations in 2 files
definition ins_rem source, line 197
Type
forall {R : realType} {N : nat},
('rV_N -> R) -> R -> forall [k : nat], 'M_(k, N) -> 'rV_N -> 'rV_(1 + k) -> R
Definition
Definition ins_rem (w : 'rV[R]_(1 + k)) : R :=
  gamma * (bregman_div B (thm + hw w) thm - 'D_(hw w) ('D_(hw w) B) thm / 2).

The remainder of the quadratic expansion along the direction w.

Used by 3 declarations in 1 file
lemma ins_n_gt0 source, line 200 
forall [n : nat], 'I_n -> (0 < n)%N
Statement as written in the source
Lemma ins_n_gt0 : (0 < n)%N.
Used by 1 declaration in 1 file
lemma ins_nR_gt0 source, line 203 
forall {R : realType} [n : nat], 'I_n -> 0 < (n%:R : R)
Statement as written in the source
Lemma ins_nR_gt0 : 0 < (n%:R : R).
Used by 6 declarations in 1 file
lemma ins_s_eq source, line 206 
forall {R : realType} (n : nat), ((n%:R *+ 2)^-1 : R) = (2 * n%:R)^-1
Statement as written in the source
Lemma ins_s_eq : s = (2 * n%:R)^-1.
Used by 2 declarations in 1 file
lemma ins_hV source, line 209 
forall {R : realType} {N : nat} [V : {vspace 'rV_N}] [k : nat] [E : 'M_(k, N)],
(forall v : 'rV_N, v \in V <-> (exists y : 'rV_k, v = y *m E)) ->
forall w : 'rV_(1 + k), ins_h E w \in V
Statement as written in the source
Lemma ins_hV w : hw w \in V.
Used by 5 declarations in 1 file
lemma ins_norm_h source, line 212 
forall {R : realType} {N : nat} [k : nat] [E : 'M_(k, N)],
E *m E^T = 1%:M ->
forall w : 'rV_(1 + k), mxdot (ins_h E w) (ins_h E w) = mxdot (rsubmx w) (rsubmx w)
Statement as written in the source
Lemma ins_norm_h w : mxdot (hw w) (hw w) = mxdot (rsubmx w) (rsubmx w).
Used by 2 declarations in 1 file
lemma ins_D2B_ge0 source, line 215 
forall {R : realType} {N : nat} [V : {vspace 'rV_N}] [D : set 'rV_N] [B : 'rV_N -> R],
sc_function V D B ->
forall [k : nat] [E : 'M_(k, N)],
(forall v : 'rV_N, v \in V <-> (exists y : 'rV_k, v = y *m E)) ->
forall [thm : 'rV_N],
D thm -> forall w : 'rV_(1 + k), 0 <= 'D_(ins_h E w) ('D_(ins_h E w) B) thm
Statement as written in the source
Lemma ins_D2B_ge0 w : 0 <= 'D_(hw w) ('D_(hw w) B) thm.
Used by 2 declarations in 1 file
lemma ins_hform_ridge source, line 218 
forall {R : realType} {N : nat} [V : {vspace 'rV_N}] [B : 'rV_N -> R] 
  [n : nat] (x : n.-tuple 'rV_N) (i : 'I_n) (lambda beta gamma : R) 
  [k : nat] [E : 'M_(k, N)],
(forall v : 'rV_N, v \in V <-> (exists y : 'rV_k, v = y *m E)) ->
forall [thm : 'rV_N] [M : 'M_N],
(forall h : 'rV_N, h \in V -> 'D_h ('D_h B) thm = mxdot h (h *m M)) ->
forall w : 'rV_(1 + k),
ins_hform x i lambda beta gamma M E w w =
2 *
ls_ridge x (fun j : 'I_n => j != i) ((n%:R *+ 2)^-1 : R) lambda beta (ins_h E w) (ins_c w) +
gamma * 'D_(ins_h E w) ('D_(ins_h E w) B) thm
Statement as written in the source
Lemma ins_hform_ridge w :
  hform w w = 2 * ridge (hw w) (cw w) + gamma * 'D_(hw w) ('D_(hw w) B) thm.
Used by 3 declarations in 1 file
lemma ins_ridge_ge source, line 226 
forall {R : realType} {N : nat} [n : nat] (x : n.-tuple 'rV_N) 
  (i : 'I_n) (lambda beta : R) (h : 'rV_N) (c : R),
beta * (lambda * mxdot h h + c ^+ 2) <=
ls_ridge x (fun j : 'I_n => j != i) ((n%:R *+ 2)^-1 : R) lambda beta h c
Statement as written in the source
Lemma ins_ridge_ge h c : beta * (lambda * mxdot h h + c ^+ 2) <= ridge h c.
Used by 1 declaration in 1 file
lemma ins_hform_ge source, line 233 
forall {R : realType} {N : nat} [V : {vspace 'rV_N}] [D : set 'rV_N] [B : 'rV_N -> R],
sc_function V D B ->
forall [n : nat] (x : n.-tuple 'rV_N) (i : 'I_n) (lambda beta : R) [gamma : R],
0 < gamma ->
forall [k : nat] [E : 'M_(k, N)],
E *m E^T = 1%:M ->
(forall v : 'rV_N, v \in V <-> (exists y : 'rV_k, v = y *m E)) ->
forall [thm : 'rV_N] [M : 'M_N],
D thm ->
(forall h : 'rV_N, h \in V -> 'D_h ('D_h B) thm = mxdot h (h *m M)) ->
forall w : 'rV_(1 + k),
2 * beta * (lambda * mxdot (rsubmx w) (rsubmx w) + ins_c w ^+ 2) <=
ins_hform x i lambda beta gamma M E w w
Statement as written in the source
Lemma ins_hform_ge w :
  2 * beta * (lambda * mxdot (rsubmx w) (rsubmx w) + cw w ^+ 2) <= hform w w.
Used by 2 declarations in 1 file
lemma ins_hessian_pd main result source, line 242 
forall {R : realType} {N : nat} [V : {vspace 'rV_N}] [D : set 'rV_N] [B : 'rV_N -> R],
sc_function V D B ->
forall [n : nat] (x : n.-tuple 'rV_N) (i : 'I_n) [lambda beta gamma : R],
0 < lambda ->
0 < beta ->
0 < gamma ->
forall [k : nat] [E : 'M_(k, N)],
E *m E^T = 1%:M ->
(forall v : 'rV_N, v \in V <-> (exists y : 'rV_k, v = y *m E)) ->
forall [thm : 'rV_N] [M : 'M_N],
D thm ->
M \is symmetricmx ->
(forall h : 'rV_N, h \in V -> 'D_h ('D_h B) thm = mxdot h (h *m M)) ->
posdefmx (ins_hessian x i lambda beta gamma M E)

Lemma 4.1: the Hessian at the minimizer is positive definite.

Main result, as the README states it

Lemmas 4.1 and 4.2 and Proposition 2.14, (2.23), pointwise: for the leave-one-out minimizer of the barrier-regularized problem, the Hessian H in coordinates of V x R is positive definite; the cost Delta(z) of inserting a feature z satisfies 0 <= Delta(z) <= r(z)^2 / (2 n), and if 36 <= n gamma then |Delta(z) - r(z)^2 / (2 (n + l(z)))| <= (2 + 3 r(z)^4) / (n sqrt (n gamma)), with r(z) the residual of z and l(z) = <alpha(z), H^-1 alpha(z)>.

Statement as written in the source
Lemma ins_hessian_pd : posdefmx H.
Used by 7 declarations in 1 file
lemma ins_dir source, line 261 
forall {R : realType} {N : nat} [V : {vspace 'rV_N}] [D : set 'rV_N],
rel_open_convex V D ->
forall [k : nat] [E : 'M_(k, N)],
(forall v : 'rV_N, v \in V <-> (exists y : 'rV_k, v = y *m E)) ->
forall [thm : 'rV_N] (bm : R),
D thm ->
forall [theta : 'rV_N] (b : R),
D theta -> exists w : 'rV_(1 + k), theta = thm + ins_h E w /\ b = bm + ins_c w

Every point of D x R is (thm + h, bm + c) for some coordinates w.

Statement as written in the source
Lemma ins_dir theta b : D theta ->
  exists w, theta = thm + hw w /\ b = bm + cw w.
Used by 1 declaration in 1 file
lemma ins_objective source, line 272 
forall {R : realType} {N : nat} (B : 'rV_N -> R) [n : nat] (x : n.-tuple 'rV_N) 
  (i : 'I_n) (lambda beta gamma : R) (z theta : 'rV_N) (b : R),
ls_objective (tuple_set x i z) lambda beta theta b + gamma * B theta =
ls_barrier_objective x (fun j : 'I_n => j != i) ((n%:R *+ 2)^-1 : R) lambda beta gamma B
  theta b +
((n%:R *+ 2)^-1 : R) * (b - mxdot z theta) ^+ 2

The objective of the full problem, with z at the place i.

Statement as written in the source
Lemma ins_objective z theta b :
  ls_objective (tuple_set x i z) lambda beta theta b + gamma * B theta =
  F theta b + s * (b - mxdot z theta) ^+ 2.
Used by 1 declaration in 1 file
lemma ins_taylor main result source, line 286 
forall {R : realType} {N : nat} [V : {vspace 'rV_N}] [D : set 'rV_N] [B : 'rV_N -> R],
rel_open_convex V D ->
sc_function V D B ->
forall [n : nat] [x : n.-tuple 'rV_N] [i : 'I_n] [lambda beta gamma : R] 
  [k : nat] [E : 'M_(k, N)],
(forall v : 'rV_N, v \in V <-> (exists y : 'rV_k, v = y *m E)) ->
forall [thm : 'rV_N] [bm : R] [M : 'M_N],
D thm ->
(forall (theta : 'rV_N) (b : R),
 D theta ->
 ls_barrier_objective x (fun j : 'I_n => j != i) (n%:R *+ 2)^-1 lambda beta gamma B thm bm <=
 ls_barrier_objective x (fun j : 'I_n => j != i) (n%:R *+ 2)^-1 lambda beta gamma B theta b) ->
M \is symmetricmx ->
(forall h : 'rV_N, h \in V -> 'D_h ('D_h B) thm = mxdot h (h *m M)) ->
forall (z : 'rV_N) (w : 'rV_(1 + k)),
ls_barrier_objective x (fun j : 'I_n => j != i) ((n%:R *+ 2)^-1 : R) lambda beta gamma B
  (thm + ins_h E w) (bm + ins_c w) +
((n%:R *+ 2)^-1 : R) * (bm + ins_c w - mxdot z (thm + ins_h E w)) ^+ 2 -
ls_barrier_objective x (fun j : 'I_n => j != i) ((n%:R *+ 2)^-1 : R) lambda beta gamma B
  thm bm =
mxdot w (w *m ins_hessian x i lambda beta gamma M E) / 2 + ins_rem B gamma E thm w +
(ins_r thm bm z + mxdot (ins_alpha E z) w) ^+ 2 / (2 * n%:R)

Taylor's formula for the inserted problem around the minimizer.

Main result

Stated in the README together with ins_hessian_pd.

Statement as written in the source
Lemma ins_taylor z w :
  F (thm + hw w) (bm + cw w) + s * (bm + cw w - mxdot z (thm + hw w)) ^+ 2 -
    F thm bm =
  mxdot w (w *m H) / 2 + ins_rem w +
  (ins_r z + mxdot (alpha z) w) ^+ 2 / (2 * n%:R).
Used by 2 declarations in 1 file
lemma ins_s_ge0 source, line 299 
forall {R : realType} (n : nat), 0 <= ((n%:R *+ 2)^-1 : R)
Statement as written in the source
Lemma ins_s_ge0 : 0 <= s.
Used by 4 declarations in 1 file
lemma ins_cost_set source, line 302 
forall {R : realType} {N : nat} (D : set 'rV_N) (B : 'rV_N -> R) 
  [n : nat] (x : n.-tuple 'rV_N) (i : 'I_n) (lambda beta gamma : R) 
  (thm : 'rV_N) (bm : R) (z : 'rV_N),
ins_cost D B x i lambda beta gamma thm bm z =
inf
  [set ls_barrier_objective x (fun j : 'I_n => j != i) ((n%:R *+ 2)^-1 : R) lambda beta
         gamma B theta b +
       ((n%:R *+ 2)^-1 : R) * (b - mxdot z theta) ^+ 2
     | theta in D & b in [set: R]] -
ls_barrier_objective x (fun j : 'I_n => j != i) ((n%:R *+ 2)^-1 : R) lambda beta gamma B
  thm bm
Statement as written in the source
Lemma ins_cost_set z : ins_cost z =
  inf [set F theta b + s * (b - mxdot z theta) ^+ 2 |
       theta in D & b in [set: R]] - F thm bm.
Used by 3 declarations in 1 file
lemma ins_cost_bounds main result source, line 312 
forall {R : realType} {N : nat} [D : set 'rV_N] [B : 'rV_N -> R] 
  [n : nat] [x : n.-tuple 'rV_N] [i : 'I_n] [lambda beta gamma : R] 
  [thm : 'rV_N] [bm : R],
D thm ->
(forall (theta : 'rV_N) (b : R),
 D theta ->
 ls_barrier_objective x (fun j : 'I_n => j != i) (n%:R *+ 2)^-1 lambda beta gamma B thm bm <=
 ls_barrier_objective x (fun j : 'I_n => j != i) (n%:R *+ 2)^-1 lambda beta gamma B theta b) ->
forall z : 'rV_N,
0 <= ins_cost D B x i lambda beta gamma thm bm z <= ins_r thm bm z ^+ 2 / (2 * n%:R)

(2.20): 0 <= Delta(z) <= r(z)^2 / (2 n).

Main result

Stated in the README together with ins_hessian_pd.

Statement as written in the source
Lemma ins_cost_bounds z : 0 <= ins_cost z <= ins_r z ^+ 2 / (2 * n%:R).
Used by 3 declarations in 2 files
lemma ins_rem_le source, line 327 
forall {R : realType} {N : nat} [V : {vspace 'rV_N}] [D : set 'rV_N] [B : 'rV_N -> R],
rel_open_convex V D ->
sc_function V D B ->
forall [gamma : R],
0 < gamma ->
forall [k : nat] [E : 'M_(k, N)],
(forall v : 'rV_N, v \in V <-> (exists y : 'rV_k, v = y *m E)) ->
forall [thm : 'rV_N],
D thm ->
forall [w : 'rV_(1 + k)],
sc_norm B thm (ins_h E w) <= 2^-1 ->
D (thm + ins_h E w) /\
`|ins_rem B gamma E thm w| <= gamma * (2 * sc_norm B thm (ins_h E w) ^+ 3 / 3)
Statement as written in the source
Lemma ins_rem_le w : sc_norm B thm (hw w) <= 2^-1 ->
  D (thm + hw w) /\
  `|ins_rem w| <= gamma * (2 * sc_norm B thm (hw w) ^+ 3 / 3%:R).
Used by 2 declarations in 1 file
lemma ins_sqrt_ge6 source, line 340 
forall {R : realType} [n : nat] [gamma : R],
36 <= n%:R * gamma -> 6 <= Num.ExtraDef.sqrtr (n%:R * gamma)
Statement as written in the source
Lemma ins_sqrt_ge6 : 36 <= n%:R * gamma -> 6 <= Num.sqrt (n%:R * gamma).
Used by 3 declarations in 1 file
lemma ins_cost_upper main result source, line 348 
forall {R : realType} {N : nat} [V : {vspace 'rV_N}] [D : set 'rV_N] [B : 'rV_N -> R],
rel_open_convex V D ->
sc_function V D B ->
forall [n : nat] [x : n.-tuple 'rV_N] [i : 'I_n] [lambda beta gamma : R],
0 < lambda ->
0 < beta ->
0 < gamma ->
forall [k : nat] [E : 'M_(k, N)],
E *m E^T = 1%:M ->
(forall v : 'rV_N, v \in V <-> (exists y : 'rV_k, v = y *m E)) ->
forall [thm : 'rV_N] [bm : R] [M : 'M_N],
D thm ->
(forall (theta : 'rV_N) (b : R),
 D theta ->
 ls_barrier_objective x (fun j : 'I_n => j != i) (n%:R *+ 2)^-1 lambda beta gamma B thm bm <=
 ls_barrier_objective x (fun j : 'I_n => j != i) (n%:R *+ 2)^-1 lambda beta gamma B theta b) ->
M \is symmetricmx ->
(forall h : 'rV_N, h \in V -> 'D_h ('D_h B) thm = mxdot h (h *m M)) ->
forall [z : 'rV_N],
36 <= n%:R * gamma ->
ins_r thm bm z ^+ 2 <= Num.ExtraDef.sqrtr (n%:R * gamma) ->
ins_cost D B x i lambda beta gamma thm bm z <=
ins_r thm bm z ^+ 2 / (2 * (n%:R + ins_ell x i lambda beta gamma M E z)) +
`|ins_r thm bm z| ^+ 3 / (n%:R * Num.ExtraDef.sqrtr (n%:R * gamma))

Lemma 4.2 for the optimizer of the quadratic problem: the upper bound on the insertion cost.

Main result

Stated in the README together with ins_hessian_pd.

Statement as written in the source
Lemma ins_cost_upper z : 36 <= n%:R * gamma ->
  ins_r z ^+ 2 <= Num.sqrt (n%:R * gamma) ->
  ins_cost z <= ins_r z ^+ 2 / (2 * (n%:R + ell z)) +
    `|ins_r z| ^+ 3 / (n%:R * Num.sqrt (n%:R * gamma)).
Used by 1 declaration in 1 file
lemma ins_cost_lower main result source, line 427 
forall {R : realType} {N : nat} [V : {vspace 'rV_N}] [D : set 'rV_N] [B : 'rV_N -> R],
rel_open_convex V D ->
sc_function V D B ->
forall [n : nat] [x : n.-tuple 'rV_N] [i : 'I_n] [lambda beta gamma : R],
0 < lambda ->
0 < beta ->
0 < gamma ->
forall [k : nat] [E : 'M_(k, N)],
E *m E^T = 1%:M ->
(forall v : 'rV_N, v \in V <-> (exists y : 'rV_k, v = y *m E)) ->
forall [thm : 'rV_N] [bm : R] [M : 'M_N],
D thm ->
(forall (theta : 'rV_N) (b : R),
 D theta ->
 ls_barrier_objective x (fun j : 'I_n => j != i) (n%:R *+ 2)^-1 lambda beta gamma B thm bm <=
 ls_barrier_objective x (fun j : 'I_n => j != i) (n%:R *+ 2)^-1 lambda beta gamma B theta b) ->
M \is symmetricmx ->
(forall h : 'rV_N, h \in V -> 'D_h ('D_h B) thm = mxdot h (h *m M)) ->
forall [z : 'rV_N],
36 <= n%:R * gamma ->
ins_r thm bm z ^+ 2 <= Num.ExtraDef.sqrtr (n%:R * gamma) ->
ins_r thm bm z ^+ 2 / (2 * (n%:R + ins_ell x i lambda beta gamma M E z)) -
2 * `|ins_r thm bm z| ^+ 3 / (n%:R * Num.ExtraDef.sqrtr (n%:R * gamma)) <=
ins_cost D B x i lambda beta gamma thm bm z

Lemma 4.2 for the optimizer of the exact problem: the lower bound on the insertion cost.

Main result

Stated in the README together with ins_hessian_pd.

Statement as written in the source
Lemma ins_cost_lower z : 36 <= n%:R * gamma ->
  ins_r z ^+ 2 <= Num.sqrt (n%:R * gamma) ->
  ins_r z ^+ 2 / (2 * (n%:R + ell z)) -
    2 * `|ins_r z| ^+ 3 / (n%:R * Num.sqrt (n%:R * gamma)) <= ins_cost z.
Used by 1 declaration in 1 file
lemma cube_le_quart source, line 541 
forall {R : realType} [a : R], 0 <= a -> a ^+ 3 <= 1 + a ^+ 4
Statement as written in the source
Lemma cube_le_quart (a : R) : 0 <= a -> a ^+ 3 <= 1 + a ^+ 4.
Used by 1 declaration in 1 file
lemma ins_cost_quadratic main result source, line 553 
forall {R : realType} {N : nat} [V : {vspace 'rV_N}] [D : set 'rV_N] [B : 'rV_N -> R],
rel_open_convex V D ->
sc_function V D B ->
forall [n : nat] [x : n.-tuple 'rV_N] [i : 'I_n] [lambda beta gamma : R],
0 < lambda ->
0 < beta ->
0 < gamma ->
forall [k : nat] [E : 'M_(k, N)],
E *m E^T = 1%:M ->
(forall v : 'rV_N, v \in V <-> (exists y : 'rV_k, v = y *m E)) ->
forall [thm : 'rV_N] [bm : R] [M : 'M_N],
D thm ->
(forall (theta : 'rV_N) (b : R),
 D theta ->
 ls_barrier_objective x (fun j : 'I_n => j != i) (n%:R *+ 2)^-1 lambda beta gamma B thm bm <=
 ls_barrier_objective x (fun j : 'I_n => j != i) (n%:R *+ 2)^-1 lambda beta gamma B theta b) ->
M \is symmetricmx ->
(forall h : 'rV_N, h \in V -> 'D_h ('D_h B) thm = mxdot h (h *m M)) ->
forall z : 'rV_N,
36 <= n%:R * gamma ->
`|ins_cost D B x i lambda beta gamma thm bm z -
  ins_r thm bm z ^+ 2 / (2 * (n%:R + ins_ell x i lambda beta gamma M E z))| <=
(2 + 3 * ins_r thm bm z ^+ 4) / (n%:R * Num.ExtraDef.sqrtr (n%:R * gamma))

Proposition 2.14, (2.23), pointwise: if 36 <= n gamma, then |Delta(z) - r(z)^2 / (2 (n + l(z)))| <= (2 + 3 r(z)^4) / (n sqrt (n gamma)).

Main result

Stated in the README together with ins_hessian_pd.

Statement as written in the source
Lemma ins_cost_quadratic z : 36 <= n%:R * gamma ->
  `|ins_cost z - ins_r z ^+ 2 / (2 * (n%:R + ell z))| <=
    (2 + 3%:R * ins_r z ^+ 4) / (n%:R * Num.sqrt (n%:R * gamma)).
Used by 1 declaration in 1 file
  • GaussianAnalysis.convex.barrier_lindeberg: loo_compare
lemma ins_size_le main result source, line 609 
forall {R : realType} {N : nat} [D : set 'rV_N] [B : 'rV_N -> R],
(forall z : 'rV_N, D z -> 0 <= B z) ->
forall [n : nat] [x : n.-tuple 'rV_N] [i : 'I_n] [lambda beta gamma : R],
0 < gamma ->
forall [thm : 'rV_N] [bm : R],
D thm ->
(forall (theta : 'rV_N) (b : R),
 D theta ->
 ls_barrier_objective x (fun j : 'I_n => j != i) (n%:R *+ 2)^-1 lambda beta gamma B thm bm <=
 ls_barrier_objective x (fun j : 'I_n => j != i) (n%:R *+ 2)^-1 lambda beta gamma B theta b) ->
forall [theta_ref : 'rV_N],
D theta_ref ->
beta * (lambda * mxdot thm thm + bm ^+ 2) <=
((n%:R *+ 2)^-1 : R) * \sum_(j < n | j != i) mxdot (tnth x j) theta_ref ^+ 2 +
beta * lambda * mxdot theta_ref theta_ref + gamma * B theta_ref

Proposition 2.14, (2.21): the size of the minimizer.

Main result

Stated in the README together with ins_ell_quadratic.

Statement as written in the source
Lemma ins_size_le theta_ref : D theta_ref ->
  beta * (lambda * mxdot thm thm + bm ^+ 2) <=
  s * \sum_(j < n | j != i) mxdot (tnth x j) theta_ref ^+ 2 +
  beta * lambda * mxdot theta_ref theta_ref + gamma * B theta_ref.
Used by 2 declarations in 1 file
definition ins_c0 source, line 627
Type
forall {R : realType} {N : nat} [n : nat],
n.-tuple 'rV_N -> 'I_n -> R -> R -> R -> forall [k : nat], 'M_(k, N) -> 'M_N -> R
Definition
Definition ins_c0 : R := ulsubmx (invmx H) 0 0.

The quadratic structure of l (proof of Proposition 2.16).

Used by 3 declarations in 2 files
definition ins_v source, line 628
Type
forall {R : realType} {N : nat} [n : nat],
n.-tuple 'rV_N -> 'I_n -> R -> R -> R -> forall [k : nat], 'M_(k, N) -> 'M_N -> 'rV_N
Definition
Definition ins_v : 'rV[R]_N := ursubmx (invmx H) *m E.
Used by 3 declarations in 2 files
definition ins_T source, line 629
Type
forall {R : realType} {N : nat} [n : nat],
n.-tuple 'rV_N -> 'I_n -> R -> R -> R -> forall [k : nat], 'M_(k, N) -> 'M_N -> 'M_N
Definition
Definition ins_T : 'M[R]_N := E^T *m drsubmx (invmx H) *m E.
Used by 6 declarations in 2 files
lemma ins_inv_sym source, line 631 
forall {R : realType} {N : nat} [V : {vspace 'rV_N}] [D : set 'rV_N] [B : 'rV_N -> R],
sc_function V D B ->
forall [n : nat] (x : n.-tuple 'rV_N) (i : 'I_n) [lambda beta gamma : R],
0 < lambda ->
0 < beta ->
0 < gamma ->
forall [k : nat] [E : 'M_(k, N)],
E *m E^T = 1%:M ->
(forall v : 'rV_N, v \in V <-> (exists y : 'rV_k, v = y *m E)) ->
forall [thm : 'rV_N] [M : 'M_N],
D thm ->
M \is symmetricmx ->
(forall h : 'rV_N, h \in V -> 'D_h ('D_h B) thm = mxdot h (h *m M)) ->
(invmx (ins_hessian x i lambda beta gamma M E))^T =
invmx (ins_hessian x i lambda beta gamma M E)
Statement as written in the source
Lemma ins_inv_sym : (invmx H)^T = invmx H.
Used by 3 declarations in 1 file
lemma ins_ell_quadratic main result source, line 637 
forall {R : realType} {N : nat} [V : {vspace 'rV_N}] [D : set 'rV_N] [B : 'rV_N -> R],
sc_function V D B ->
forall [n : nat] (x : n.-tuple 'rV_N) (i : 'I_n) [lambda beta gamma : R],
0 < lambda ->
0 < beta ->
0 < gamma ->
forall [k : nat] [E : 'M_(k, N)],
E *m E^T = 1%:M ->
(forall v : 'rV_N, v \in V <-> (exists y : 'rV_k, v = y *m E)) ->
forall [thm : 'rV_N] [M : 'M_N],
D thm ->
M \is symmetricmx ->
(forall h : 'rV_N, h \in V -> 'D_h ('D_h B) thm = mxdot h (h *m M)) ->
forall z : 'rV_N,
ins_ell x i lambda beta gamma M E z =
ins_c0 x i lambda beta gamma E M - 2 * mxdot (ins_v x i lambda beta gamma E M) z +
mxdot z (z *m ins_T x i lambda beta gamma E M)
Main result, as the README states it

l(z) = c0 - 2 <v, z> + z T z^T with T symmetric, 0 <= c0 <= 1 / (2 beta), |v|^2 <= k / (4 beta^2 lambda), 0 <= z T z^T <= |z|^2 / (2 beta lambda) and |T|_F^2 <= k / (4 beta^2 lambda^2), k = \dim V; and (2.21): beta (lambda |theta_m|^2 + b_m^2) is at most the leave-one-out objective at (theta_ref, 0).

Statement as written in the source
Lemma ins_ell_quadratic z :
  ell z = ins_c0 - 2 * mxdot ins_v z + mxdot z (z *m ins_T).
Used by 3 declarations in 2 files
lemma ins_form_le source, line 663 
forall {R : realType} {N : nat} [V : {vspace 'rV_N}] [D : set 'rV_N] [B : 'rV_N -> R],
sc_function V D B ->
forall [n : nat] (x : n.-tuple 'rV_N) (i : 'I_n) [lambda beta gamma : R],
0 < lambda ->
0 < beta ->
0 < gamma ->
forall [k : nat] [E : 'M_(k, N)],
E *m E^T = 1%:M ->
(forall v : 'rV_N, v \in V <-> (exists y : 'rV_k, v = y *m E)) ->
forall [thm : 'rV_N] [M : 'M_N],
D thm ->
M \is symmetricmx ->
(forall h : 'rV_N, h \in V -> 'D_h ('D_h B) thm = mxdot h (h *m M)) ->
forall [a : 'rV_(1 + k)] [c : R] [y : 'rV_N],
(forall w : 'rV_(1 + k), mxdot a w = c * ins_c w + mxdot y (ins_h E w)) ->
mxdot a (a *m invmx (ins_hessian x i lambda beta gamma M E)) <=
c ^+ 2 / (2 * beta) + mxdot y y / (2 * beta * lambda)

The variational bound behind Lemma 4.1: for a linear form w |-> c c_w + <y, h_w>, its squared H^-1 norm is at most c^2 / (2 beta) + |y|^2 / (2 beta lambda).

Statement as written in the source
Lemma ins_form_le (a : 'rV[R]_(1 + k)) (c : R) (y : 'rV[R]_N) :
  (forall w, mxdot a w = c * cw w + mxdot y (hw w)) ->
  mxdot a (a *m invmx H) <=
  c ^+ 2 / (2 * beta) + mxdot y y / (2 * beta * lambda).
Used by 2 declarations in 1 file
lemma ins_ell_ge0 source, line 697 
forall {R : realType} {N : nat} [V : {vspace 'rV_N}] [D : set 'rV_N] [B : 'rV_N -> R],
sc_function V D B ->
forall [n : nat] (x : n.-tuple 'rV_N) (i : 'I_n) [lambda beta gamma : R],
0 < lambda ->
0 < beta ->
0 < gamma ->
forall [k : nat] [E : 'M_(k, N)],
E *m E^T = 1%:M ->
(forall v : 'rV_N, v \in V <-> (exists y : 'rV_k, v = y *m E)) ->
forall [thm : 'rV_N] [M : 'M_N],
D thm ->
M \is symmetricmx ->
(forall h : 'rV_N, h \in V -> 'D_h ('D_h B) thm = mxdot h (h *m M)) ->
forall z : 'rV_N, 0 <= ins_ell x i lambda beta gamma M E z
Statement as written in the source
Lemma ins_ell_ge0 z : 0 <= ell z.
Used by 3 declarations in 2 files
lemma ins_c0_bounds main result source, line 700 
forall {R : realType} {N : nat} [V : {vspace 'rV_N}] [D : set 'rV_N] [B : 'rV_N -> R],
sc_function V D B ->
forall [n : nat] (x : n.-tuple 'rV_N) (i : 'I_n) [lambda beta gamma : R],
0 < lambda ->
0 < beta ->
0 < gamma ->
forall [k : nat] [E : 'M_(k, N)],
E *m E^T = 1%:M ->
(forall v : 'rV_N, v \in V <-> (exists y : 'rV_k, v = y *m E)) ->
forall [thm : 'rV_N] [M : 'M_N],
D thm ->
M \is symmetricmx ->
(forall h : 'rV_N, h \in V -> 'D_h ('D_h B) thm = mxdot h (h *m M)) ->
0 <= ins_c0 x i lambda beta gamma E M <= (2 * beta)^-1
Main result

Stated in the README together with ins_ell_quadratic.

Statement as written in the source
Lemma ins_c0_bounds : 0 <= ins_c0 <= (2 * beta)^-1.
Used by 1 declaration in 1 file
lemma ins_T_bounds main result source, line 710 
forall {R : realType} {N : nat} [V : {vspace 'rV_N}] [D : set 'rV_N] [B : 'rV_N -> R],
sc_function V D B ->
forall [n : nat] (x : n.-tuple 'rV_N) (i : 'I_n) [lambda beta gamma : R],
0 < lambda ->
0 < beta ->
0 < gamma ->
forall [k : nat] [E : 'M_(k, N)],
E *m E^T = 1%:M ->
(forall v : 'rV_N, v \in V <-> (exists y : 'rV_k, v = y *m E)) ->
forall [thm : 'rV_N] [M : 'M_N],
D thm ->
M \is symmetricmx ->
(forall h : 'rV_N, h \in V -> 'D_h ('D_h B) thm = mxdot h (h *m M)) ->
forall z : 'rV_N,
0 <= mxdot z (z *m ins_T x i lambda beta gamma E M) <= mxdot z z / (2 * beta * lambda)
Main result

Stated in the README together with ins_ell_quadratic.

Statement as written in the source
Lemma ins_T_bounds (z : 'rV[R]_N) :
  0 <= mxdot z (z *m ins_T) <= mxdot z z / (2 * beta * lambda).
Used by 2 declarations in 1 file
lemma ins_T_sym source, line 728 
forall {R : realType} {N : nat} [V : {vspace 'rV_N}] [D : set 'rV_N] [B : 'rV_N -> R],
sc_function V D B ->
forall [n : nat] (x : n.-tuple 'rV_N) (i : 'I_n) [lambda beta gamma : R],
0 < lambda ->
0 < beta ->
0 < gamma ->
forall [k : nat] [E : 'M_(k, N)],
E *m E^T = 1%:M ->
(forall v : 'rV_N, v \in V <-> (exists y : 'rV_k, v = y *m E)) ->
forall [thm : 'rV_N] [M : 'M_N],
D thm ->
M \is symmetricmx ->
(forall h : 'rV_N, h \in V -> 'D_h ('D_h B) thm = mxdot h (h *m M)) ->
ins_T x i lambda beta gamma E M \is symmetricmx
Statement as written in the source
Lemma ins_T_sym : ins_T \is symmetricmx.
Used by 2 declarations in 2 files
lemma ins_v_bound main result source, line 734 
forall {R : realType} {N : nat} [V : {vspace 'rV_N}] [D : set 'rV_N] [B : 'rV_N -> R],
sc_function V D B ->
forall [n : nat] (x : n.-tuple 'rV_N) (i : 'I_n) [lambda beta gamma : R],
0 < lambda ->
0 < beta ->
0 < gamma ->
forall [k : nat] [E : 'M_(k, N)],
E *m E^T = 1%:M ->
(forall v : 'rV_N, v \in V <-> (exists y : 'rV_k, v = y *m E)) ->
forall [thm : 'rV_N] [M : 'M_N],
D thm ->
M \is symmetricmx ->
(forall h : 'rV_N, h \in V -> 'D_h ('D_h B) thm = mxdot h (h *m M)) ->
mxdot (ins_v x i lambda beta gamma E M) (ins_v x i lambda beta gamma E M) <=
k%:R / (4 * beta ^+ 2 * lambda)
Main result

Stated in the README together with ins_ell_quadratic.

Statement as written in the source
Lemma ins_v_bound : mxdot ins_v ins_v <= k%:R / (4 * beta ^+ 2 * lambda).
Used by 1 declaration in 1 file
  • GaussianAnalysis.convex.barrier_lindeberg: loo_compare
lemma ins_T_frobenius main result source, line 761 
forall {R : realType} {N : nat} [V : {vspace 'rV_N}] [D : set 'rV_N] [B : 'rV_N -> R],
sc_function V D B ->
forall [n : nat] (x : n.-tuple 'rV_N) (i : 'I_n) [lambda beta gamma : R],
0 < lambda ->
0 < beta ->
0 < gamma ->
forall [k : nat] [E : 'M_(k, N)],
E *m E^T = 1%:M ->
(forall v : 'rV_N, v \in V <-> (exists y : 'rV_k, v = y *m E)) ->
forall [thm : 'rV_N] [M : 'M_N],
D thm ->
M \is symmetricmx ->
(forall h : 'rV_N, h \in V -> 'D_h ('D_h B) thm = mxdot h (h *m M)) ->
mxdot (ins_T x i lambda beta gamma E M) (ins_T x i lambda beta gamma E M) <=
k%:R / (4 * beta ^+ 2 * lambda ^+ 2)
Main result

Stated in the README together with ins_ell_quadratic.

Statement as written in the source
Lemma ins_T_frobenius :
  mxdot ins_T ins_T <= k%:R / (4 * beta ^+ 2 * lambda ^+ 2).
Used by 1 declaration in 1 file
  • GaussianAnalysis.convex.barrier_lindeberg: loo_compare
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.