On this page

Minimizers of least squares objectives with a barrier

GaussianAnalysis.convex.minimizerslibrary/convex/minimizers.v640 lines18 lemmas and theorems, 2 definitionssource

Imports 6 library modules and 20 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.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 3

Required by 1 files of the paper proofs

extension/Sat/ApproximateFit.v

The convex analysis that the Lindeberg argument of Koehler and Sohn (arXiv 2608.27372, Theorem 2.9) needs, for the objective

F(theta, b) = s sum_(i in P) (b - <Z_i, theta>)^2
              + beta (lambda |theta|^2 + b^2) + gamma B theta

on D x R (ls_barrier_objective of least_squares.v), where D is relatively open and convex with directions V (rel_open_convex), B >= 0 is a self-concordant function on D (sc_function), s >= 0 and lambda, beta, gamma > 0. D need not be bounded: the ridge term makes F coercive.

`ls_grad Z P s lambda beta theta b h c`	the first variation of the ridge objective at (theta, b) in the direction (h, c)
`ls_bopt Z P s beta theta`	the b that minimizes the ridge objective for a fixed theta

Main results:

vspace_orthonormal: every subspace V of 'rV[R]_N is the row space of a matrix E with orthonormal rows (E E^T = I, of \dim V rows); closed_vspace: V is closed.
rel_open_convex_closure: for z in D and y in the closure of D, y - z is in V and z + t (y - z) is in D for 0 <= t < 1.
sc_sublevel_closed, sc_minimizer: for g continuous, convex on D and nonnegative, the sublevel sets of g + gamma B in D are closed (the barrier tends to +oo at the relative boundary); if moreover g z >= kappa |z|^2 with kappa > 0, then g + gamma B attains its minimum on D.
ls_barrier_minimizer: F attains its minimum on D x R.
ls_first_order: at a minimizer (theta, b), the derivative of F along every direction (h, c) of V x R is 0.
ls_taylor (paper, (2.17)-(2.18)): at a minimizer, for h in V, F (theta + h) (b + c) - F theta b = ridge(h, c) + gamma bregman_div B (theta + h) theta, ridge being the quadratic part of F.
quad_response (paper, (2.19)): for H symmetric positive definite, a row vector a and nn > 0, the infimum over u of u H u^T / 2 + (r + <a, u>)^2 / (2 nn) is r^2 / (2 (nn + l)) with l = a H^-1 a^T, attained at u0 = - (r / (nn + l)) a H^-1, where u0 H u0^T = l r^2 / (nn + l)^2; and 2 <a, u> - u H u^T <= l for all u.

Main results

Results	Statement
vspace_orthonormalclosed_vspacerel_open_convex_closure	Every subspace `V` of `'rV[R]_N` is the row space of a matrix with `\dim V` orthonormal rows, and is closed; for `D` convex and relatively open with directions `V`, `z` in `D` and `y` in the closure of `D`, `y - z` is in `V` and `z + t (y - z)` is in `D` for `0 <= t < 1`.
sc_sublevel_closedsc_minimizerls_barrier_minimizer	For `B >= 0` a self-concordant function on `D` and `g` continuous, convex on `D` and nonnegative, the sublevel sets of `g + gamma B` in `D` are closed, and if `g z >= kappa \|z\|^2` with `kappa > 0` then `g + gamma B` attains its minimum on `D` (`D` need not be bounded). In particular the least squares objective with a barrier attains its minimum on `D x R`.
ls_first_orderls_taylorquad_response	At a minimizer `(theta, b)` the derivative along every direction of `V x R` is 0, and `F (theta + h) (b + c) - F theta b` is the quadratic part at `(h, c)` plus `gamma` times the Bregman divergence of `B` (Koehler-Sohn, (2.17)-(2.18)). For `H` positive definite, the infimum over `u` of `u H u^T / 2 + (r + <a, u>)^2 / (2 nn)` is `r^2 / (2 (nn + l))` with `l = a H^-1 a^T` ((2.19)).

Declarations20 exported

sectionorthonormal_basis

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

lemma vspace_orthonormal main result source, line 71

forall {R : realType} {N : nat} (V : {vspace 'rV_N}),
exists E : 'M_(\dim V, N),
  E *m E^T = 1%:M /\ (forall v : 'rV_N, v \in V <-> (exists y : 'rV_(\dim V), v = y *m E))

A subspace V of 'rV[R]_N is the row space of a matrix with orthonormal rows: the basis vbasis V made orthonormal by G^(-1/2), G its Gram matrix.

Main result, as the README states it

Every subspace V of 'rV[R]_N is the row space of a matrix with \dim V orthonormal rows, and is closed; for D convex and relatively open with directions V, z in D and y in the closure of D, y - z is in V and z + t (y - z) is in D for 0 <= t < 1.

Statement as written in the source

Lemma vspace_orthonormal (V : {vspace 'rV[R]_N}) :
  exists E : 'M[R]_(\dim V, N),
    E *m E^T = 1%:M /\ forall v, v \in V <-> exists y, v = y *m E.

Used by 4 declarations in 3 files

GaussianAnalysis.probability.measurable_minimizer: rel_open_dense_seq
this file: closed_vspace
GaussianAnalysis.convex.barrier_lindeberg: measurable_inf_rel_open, loo_compare

sectionsublevel

Context {R : realType} {N : nat}.
Implicit Types (V : {vspace 'rV[R]_N}) (D : set 'rV[R]_N).

lemma closed_vspace main result source, line 126

forall {R : realType} {N : nat} [V : {vspace 'rV_N}], closed [set` V]

Main result

Stated in the README together with vspace_orthonormal.

Statement as written in the source

Lemma closed_vspace V : closed [set v : 'rV[R]_N | v \in V].

Used by 1 declaration in 1 file

this file: rel_open_convex_closure

lemma rel_open_convex_closure main result source, line 143

forall {R : realType} {N : nat} [V : {vspace 'rV_N}] [D : set 'rV_N] 
  [z : 'rV_N]
  [y : 'rV[R]_N],
rel_open_convex V D ->
D z -> closure D y -> y - z \in V /\ (forall t : R, 0 <= t < 1 -> D (z + t *: (y - z)))

The points of the closure of D are in z + V, and the segment from a point of D to them stays in D up to its end.

Main result

Stated in the README together with vspace_orthonormal.

Statement as written in the source

Lemma rel_open_convex_closure V D z y : rel_open_convex V D -> D z ->
  closure D y ->
  y - z \in V /\ forall t : R, 0 <= t < 1 -> D (z + t *: (y - z)).

Used by 1 declaration in 1 file

this file: sc_sublevel_closed

lemma sc_sublevel_closed main result source, line 190

forall {R : realType} {N : nat} [V : {vspace 'rV_N}] [D : set 'rV_N] 
  [B g : 'rV_N -> R] [gamma c : R],
rel_open_convex V D ->
sc_function V D B ->
0 < gamma ->
continuous g ->
(forall (z y : 'rV_N) (t : R),
 D z -> D y -> 0 <= t <= 1 -> g (z + t *: (y - z)) <= (1 - t) * g z + t * g y) ->
(forall z : 'rV_N, D z -> 0 <= B z) ->
(forall z : 'rV_N, 0 <= g z) -> closed [set z | D z /\ g z + gamma * B z <= c]

If B is a self-concordant function on D and g is continuous and convex on D, then the sublevel sets of g + gamma B in D are closed.

Main result, as the README states it

For B >= 0 a self-concordant function on D and g continuous, convex on D and nonnegative, the sublevel sets of g + gamma B in D are closed, and if g z >= kappa |z|^2 with kappa > 0 then g + gamma B attains its minimum on D (D need not be bounded). In particular the least squares objective with a barrier attains its minimum on D x R.

Statement as written in the source

Lemma sc_sublevel_closed V D (B g : 'rV[R]_N -> R) (gamma c : R) :
  rel_open_convex V D -> sc_function V D B -> 0 < gamma -> continuous g ->
  (forall z y (t : R), D z -> D y -> 0 <= t <= 1 ->
     g (z + t *: (y - z)) <= (1 - t) * g z + t * g y) ->
  (forall z, D z -> 0 <= B z) -> (forall z, 0 <= g z) ->
  closed [set z | D z /\ g z + gamma * B z <= c].

Used by 1 declaration in 1 file

this file: sc_minimizer

lemma sc_minimizer main result source, line 268

forall {R : realType} {N : nat} [V : {vspace 'rV_N}] [D : set 'rV_N] 
  [B g : 'rV_N -> R] [gamma kappa : R],
rel_open_convex V D ->
sc_function V D B ->
0 < gamma ->
0 < kappa ->
continuous g ->
(forall (z y : 'rV_N) (t : R),
 D z -> D y -> 0 <= t <= 1 -> g (z + t *: (y - z)) <= (1 - t) * g z + t * g y) ->
(forall z : 'rV_N, D z -> 0 <= B z) ->
(forall z : 'rV_N, kappa * mxdot z z <= g z) ->
D !=set0 ->
exists2 zm : 'rV_N,
  D zm & forall z : 'rV_N, D z -> g zm + gamma * B zm <= g z + gamma * B z

Existence of a minimizer of g + gamma B on D, for g continuous, convex on D and coercive, and B >= 0 a self-concordant function on D.

Main result

Stated in the README together with sc_sublevel_closed.

Statement as written in the source

Lemma sc_minimizer V D (B g : 'rV[R]_N -> R) (gamma kappa : R) :
  rel_open_convex V D -> sc_function V D B -> 0 < gamma -> 0 < kappa ->
  continuous g ->
  (forall z y (t : R), D z -> D y -> 0 <= t <= 1 ->
     g (z + t *: (y - z)) <= (1 - t) * g z + t * g y) ->
  (forall z, D z -> 0 <= B z) -> (forall z, kappa * mxdot z z <= g z) ->
  D !=set0 ->
  exists2 zm, D zm & forall z, D z -> g zm + gamma * B zm <= g z + gamma * B z.

Used by 2 declarations in 2 files

GaussianAnalysis.probability.measurable_minimizer: ls_min_exists
this file: ls_barrier_minimizer

sectionls_expansion

Context {R : realType} {N : nat}.
Variables (n : nat) (Z : n.-tuple 'rV[R]_N) (P : pred 'I_n).
Variables (s lambda beta : R).

definition ls_grad source, line 326

Type

forall {R : realType} {N : nat} [n : nat],
n.-tuple 'rV_N -> pred 'I_n -> R -> R -> R -> 'rV_N -> R -> 'rV_N -> R -> R

Definition

Definition ls_grad (theta : 'rV[R]_N) (b : R) (h : 'rV[R]_N) (c : R) : R :=
  2 * s * \sum_(i < n | P i)
    (b - mxdot (tnth Z i) theta) * (c - mxdot (tnth Z i) h) +
  2 * beta * (lambda * mxdot theta h + b * c).

The first variation of the ridge least squares objective at (theta, b) in the direction (h, c).

Used by 5 declarations in 1 file

this file: ls_ridge_expand, ls_ridge_bopt, convex_ls_reduced, ls_first_order, ls_taylor

lemma ls_ridge_expand source, line 332

forall {R : realType} {N : nat} [n : nat] (Z : n.-tuple 'rV_N) 
  (P : pred 'I_n) (s lambda beta t : R)
  (theta : 'rV[R]_N) (b : R)
  (h : 'rV[R]_N) (c : R),
ls_ridge Z P s lambda beta (theta + t *: h) (b + t * c) =
ls_ridge Z P s lambda beta theta b + t * ls_grad Z P s lambda beta theta b h c +
t ^+ 2 * ls_ridge Z P s lambda beta h c

The objective is quadratic: its expansion along a line is exact.

Statement as written in the source

Lemma ls_ridge_expand (t : R) theta b h c :
  ls_ridge Z P s lambda beta (theta + t *: h) (b + t * c) =
  ls_ridge Z P s lambda beta theta b + t * ls_grad theta b h c +
  t ^+ 2 * ls_ridge Z P s lambda beta h c.

Used by 4 declarations in 1 file

this file: ls_ridge_bopt, convex_ls_reduced, ls_first_order, ls_taylor

definition ls_bopt source, line 350

Type

forall {R : realType} {N : nat} [n : nat],
n.-tuple 'rV_N -> pred 'I_n -> R -> R -> 'rV_N -> R

Definition

Definition ls_bopt (theta : 'rV[R]_N) : R :=
  s * (\sum_(i < n | P i) mxdot (tnth Z i) theta) / (s * #|P|%:R + beta).

Used by 14 declarations in 3 files

GaussianAnalysis.probability.measurable_minimizer: ls_reduced, ls_min_exists, ls_minP, ls_min_growth, measurable_ls_bopt_min, ls_bopt_tuple_set
this file: ls_ridge_bopt, ls_bopt_linear, continuous_ls_reduced, convex_ls_reduced, ls_barrier_minimizer
GaussianAnalysis.convex.barrier_lindeberg: measurable_ls_reduced, ls_barrier_valueE, measurable_ls_barrier_value

lemma ls_ridge_bopt source, line 353

forall {R : realType} {N : nat} [n : nat] (Z : n.-tuple 'rV_N) 
  [P : pred 'I_n] [s : R] (lambda : R) [beta : R] (theta : 'rV_N) 
  (b : R),
0 < s * #|P|%:R + beta ->
ls_ridge Z P s lambda beta theta b =
ls_ridge Z P s lambda beta theta (ls_bopt Z P s beta theta) +
(s * #|P|%:R + beta) * (b - ls_bopt Z P s beta theta) ^+ 2

Statement as written in the source

Lemma ls_ridge_bopt theta b : 0 < s * #|P|%:R + beta ->
  ls_ridge Z P s lambda beta theta b =
  ls_ridge Z P s lambda beta theta (ls_bopt theta) +
  (s * #|P|%:R + beta) * (b - ls_bopt theta) ^+ 2.

Used by 4 declarations in 3 files

GaussianAnalysis.probability.measurable_minimizer: ls_reduced_le
this file: convex_ls_reduced, ls_barrier_minimizer
GaussianAnalysis.convex.barrier_lindeberg: ls_barrier_valueE

sectionls_minimizer

Context {R : realType} {N : nat}.
Variables (V : {vspace 'rV[R]_N}) (D : set 'rV[R]_N) (B : 'rV[R]_N -> R).
Variables (n : nat) (Z : n.-tuple 'rV[R]_N) (P : pred 'I_n).
Variables (s lambda beta gamma : R).
Hypotheses (DV : rel_open_convex V D) (scB : sc_function V D B).
Hypotheses (B0 : forall z, D z -> 0 <= B z).
Hypotheses (s0 : 0 <= s) (l0 : 0 < lambda) (b0 : 0 < beta) (g0 : 0 < gamma).
Local Notation ridge := (ls_ridge Z P s lambda beta).
Local Notation F := (ls_barrier_objective Z P s lambda beta gamma B).
Local Notation bopt := (ls_bopt Z P s beta).
Local Notation grad := (ls_grad Z P s lambda beta).

lemma ls_A0 source, line 398

forall {R : realType} [n : nat] (P : pred 'I_n) [s beta : R],
0 <= s -> 0 < beta -> 0 < s * #|P|%:R + beta

Statement as written in the source

Lemma ls_A0 : 0 < s * #|P|%:R + beta.

Used by 3 declarations in 2 files

GaussianAnalysis.probability.measurable_minimizer: ls_reduced_le
this file: convex_ls_reduced, ls_barrier_minimizer

lemma ls_ridge_ge0 source, line 401

forall {R : realType} {N : nat} [n : nat] (Z : n.-tuple 'rV_N) 
  (P : pred 'I_n) [s lambda beta : R],
0 <= s ->
0 < lambda ->
0 < beta -> forall (theta : 'rV_N) (b : R), 0 <= ls_ridge Z P s lambda beta theta b

Statement as written in the source

Lemma ls_ridge_ge0 theta b : 0 <= ridge theta b.

Used by 3 declarations in 2 files

this file: convex_ls_reduced
GaussianAnalysis.convex.ls_insertion: ins_cost_upper, ins_cost_lower

lemma ls_ridge_coercive source, line 409

forall {R : realType} {N : nat} [n : nat] (Z : n.-tuple 'rV_N) 
  (P : pred 'I_n) [s : R] (lambda : R) [beta : R],
0 <= s ->
0 < beta ->
forall (theta : 'rV_N) (b : R),
beta * lambda * mxdot theta theta <= ls_ridge Z P s lambda beta theta b

Statement as written in the source

Lemma ls_ridge_coercive theta b :
  beta * lambda * mxdot theta theta <= ridge theta b.

Used by 3 declarations in 2 files

GaussianAnalysis.probability.measurable_minimizer: ls_min_exists, ls_min_growth
this file: ls_barrier_minimizer

lemma ls_bopt_linear source, line 417

forall {R : realType} {N : nat} [n : nat] (Z : n.-tuple 'rV_N) 
  (P : pred 'I_n) (s beta c : R) (u v : 'rV_N),
ls_bopt Z P s beta (c *: u + v) = c * ls_bopt Z P s beta u + ls_bopt Z P s beta v

Statement as written in the source

Lemma ls_bopt_linear (c : R) (u v : 'rV[R]_N) :
  bopt (c *: u + v) = c * bopt u + bopt v.

Used by 1 declaration in 1 file

this file: continuous_ls_reduced

lemma continuous_ls_reduced source, line 427

forall {R : realType} {N : nat} [n : nat] [Z : n.-tuple 'rV_N] 
  [P : pred 'I_n] [s lambda beta : R],
continuous
  (fun
     theta : 'rV[R]_N =>
   ls_ridge Z P s lambda beta theta (ls_bopt Z P s beta theta))

The reduced objective theta |-> ridge theta (bopt theta) is a quadratic form, hence continuous.

Statement as written in the source

Lemma continuous_ls_reduced :
  continuous (fun theta => ridge theta (bopt theta)).

Used by 4 declarations in 3 files

GaussianAnalysis.probability.measurable_minimizer: ls_min_exists, measurable_ls_min
this file: ls_barrier_minimizer
GaussianAnalysis.convex.barrier_lindeberg: measurable_ls_barrier_value

lemma convex_ls_reduced source, line 458

forall {R : realType} {N : nat} [n : nat] (Z : n.-tuple 'rV_N) 
  (P : pred 'I_n) [s lambda beta : R],
0 <= s ->
0 < lambda ->
0 < beta ->
forall (z y : 'rV[R]_N) [t : R],
0 <= t <= 1 ->
ls_ridge Z P s lambda beta (z + t *: (y - z)) (ls_bopt Z P s beta (z + t *: (y - z))) <=
(1 - t) * ls_ridge Z P s lambda beta z (ls_bopt Z P s beta z) +
t * ls_ridge Z P s lambda beta y (ls_bopt Z P s beta y)

Statement as written in the source

Lemma convex_ls_reduced z y (t : R) : 0 <= t <= 1 ->
  ridge (z + t *: (y - z)) (bopt (z + t *: (y - z))) <=
  (1 - t) * ridge z (bopt z) + t * ridge y (bopt y).

Used by 2 declarations in 2 files

GaussianAnalysis.probability.measurable_minimizer: ls_min_exists
this file: ls_barrier_minimizer

lemma ls_barrier_minimizer main result source, line 478

forall {R : realType} {N : nat} [V : {vspace 'rV_N}] [D : set 'rV_N] 
  [B : 'rV_N -> R] [n : nat] (Z : n.-tuple 'rV_N) (P : pred 'I_n) 
  [s lambda beta gamma : R],
rel_open_convex V D ->
sc_function V D B ->
(forall z : 'rV_N, D z -> 0 <= B z) ->
0 <= s ->
0 < lambda ->
0 < beta ->
0 < gamma ->
D !=set0 ->
exists (theta : 'rV_N) (b : R),
  D theta /\
  (forall (theta' : 'rV_N) (b' : R),
   D theta' ->
   ls_barrier_objective Z P s lambda beta gamma B theta b <=
   ls_barrier_objective Z P s lambda beta gamma B theta' b')

Existence of a minimizer of the objective on D x R.

Main result

Stated in the README together with sc_sublevel_closed.

Statement as written in the source

Lemma ls_barrier_minimizer : D !=set0 ->
  exists theta : 'rV[R]_N, exists b : R,
    D theta /\ forall theta' b', D theta' -> F theta b <= F theta' b'.

Used by 2 declarations in 1 file

GaussianAnalysis.convex.barrier_lindeberg: loo_compare, loo_variance

sectionat_minimizer

Variables (theta : 'rV[R]_N) (b : R).
Hypotheses (Dtheta : D theta)
  (thmin : forall theta' b', D theta' -> F theta b <= F theta' b').

lemma ls_first_order main result source, line 501

forall {R : realType} {N : nat} [V : {vspace 'rV_N}] [D : set 'rV_N] 
  [B : 'rV_N -> R] [n : nat] [Z : n.-tuple 'rV_N] [P : pred 'I_n] 
  [s lambda beta gamma : R],
rel_open_convex V D ->
sc_function V D B ->
forall [theta : 'rV_N] [b : R],
D theta ->
(forall (theta' : 'rV_N) (b' : R),
 D theta' ->
 ls_barrier_objective Z P s lambda beta gamma B theta b <=
 ls_barrier_objective Z P s lambda beta gamma B theta' b') ->
forall [h : 'rV_N] (c : R),
h \in V -> ls_grad Z P s lambda beta theta b h c + gamma * 'D_h B theta = 0

The first order condition.

Main result, as the README states it

At a minimizer (theta, b) the derivative along every direction of V x R is 0, and F (theta + h) (b + c) - F theta b is the quadratic part at (h, c) plus gamma times the Bregman divergence of B (Koehler-Sohn, (2.17)-(2.18)). For H positive definite, the infimum over u of u H u^T / 2 + (r + <a, u>)^2 / (2 nn) is r^2 / (2 (nn + l)) with l = a H^-1 a^T ((2.19)).

Statement as written in the source

Lemma ls_first_order h c : h \in V ->
  grad theta b h c + gamma * 'D_h B theta = 0.

Used by 1 declaration in 1 file

this file: ls_taylor

lemma ls_taylor main result source, line 537

forall {R : realType} {N : nat} [V : {vspace 'rV_N}] [D : set 'rV_N] 
  [B : 'rV_N -> R] [n : nat] [Z : n.-tuple 'rV_N] [P : pred 'I_n] 
  [s lambda beta gamma : R],
rel_open_convex V D ->
sc_function V D B ->
forall [theta : 'rV_N] [b : R],
D theta ->
(forall (theta' : 'rV_N) (b' : R),
 D theta' ->
 ls_barrier_objective Z P s lambda beta gamma B theta b <=
 ls_barrier_objective Z P s lambda beta gamma B theta' b') ->
forall [h : 'rV_N] (c : R),
h \in V ->
ls_barrier_objective Z P s lambda beta gamma B (theta + h) (b + c) -
ls_barrier_objective Z P s lambda beta gamma B theta b =
ls_ridge Z P s lambda beta h c + gamma * bregman_div B (theta + h) theta

Taylor's formula at the minimizer: the objective is quadratic up to the Bregman divergence of the barrier (paper, (2.17)-(2.18)).

Main result

Stated in the README together with ls_first_order.

Statement as written in the source

Lemma ls_taylor h c : h \in V ->
  F (theta + h) (b + c) - F theta b =
  ridge h c + gamma * bregman_div B (theta + h) theta.

Used by 3 declarations in 2 files

GaussianAnalysis.probability.measurable_minimizer: ls_min_growth
GaussianAnalysis.convex.ls_insertion: ins_taylor, ins_cost_lower

sectionquadratic_response

Context {R : realType} {k : nat}.
Implicit Types (H : 'M[R]_k) (a u v w : 'rV[R]_k).

lemma posdefmx_unit source, line 559

forall {R : realType} {k : nat} [H : 'M_k], posdefmx H -> H \in unitmx

Statement as written in the source

Lemma posdefmx_unit H : posdefmx H -> H \in unitmx.

Used by 2 declarations in 2 files

this file: quad_response
GaussianAnalysis.convex.ls_insertion: ins_form_le

lemma quad_response main result source, line 575

forall {R : realType} {k : nat} [H : 'M_k] (a : 'rV_k) (r : R) [nn : R],
posdefmx H ->
0 < nn ->
let l := mxdot a (a *m invmx H) in
let u0 := - (r / (nn + l)) *: (a *m invmx H) in
[/\ 0 <= l, forall u : 'rV_k, 2 * mxdot a u - mxdot u (u *m H) <= l,
    forall u : 'rV_k,
    r ^+ 2 / (2 * (nn + l)) <= mxdot u (u *m H) / 2 + (r + mxdot a u) ^+ 2 / (2 * nn),
    mxdot u0 (u0 *m H) / 2 + (r + mxdot a u0) ^+ 2 / (2 * nn) = r ^+ 2 / (2 * (nn + l))
  & mxdot u0 (u0 *m H) = l * r ^+ 2 / (nn + l) ^+ 2]

For H symmetric positive definite, a row vector a and nn > 0, the quadratic problem inf_u { u H u^T / 2 + (r + <a, u>)^2 / (2 nn) } has value r^2 / (2 (nn + l)), l = a H^-1 a^T, attained at u0 = - (r / (nn + l)) a H^-1 (paper, (2.19)); and l = sup_u (2 <a, u> - u H u^T).

Main result

Stated in the README together with ls_first_order.

Statement as written in the source

Lemma quad_response H a (r nn : R) : posdefmx H -> 0 < nn ->
  let l := mxdot a (a *m invmx H) in
  let u0 := (- (r / (nn + l))) *: (a *m invmx H) in
  [/\ 0 <= l, forall u, 2 * mxdot a u - mxdot u (u *m H) <= l,
      forall u, r ^+ 2 / (2 * (nn + l)) <=
        mxdot u (u *m H) / 2 + (r + mxdot a u) ^+ 2 / (2 * nn),
      mxdot u0 (u0 *m H) / 2 + (r + mxdot a u0) ^+ 2 / (2 * nn) =
        r ^+ 2 / (2 * (nn + l)) &
      mxdot u0 (u0 *m H) = l * r ^+ 2 / (nn + l) ^+ 2].

Used by 5 declarations in 1 file

GaussianAnalysis.convex.ls_insertion: ins_cost_upper, ins_cost_lower, ins_cost_quadratic, ins_ell_ge0, ins_T_bounds

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.