On this page

Removing the barrier

GaussianAnalysis.convex.barrier_removallibrary/convex/barrier_removal.v177 lines5 lemmas and theoremssource

Imports 3 library modules and 18 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.classical.boolp, mathcomp.classical.classical_sets, mathcomp.classical.functions, mathcomp.reals.reals, 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

GaussianAnalysis.convex.ridge_comparison

Required by 1 files of the paper proofs

extension/Unsat/Regularized.v

Lemma 2.11 of Koehler and Sohn (arXiv 2608.27372, lines 1386-1441): the cost of a theta-self-concordant barrier B >= 0 in the least squares value is controlled by the contraction toward a reference point. Below, D is convex and relatively open with directions V, B is a theta-self-concordant barrier on D with theta >= 0 and B >= 0 on D, theta_ref is in D, b_ref is real, lambda, beta >= 0, gamma > 0 and 0 < eps < 1. F_Z is ls_objective, Phi_Z(D; beta) is ls_value and Phi_Z(D, B; beta, gamma) is ls_barrier_value (least_squares.v).

ls_objective_convex: F_Z is convex in (theta, b).

barrier_removal, Lemma 2.11: for every n-tuple of features Z,

0 <= Phi_Z(D, B; beta, gamma) - Phi_Z(D; beta)
  <= eps F_Z(theta_ref, b_ref; beta) + gamma B theta_ref
     + gamma theta ln (1 / eps).

barrier_removal_compare, (2.15): for two tuples W and G,

|Phi_W(D; beta) - Phi_G(D; beta)|
  <= |Phi_W(D, B; beta, gamma) - Phi_G(D, B; beta, gamma)|
     + eps (F_W + F_G)(theta_ref, b_ref; beta) + 2 gamma B theta_ref
     + 2 gamma theta ln (1 / eps).

Main results

Results	Statement
barrier_removalbarrier_removal_comparels_objective_convex	Lemma 2.11 of Koehler and Sohn: for `B >= 0` a `theta`-self-concordant barrier on `D` (convex, relatively open), `theta_ref` in `D`, `lambda, beta >= 0`, `gamma > 0` and `0 < eps < 1`, `0 <= Phi_Z(D, B; beta, gamma) - Phi_Z(D; beta) <= eps F_Z(theta_ref, b_ref; beta) + gamma B theta_ref + gamma theta ln (1 / eps)` for every tuple of features `Z`, by contracting toward the reference point (`F_Z` is convex); hence (2.15), the comparison of the values without barrier for two tuples `W` and `G`.

Declarations5 exported

sectionls_convexity

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

lemma sqr_convex source, line 44

forall {R : realType} (a c : R) [t : R],
0 <= t <= 1 -> ((1 - t) * a + t * c) ^+ 2 <= (1 - t) * a ^+ 2 + t * c ^+ 2

Statement as written in the source

Lemma sqr_convex (a c t : R) : 0 <= t <= 1 ->
  ((1 - t) * a + t * c) ^+ 2 <= (1 - t) * a ^+ 2 + t * c ^+ 2.

Used by 1 declaration in 1 file

this file: ls_objective_convex

lemma mxdot_convex source, line 53

forall {R : realType} {N : nat} (u v : 'rV_N) [t : R],
0 <= t <= 1 ->
mxdot ((1 - t) *: u + t *: v) ((1 - t) *: u + t *: v) <=
(1 - t) * mxdot u u + t * mxdot v v

Statement as written in the source

Lemma mxdot_convex (u v : 'rV[R]_N) (t : R) : 0 <= t <= 1 ->
  mxdot ((1 - t) *: u + t *: v) ((1 - t) *: u + t *: v) <=
  (1 - t) * mxdot u u + t * mxdot v v.

Used by 1 declaration in 1 file

this file: ls_objective_convex

lemma ls_objective_convex main result source, line 67

forall {R : realType} {N : nat} [n : nat] (Z : n.-tuple 'rV_N) 
  [lambda beta t : R] (th th' : 'rV_N) (b b' : R),
0 <= lambda ->
0 <= beta ->
0 <= t <= 1 ->
ls_objective Z lambda beta ((1 - t) *: th + t *: th') ((1 - t) * b + t * b') <=
(1 - t) * ls_objective Z lambda beta th b + t * ls_objective Z lambda beta th' b'

F_Z is convex in (theta, b).

Main result

Stated in the README together with barrier_removal.

Statement as written in the source

Lemma ls_objective_convex n (Z : n.-tuple 'rV[R]_N) (lambda beta t : R)
    (th th' : 'rV[R]_N) (b b' : R) :
  0 <= lambda -> 0 <= beta -> 0 <= t <= 1 ->
  ls_objective Z lambda beta ((1 - t) *: th + t *: th') ((1 - t) * b + t * b')
  <= (1 - t) * ls_objective Z lambda beta th b +
     t * ls_objective Z lambda beta th' b'.

Used by 1 declaration in 1 file

this file: barrier_removal

sectionbarrier_removal

Context {R : realType} {N : nat}.
Variables (V : {vspace 'rV[R]_N}) (D : set 'rV[R]_N) (theta : R)
  (B : 'rV[R]_N -> R).
Hypotheses (DV : rel_open_convex V D) (scB : sc_barrier V D theta B).
Hypotheses (theta0 : 0 <= theta) (B0 : forall z, D z -> 0 <= B z).

lemma barrier_removal main result source, line 107

forall {R : realType} {N : nat} [V : {vspace 'rV_N}] [D : set 'rV_N] 
  [theta : R] [B : 'rV_N -> R],
rel_open_convex V D ->
sc_barrier V D theta B ->
0 <= theta ->
(forall z : 'rV_N, D z -> 0 <= B z) ->
forall [n : nat] (Z : n.-tuple 'rV_N) [lambda beta gamma eps : R] [thr : 'rV_N] (br : R),
D thr ->
0 <= lambda ->
0 <= beta ->
0 < gamma ->
0 < eps < 1 ->
0 <= ls_barrier_value Z lambda beta D gamma B - ls_value Z lambda beta D <=
eps * ls_objective Z lambda beta thr br + gamma * B thr + gamma * theta * ln eps^-1

Lemma 2.11.

Main result, as the README states it

Lemma 2.11 of Koehler and Sohn: for B >= 0 a theta-self-concordant barrier on D (convex, relatively open), theta_ref in D, lambda, beta >= 0, gamma > 0 and 0 < eps < 1, 0 <= Phi_Z(D, B; beta, gamma) - Phi_Z(D; beta) <= eps F_Z(theta_ref, b_ref; beta) + gamma B theta_ref + gamma theta ln (1 / eps) for every tuple of features Z, by contracting toward the reference point (F_Z is convex); hence (2.15), the comparison of the values without barrier for two tuples W and G.

Statement as written in the source

Lemma barrier_removal n (Z : n.-tuple 'rV[R]_N) (lambda beta gamma eps : R)
    (thr : 'rV[R]_N) (br : R) :
  D thr -> 0 <= lambda -> 0 <= beta -> 0 < gamma -> 0 < eps < 1 ->
  0 <= ls_barrier_value Z lambda beta D gamma B - ls_value Z lambda beta D <=
  eps * ls_objective Z lambda beta thr br + gamma * B thr +
    gamma * theta * ln eps^-1.

Used by 2 declarations in 2 files

this file: barrier_removal_compare
GaussianAnalysis.convex.ridge_comparison: ridge_comparison

lemma barrier_removal_compare main result source, line 156

forall {R : realType} {N : nat} [V : {vspace 'rV_N}] [D : set 'rV_N] 
  [theta : R] [B : 'rV_N -> R],
rel_open_convex V D ->
sc_barrier V D theta B ->
0 <= theta ->
(forall z : 'rV_N, D z -> 0 <= B z) ->
forall [n : nat] (W G : n.-tuple 'rV_N) [lambda beta gamma eps : R] [thr : 'rV_N] (br : R),
D thr ->
0 <= lambda ->
0 <= beta ->
0 < gamma ->
0 < eps < 1 ->
`|ls_value W lambda beta D - ls_value G lambda beta D| <=
`|ls_barrier_value W lambda beta D gamma B - ls_barrier_value G lambda beta D gamma B| +
eps * (ls_objective W lambda beta thr br + ls_objective G lambda beta thr br) +
2 * gamma * B thr + 2 * gamma * theta * ln eps^-1

(2.15): the comparison of the values without barrier.

Main result

Stated in the README together with barrier_removal.

Statement as written in the source

Lemma barrier_removal_compare n (W G : n.-tuple 'rV[R]_N)
    (lambda beta gamma eps : R) (thr : 'rV[R]_N) (br : R) :
  D thr -> 0 <= lambda -> 0 <= beta -> 0 < gamma -> 0 < eps < 1 ->
  `|ls_value W lambda beta D - ls_value G lambda beta D| <=
  `|ls_barrier_value W lambda beta D gamma B -
    ls_barrier_value G lambda beta D gamma B| +
  eps * (ls_objective W lambda beta thr br + ls_objective G lambda beta thr br)
  + 2 * gamma * B thr + 2 * gamma * theta * ln eps^-1.

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.