On this page

Self-concordant functions and barriers

GaussianAnalysis.convex.self_concordantlibrary/convex/self_concordant.v1,247 lines41 lemmas and theorems, 7 definitionssource

Imports 2 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 7

Required by 3 files of the paper proofs

Self-concordant functions and barriers in the sense of Nesterov and Nemirovskii (Interior-point polynomial algorithms, Definition 2.3.1), on a convex set D of 'rV[R]_N that is open in its affine hull z + V, with V a subspace. Derivatives are taken along the directions h of V, with MathComp's directional derivative 'D_h. A self-concordant function is convex, three times differentiable along V, its first and second derivatives are a linear and a quadratic form, it tends to +oo at the relative boundary of D, and

(SC)  |D^3 B(z)[h, h, h]| <= 2 (D^2 B(z)[h, h])^(3/2),

written (D^3 B(z)[h, h, h])^2 <= 4 (D^2 B(z)[h, h])^3. A theta-self-concordant barrier satisfies moreover

(BP)  (D B(z)[h])^2 <= theta D^2 B(z)[h, h].

These are the notions of Koehler and Sohn, Universality and sharp thresholds for ellipsoid fitting (arXiv 2608.27372), Definition 2.7.

`rel_open_convex V D`	D is convex, y - z is in V for y, z in D, and around each z of D, D contains the points z + h with h in V and `\|h\| < e for some e > 0: D is relatively open in its affine hull z + V
`sc_function V D B`	B is a self-concordant function on D with directions V: three times differentiable along V, with a gradient vector and a Hessian matrix, convex, (SC), and B (z + t h) tends to +oo when t tends to 1 from the left, if z + t h is in D for 0 <= t < 1 and z + h is not
`sc_barrier V D theta B`	B is a theta-self-concordant barrier: a self-concordant function with (BP)
`sc_norm B z h`	the local norm sqrt (D^2 B(z)[h, h])
`bregman_div B y z`	the Bregman divergence B y - B z - D B(z)[y - z]
`sc_omega r`	r - ln (1 + r)
`sc_omega_star r`	- r - ln (1 - r)

Main results, for D relatively open and convex with directions V, B a self-concordant function on D, z in D, h in V and r = sc_norm B z h:

sc_hessian_line_ge, sc_hessian_line_le: for t >= 0 with z + t h in D, r^2 / (1 + t r)^2 <= D^2 B(z + t h)[h, h], and D^2 B(z + t h)[h, h] is at most r^2 / (1 - t r)^2 when moreover t r < 1 (Koehler-Sohn, proof of Lemma 2.15); the one-dimensional comparison is sc_ode_ge, sc_ode_le.
sc_dikin: the Dikin ellipsoid: if r < 1, then z + h is in D (Nesterov-Nemirovskii, Theorem 2.1.1).
sc_bregman_ge, sc_bregman_le: sc_omega r <= bregman_div B (z + h) z when z + h is in D, and bregman_div B (z + h) z <= sc_omega_star r when r < 1.
sc_bregman_small (Lemma 2.15 (i)): if z + h is in D and bregman_div B (z + h) z <= sc_omega (1/2), then r <= 1/2 and r^2 / 3 <= bregman_div B (z + h) z.
sc_taylor3 (Lemma 2.15 (ii)): if r <= 1/2, then z + h is in D and |B (z + h) - B z - D B(z)[h] - r^2 / 2| <= 2 r^3 / 3.
sc_function_convex, sc_function_continuous: B is convex on D, and continuous at every point of D for the points of D.
sc_barrier_grad_le (Lemma 2.10, Nesterov Theorem 4.2.4): for a theta-self-concordant barrier with theta >= 0 and y, z in D, D B(z)[y - z] <= theta.
sc_barrier_contraction (Lemma 2.10): for x0, x in D and 0 < eps < 1, B ((1 - eps) x + eps x0) <= B x0 + theta ln (1 / eps).
line_derive3: if B agrees on the line through z along h with a function of one variable with three derivatives, these are the derivatives of B along h at the points of the line in D; with lin_form_vec and bilin_form_mx (a linear form is mxdot g h and a bilinear form is h M h^T), this reduces the conditions of sc_function to facts in one variable (convex/logdet_barrier.v).

Main results

Results	Statement
rel_open_convexsc_functionsc_barriersc_normbregman_div	Self-concordant functions and barriers (Nesterov-Nemirovskii; Koehler-Sohn, Definition 2.7) on a convex set `D` of `'rV[R]_N` that is relatively open in `z + V` for a subspace `V`: derivatives along the directions of `V` (MathComp's `'D_h`) up to order 3, a gradient vector and a Hessian matrix, convexity, `(D^3 B[h,h,h])^2 <= 4 (D^2 B[h,h])^3`, and `B` tends to `+oo` along segments that leave `D`; a `theta`-barrier also has `(D B[h])^2 <= theta D^2 B[h,h]`. `sc_norm B z h` is the local norm `sqrt (D^2 B(z)[h,h])`, `bregman_div B y z = B y - B z - D B(z)[y - z]`.
sc_hessian_line_gesc_hessian_line_lesc_ode_gesc_ode_le	Along a segment `z + t h` in `D`, with `r = sc_norm B z h`: `r^2 / (1 + t r)^2 <= D^2 B(z + t h)[h,h]`, and `D^2 B(z + t h)[h,h] <= r^2 / (1 - t r)^2` when `t r < 1`. The one-dimensional comparison behind it compares `1 / sqrt (psi + e)` with `t` for a function `psi >= 0` with `psi'^2 <= 4 psi^3`.
sc_dikin	The Dikin ellipsoid: if `sc_norm B z h < 1` then `z + h` is in `D` (Nesterov-Nemirovskii, Theorem 2.1.1); proved from the bound above and the blow-up of `B` at the exit point of the segment.
sc_bregman_gesc_bregman_lesc_bregman_smallsc_taylor3	Lemma 2.15 of Koehler and Sohn: `r - ln (1 + r) <= bregman_div B (z + h) z` when `z + h` is in `D`, and `bregman_div B (z + h) z <= - r - ln (1 - r)` when `r < 1`; hence (i) if the Bregman divergence is at most `1/2 - ln (3/2)` then `r <= 1/2` and it is at least `r^2 / 3`, and (ii) if `r <= 1/2` then `z + h` is in `D` and `\|B (z + h) - B z - D B(z)[h] - r^2 / 2\| <= 2 r^3 / 3`.
sc_function_convexsc_function_continuous	A self-concordant function is convex on `D`, and continuous at every point of `D` for the points of `D`.
sc_barrier_grad_lesc_barrier_contraction	Lemma 2.10 of Koehler and Sohn, for a `theta`-self-concordant barrier with `theta >= 0`: `D B(z)[y - z] <= theta` for `y`, `z` in `D` (Nesterov, Theorem 4.2.4), and `B ((1 - eps) x + eps x0) <= B x0 + theta ln (1 / eps)` for `x0`, `x` in `D` and `0 < eps < 1`.
derive_ge0_lederive_le0_lederive2_ge0_tangent	Monotonicity on `[a, b]` from the sign of the derivative, and a function with a nonnegative second derivative on `[a, b]` lies above its tangents there.
line_derive3lin_form_vecbilin_form_mx	If `B` agrees on `D`, along the line through `z` in the direction `h` of `V`, with a function of one variable that has three derivatives, these are the derivatives of `B` along `h` at the points of the line in `D`. A linear form on row vectors is `mxdot g h` and a bilinear form `Q` has `Q h h = h M h^T`, for the vector and the matrix of their values on the basis.

Declarations48 exported

sectionself_concordant_definitions

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

definition rel_open_convex main result source, line 92

Type

forall {R : realType} {N : nat}, {vspace 'rV_N} -> set 'rV_N -> Prop

Definition

Definition rel_open_convex V D :=
  [/\ forall z y (t : R), D z -> D y -> 0 <= t <= 1 -> D (z + t *: (y - z)),
      forall z y, D z -> D y -> y - z \in V &
      forall z, D z -> exists2 e : R, 0 < e &
        forall h, h \in V -> `|h| < e -> D (z + h)].

Main result, as the README states it

Self-concordant functions and barriers (Nesterov-Nemirovskii; Koehler-Sohn, Definition 2.7) on a convex set D of 'rV[R]_N that is relatively open in z + V for a subspace V: derivatives along the directions of V (MathComp's 'D_h) up to order 3, a gradient vector and a Hessian matrix, convexity, (D^3 B[h,h,h])^2 <= 4 (D^2 B[h,h])^3, and B tends to +oo along segments that leave D; a theta-barrier also has (D B[h])^2 <= theta D^2 B[h,h]. sc_norm B z h is the local norm sqrt (D^2 B(z)[h,h]), bregman_div B y z = B y - B z - D B(z)[y - z].

Used by 9 declarations in 5 files

GaussianAnalysis.probability.measurable_minimizer: rel_open_dense_seq
GaussianAnalysis.convex.logdet_barrier: rel_open_convex_pd_slice, rel_open_convex_pd_slice2, logsum_sc_barrier
GaussianAnalysis.convex.minimizers: rel_open_convex_closure, sc_sublevel_closed, sc_minimizer
GaussianAnalysis.convex.barrier_lindeberg: measurable_inf_rel_open
GaussianAnalysis.convex.ridge_comparison: measurable_ls_value

definition sc_function main result source, line 98

Type

forall {R : realType} {N : nat}, {vspace 'rV_N} -> set 'rV_N -> ('rV_N -> R) -> Prop

Definition

Definition sc_function V D B :=
  [/\ forall z h, D z -> h \in V ->
        [/\ derivable B z h, derivable ('D_h B) z h &
            derivable ('D_h ('D_h B)) z h],
      forall z, D z -> exists (g : 'rV[R]_N) (M : 'M[R]_N),
        forall h, h \in V ->
          'D_h B z = mxdot g h /\ 'D_h ('D_h B) z = mxdot h (h *m M),
      forall z h, D z -> h \in V -> 0 <= 'D_h ('D_h B) z,
      forall z h, D z -> h \in V ->
        ('D_h ('D_h ('D_h B)) z) ^+ 2 <= 4%:R * ('D_h ('D_h B) z) ^+ 3 &
      forall z h, D z -> h \in V ->
        (forall t, 0 <= t < 1 -> D (z + t *: h)) -> ~ D (z + h) ->
        B (z + t *: h) @[t --> (1 : R)^'-] --> +oo].

Main result

Stated in the README together with rel_open_convex.

Used by 3 declarations in 2 files

this file: sc_barrier
GaussianAnalysis.convex.minimizers: sc_sublevel_closed, sc_minimizer

definition sc_barrier main result source, line 112

Type

forall {R : realType} {N : nat}, {vspace 'rV_N} -> set 'rV_N -> R -> ('rV_N -> R) -> Prop

Definition

Definition sc_barrier V D (theta : R) B :=
  sc_function V D B /\
  forall z h, D z -> h \in V -> ('D_h B z) ^+ 2 <= theta * 'D_h ('D_h B) z.

Main result

Stated in the README together with rel_open_convex.

Used by 3 declarations in 1 file

GaussianAnalysis.convex.logdet_barrier: logsum_sc_barrier, logdet_sc_barrier, logdet2_sc_barrier

definition sc_norm main result source, line 116

Type

forall {R : realType} {N : nat}, ('rV_N -> R) -> 'rV_N -> 'rV_N -> R

Definition

Definition sc_norm B (z h : 'rV[R]_N) : R := Num.sqrt ('D_h ('D_h B) z).

Main result

Stated in the README together with rel_open_convex.

Used by 11 declarations in 2 files

this file: sc_hessian_line_ge, sc_hessian_line_le, sc_dikin, sc_bregman_ge, sc_bregman_le, sc_bregman_small, sc_taylor3, sc_function_continuous
GaussianAnalysis.convex.ls_insertion: ins_rem_le, ins_cost_upper, ins_cost_lower

definition bregman_div main result source, line 118

Type

forall {R : realType} {N : nat}, ('rV_N -> R) -> 'rV_N -> 'rV_N -> R

Definition

Definition bregman_div B (y z : 'rV[R]_N) : R := B y - B z - 'D_(y - z) B z.

Main result

Stated in the README together with rel_open_convex.

Used by 9 declarations in 4 files

GaussianAnalysis.probability.measurable_minimizer: ls_min_growth
this file: bregman_div_add, sc_bregman_ge, sc_bregman_le, sc_bregman_small
GaussianAnalysis.convex.minimizers: ls_taylor
GaussianAnalysis.convex.ls_insertion: ins_rem, ins_rem_le, ins_cost_lower

definition sc_omega source, line 120

Type

forall {R : realType}, R -> R

Definition

Definition sc_omega (r : R) : R := r - ln (1 + r).

Used by 10 declarations in 2 files

this file: is_derive_sc_omega, sc_omega0, sc_omega_ge0, sc_omega_ge, sc_omega_le, sc_omega_taylor, sc_omega_gt_half, sc_bregman_ge, sc_bregman_small
GaussianAnalysis.convex.ls_insertion: ins_cost_lower

definition sc_omega_star source, line 122

Type

forall {R : realType}, R -> R

Definition

Definition sc_omega_star (r : R) : R := - r - ln (1 - r).

Used by 4 declarations in 1 file

this file: is_derive_sc_omega_star, sc_omega_star0, sc_omega_star_taylor, sc_bregman_le

sectionone_dimensional

Context {R : realType}.
Implicit Types (f df : R -> R) (a b : R).

lemma derive_ge0_le main result source, line 132

forall {R : realType} [f df : R -> R] [a b : R],
a <= b ->
(forall x : R, a <= x <= b -> is_derive x 1 f (df x)) ->
(forall x : R, a <= x <= b -> 0 <= df x) -> f a <= f b

A function with a nonnegative derivative on [a, b] is nondecreasing on [a, b].

Main result, as the README states it

Monotonicity on [a, b] from the sign of the derivative, and a function with a nonnegative second derivative on [a, b] lies above its tangents there.

Statement as written in the source

Lemma derive_ge0_le f df a b : a <= b ->
  (forall x, a <= x <= b -> is_derive x 1 f (df x)) ->
  (forall x, a <= x <= b -> 0 <= df x) -> f a <= f b.

Used by 10 declarations in 1 file

this file: derive_le0_le, derive2_ge0_tangent, sc_ode_inv, sc_omega_ge0, sc_omega_ge, sc_omega_le, sc_omega_taylor, sc_omega_star_taylor, sc_omega_gt_half, sc_barrier_grad_le

lemma derive_le0_le main result source, line 150

forall {R : realType} [f df : R -> R] [a b : R],
a <= b ->
(forall x : R, a <= x <= b -> is_derive x 1 f (df x)) ->
(forall x : R, a <= x <= b -> df x <= 0) -> f b <= f a

A function with a nonpositive derivative on [a, b] is nonincreasing on [a, b].

Main result

Stated in the README together with derive_ge0_le.

Statement as written in the source

Lemma derive_le0_le f df a b : a <= b ->
  (forall x, a <= x <= b -> is_derive x 1 f (df x)) ->
  (forall x, a <= x <= b -> df x <= 0) -> f b <= f a.

Used by 4 declarations in 1 file

this file: derive2_ge0_tangent, sc_ode_inv, sc_barrier_grad_le, sc_barrier_contraction

lemma derive2_ge0_tangent main result source, line 162

forall {R : realType} [f f1 f2 : R -> R] [a b s t : R],
(forall x : R, a <= x <= b -> is_derive x 1 f (f1 x)) ->
(forall x : R, a <= x <= b -> is_derive x 1 f1 (f2 x)) ->
(forall x : R, a <= x <= b -> 0 <= f2 x) ->
a <= s <= b -> a <= t <= b -> f t + f1 t * (s - t) <= f s

A function whose second derivative is nonnegative on [a, b] lies above its tangents there.

Main result

Stated in the README together with derive_ge0_le.

Statement as written in the source

Lemma derive2_ge0_tangent f f1 f2 a b s t :
  (forall x, a <= x <= b -> is_derive x 1 f (f1 x)) ->
  (forall x, a <= x <= b -> is_derive x 1 f1 (f2 x)) ->
  (forall x, a <= x <= b -> 0 <= f2 x) ->
  a <= s <= b -> a <= t <= b -> f t + f1 t * (s - t) <= f s.

Used by 4 declarations in 1 file

this file: sc_line_taylor_le, sc_bregman_ge, sc_bregman_le, sc_function_convex

lemma sc_ode_inv source, line 196

forall {R : realType} [psi dpsi : R -> R] [T e : R],
0 <= T ->
0 < e ->
(forall x : join_Num_POrderNmodule_between_Algebra_BaseAddUMagma_and_Order_Preorder R,
 0 <= x <= T -> is_derive x 1 psi (dpsi x)) ->
(forall x : join_Num_POrderNmodule_between_Algebra_BaseAddUMagma_and_Order_Preorder R,
 0 <= x <= T -> 0 <= psi x) ->
(forall x : join_Num_POrderNmodule_between_Algebra_BaseAddUMagma_and_Order_Preorder R,
 0 <= x <= T -> dpsi x ^+ 2 <= 4 * psi x ^+ 3) ->
(Num.ExtraDef.sqrtr (psi T + e))^-1 - T <= (Num.ExtraDef.sqrtr (psi 0 + e))^-1 <=
(Num.ExtraDef.sqrtr (psi T + e))^-1 + T

The comparison behind Lemma 2.15 of Koehler and Sohn: let psi >= 0 have the derivative dpsi on [0, T] with dpsi^2 <= 4 psi^3. Then for e > 0, t |-> 1 / sqrt (psi t + e) has a derivative of absolute value at most 1 on [0, T].

Statement as written in the source

Lemma sc_ode_inv (psi dpsi : R -> R) (T e : R) : 0 <= T -> 0 < e ->
  (forall x, 0 <= x <= T -> is_derive x 1 psi (dpsi x)) ->
  (forall x, 0 <= x <= T -> 0 <= psi x) ->
  (forall x, 0 <= x <= T -> dpsi x ^+ 2 <= 4%:R * psi x ^+ 3) ->
  (Num.sqrt (psi T + e))^-1 - T <= (Num.sqrt (psi 0 + e))^-1 <=
    (Num.sqrt (psi T + e))^-1 + T.

Used by 2 declarations in 1 file

this file: sc_ode_ge, sc_ode_le

lemma sc_ode_ge main result source, line 250

forall {R : realType} [psi dpsi : R -> R] [T : R],
0 <= T ->
(forall x : join_Num_POrderNmodule_between_Algebra_BaseAddUMagma_and_Order_Preorder R,
 0 <= x <= T -> is_derive x 1 psi (dpsi x)) ->
(forall x : join_Num_POrderNmodule_between_Algebra_BaseAddUMagma_and_Order_Preorder R,
 0 <= x <= T -> 0 <= psi x) ->
(forall x : join_Num_POrderNmodule_between_Algebra_BaseAddUMagma_and_Order_Preorder R,
 0 <= x <= T -> dpsi x ^+ 2 <= 4 * psi x ^+ 3) ->
psi 0 / (1 + T * Num.ExtraDef.sqrtr (psi 0)) ^+ 2 <= psi T

Then r^2 / (1 + t r)^2 <= psi t, and psi t <= r^2 / (1 - t r)^2 when t r < 1, for t = T and r^2 = psi 0.

Main result

Stated in the README together with sc_hessian_line_ge.

Statement as written in the source

Lemma sc_ode_ge (psi dpsi : R -> R) (T : R) : 0 <= T ->
  (forall x, 0 <= x <= T -> is_derive x 1 psi (dpsi x)) ->
  (forall x, 0 <= x <= T -> 0 <= psi x) ->
  (forall x, 0 <= x <= T -> dpsi x ^+ 2 <= 4%:R * psi x ^+ 3) ->
  psi 0 / (1 + T * Num.sqrt (psi 0)) ^+ 2 <= psi T.

Used by 1 declaration in 1 file

this file: sc_hessian_line_ge

lemma sc_ode_le main result source, line 281

forall {R : realType} [psi dpsi : R -> R] [T : R],
0 <= T ->
(forall x : join_Num_POrderNmodule_between_Algebra_BaseAddUMagma_and_Order_Preorder R,
 0 <= x <= T -> is_derive x 1 psi (dpsi x)) ->
(forall x : join_Num_POrderNmodule_between_Algebra_BaseAddUMagma_and_Order_Preorder R,
 0 <= x <= T -> 0 <= psi x) ->
(forall x : join_Num_POrderNmodule_between_Algebra_BaseAddUMagma_and_Order_Preorder R,
 0 <= x <= T -> dpsi x ^+ 2 <= 4 * psi x ^+ 3) ->
T * Num.ExtraDef.sqrtr (psi 0) < 1 ->
psi T <= psi 0 / (1 - T * Num.ExtraDef.sqrtr (psi 0)) ^+ 2

Main result

Stated in the README together with sc_hessian_line_ge.

Statement as written in the source

Lemma sc_ode_le (psi dpsi : R -> R) (T : R) : 0 <= T ->
  (forall x, 0 <= x <= T -> is_derive x 1 psi (dpsi x)) ->
  (forall x, 0 <= x <= T -> 0 <= psi x) ->
  (forall x, 0 <= x <= T -> dpsi x ^+ 2 <= 4%:R * psi x ^+ 3) ->
  T * Num.sqrt (psi 0) < 1 ->
  psi T <= psi 0 / (1 - T * Num.sqrt (psi 0)) ^+ 2.

Used by 1 declaration in 1 file

this file: sc_hessian_line_le

lemma is_derive_sc_omega source, line 343

forall {R : realType} [x : R], -1 < x -> is_derive x 1 sc_omega (x / (1 + x))

The derivatives of omega and omega_star, and of the functions t |-> omega (t r) and t |-> omega_star (t r) of the Bregman bounds.

Statement as written in the source

Lemma is_derive_sc_omega (x : R) : -1 < x ->
  is_derive x 1 sc_omega (x / (1 + x)).

Used by 5 declarations in 1 file

this file: sc_omega_ge0, sc_omega_ge, sc_omega_le, sc_omega_taylor, sc_omega_gt_half

lemma is_derive_sc_omega_star source, line 358

forall {R : realType} [x : R], x < 1 -> is_derive x 1 sc_omega_star (x / (1 - x))

Statement as written in the source

Lemma is_derive_sc_omega_star (x : R) : x < 1 ->
  is_derive x 1 sc_omega_star (x / (1 - x)).

Used by 1 declaration in 1 file

this file: sc_omega_star_taylor

lemma is_derive_omega_line source, line 373

forall {R : realType} [r t : R],
0 < 1 + t * r ->
is_derive t 1
  (fun s : R =>
   s * r - ln (1 + s * r))
  (r - r / (1 + t * r))

Statement as written in the source

Lemma is_derive_omega_line (r t : R) : 0 < 1 + t * r ->
  is_derive t 1 (fun s => s * r - ln (1 + s * r)) (r - r / (1 + t * r)).

Used by 1 declaration in 1 file

this file: sc_bregman_ge

lemma is_derive_omega_line1 source, line 390

forall {R : realType} [r t : R],
0 < 1 + t * r ->
is_derive t 1
  (fun s : R =>
   r - r / (1 + s * r))
  (r ^+ 2 / (1 + t * r) ^+ 2)

Statement as written in the source

Lemma is_derive_omega_line1 (r t : R) : 0 < 1 + t * r ->
  is_derive t 1 (fun s => r - r / (1 + s * r)) (r ^+ 2 / (1 + t * r) ^+ 2).

Used by 1 declaration in 1 file

this file: sc_bregman_ge

lemma is_derive_omega_star_line source, line 405

forall {R : realType} [r t : R],
0 < 1 - t * r ->
is_derive t 1
  (fun s : R =>
   - (s * r) - ln (1 - s * r))
  (r / (1 - t * r) - r)

Statement as written in the source

Lemma is_derive_omega_star_line (r t : R) : 0 < 1 - t * r ->
  is_derive t 1 (fun s => - (s * r) - ln (1 - s * r)) (r / (1 - t * r) - r).

Used by 1 declaration in 1 file

this file: sc_bregman_le

lemma is_derive_omega_star_line1 source, line 423

forall {R : realType} [r t : R],
0 < 1 - t * r ->
is_derive t 1
  (fun s : R =>
   r / (1 - s * r) - r)
  (r ^+ 2 / (1 - t * r) ^+ 2)

Statement as written in the source

Lemma is_derive_omega_star_line1 (r t : R) : 0 < 1 - t * r ->
  is_derive t 1 (fun s => r / (1 - s * r) - r) (r ^+ 2 / (1 - t * r) ^+ 2).

Used by 1 declaration in 1 file

this file: sc_bregman_le

lemma sc_omega0 source, line 438

forall {R : realType}, sc_omega (0 : R) = 0

Statement as written in the source

Lemma sc_omega0 : sc_omega (0 : R) = 0.

Used by 4 declarations in 1 file

this file: sc_omega_ge0, sc_omega_ge, sc_omega_le, sc_omega_taylor

lemma sc_omega_star0 source, line 441

forall {R : realType}, sc_omega_star (0 : R) = 0

Statement as written in the source

Lemma sc_omega_star0 : sc_omega_star (0 : R) = 0.

Used by 1 declaration in 1 file

this file: sc_omega_star_taylor

lemma sc_omega_ge0 source, line 444

forall {R : realType} [r : R], 0 <= r -> 0 <= sc_omega r

Statement as written in the source

Lemma sc_omega_ge0 (r : R) : 0 <= r -> 0 <= sc_omega r.

Used by 1 declaration in 1 file

GaussianAnalysis.probability.measurable_minimizer: ls_min_growth

lemma sc_omega_ge source, line 454

forall {R : realType} [r : R], 0 <= r -> r <= 2^-1 -> r ^+ 2 / 3 <= sc_omega r

r^2 / 3 <= omega r <= r^2 / 2 for 0 <= r <= 1/2, and the Taylor bounds of order 3 that the second part of Lemma 2.15 uses.

Statement as written in the source

Lemma sc_omega_ge (r : R) : 0 <= r -> r <= 2^-1 -> r ^+ 2 / 3%:R <= sc_omega r.

Used by 2 declarations in 2 files

this file: sc_bregman_small
GaussianAnalysis.convex.ls_insertion: ins_cost_lower

lemma sc_omega_le source, line 475

forall {R : realType} [r : R], 0 <= r -> sc_omega r <= r ^+ 2 / 2

Statement as written in the source

Lemma sc_omega_le (r : R) : 0 <= r -> sc_omega r <= r ^+ 2 / 2.

lemma sc_omega_taylor source, line 492

forall {R : realType} [r : R], 0 <= r -> r ^+ 2 / 2 - r ^+ 3 / 3 <= sc_omega r

Statement as written in the source

Lemma sc_omega_taylor (r : R) : 0 <= r ->
  r ^+ 2 / 2 - r ^+ 3 / 3%:R <= sc_omega r.

Used by 1 declaration in 1 file

this file: sc_taylor3

lemma sc_omega_star_taylor source, line 512

forall {R : realType} [r : R],
0 <= r -> r <= 2^-1 -> sc_omega_star r <= r ^+ 2 / 2 + 2 * r ^+ 3 / 3

Statement as written in the source

Lemma sc_omega_star_taylor (r : R) : 0 <= r -> r <= 2^-1 ->
  sc_omega_star r <= r ^+ 2 / 2 + 2 * r ^+ 3 / 3%:R.

Used by 1 declaration in 1 file

this file: sc_taylor3

lemma sc_omega_gt_half source, line 534

forall {R : realType} [r : R], 2^-1 < r -> sc_omega 2^-1 < sc_omega r

Statement as written in the source

Lemma sc_omega_gt_half (r : R) : 2^-1 < r -> sc_omega 2^-1 < sc_omega r.

Used by 1 declaration in 1 file

this file: sc_bregman_small

sectionline

Context {R : realType} {N : nat}.
Implicit Types (f : 'rV[R]_N -> R) (a h : 'rV[R]_N).

lemma is_derive_line source, line 559

forall {R : realType} {N : nat} [f : 'rV_N -> R] [a h : 'rV_N] [t : R],
derivable f (a + t *: h) h ->
is_derive t 1
  (fun s : R =>
   f (a + s *: h))
  ('D_h f (a + t *: h))

The derivative of t |-> f (a + t h) at t is the derivative of f at a + t h along h.

Statement as written in the source

Lemma is_derive_line f a h (t : R) : derivable f (a + t *: h) h ->
  is_derive t 1 (fun s => f (a + s *: h)) ('D_h f (a + t *: h)).

Used by 2 declarations in 2 files

this file: sc_line_derive
GaussianAnalysis.convex.minimizers: ls_first_order

lemma is_derive_line_inv source, line 575

forall {R : realType} {N : nat} [f : 'rV_N -> R] [a h : 'rV_N] [t d : R],
is_derive t 1
  (fun s : R =>
   f (a + s *: h))
  d ->
is_derive (a + t *: h) h f d

Conversely, a derivative of t |-> f (a + t h) is a derivative of f along h.

Statement as written in the source

Lemma is_derive_line_inv f a h (t d : R) :
  is_derive t 1 (fun s => f (a + s *: h)) d -> is_derive (a + t *: h) h f d.

Used by 1 declaration in 1 file

this file: line_derive3

lemma lin_form_vec main result source, line 592

forall {R : realType} [k : nat] [L : 'rV_k -> R],
(forall (c : R) (u v : 'rV_k), L (c *: u + v) = c * L u + L v) ->
forall u : 'rV_k, L u = mxdot (\row_j L (delta_mx 0 j)) u

A linear form on row vectors is the inner product with the row of its values on the basis, and a bilinear form is h M h^T for the matrix of its values on the basis.

Main result

Stated in the README together with line_derive3.

Statement as written in the source

Lemma lin_form_vec k (L : 'rV[R]_k -> R) :
  (forall (c : R) (u v : 'rV[R]_k), L (c *: u + v) = c * L u + L v) ->
  forall u, L u = mxdot (\row_j L (delta_mx 0 j)) u.

Used by 2 declarations in 2 files

this file: bilin_form_mx
GaussianAnalysis.convex.logdet_barrier: logsum_sc_barrier

lemma bilin_form_mx main result source, line 608

forall {R : realType} [k : nat] [Q : 'rV_k -> 'rV_k -> R],
(forall (c : R) (u v w : 'rV_k), Q (c *: u + v) w = c * Q u w + Q v w) ->
(forall (c : R) (u v w : 'rV_k), Q w (c *: u + v) = c * Q w u + Q w v) ->
forall u : 'rV_k, Q u u = mxdot u (u *m \matrix_(i, j) Q (delta_mx 0 i) (delta_mx 0 j))

Main result

Stated in the README together with line_derive3.

Statement as written in the source

Lemma bilin_form_mx k (Q : 'rV[R]_k -> 'rV[R]_k -> R) :
  (forall (c : R) (u v w : 'rV[R]_k), Q (c *: u + v) w = c * Q u w + Q v w) ->
  (forall (c : R) (u v w : 'rV[R]_k), Q w (c *: u + v) = c * Q w u + Q w v) ->
  forall u,
    Q u u = mxdot u (u *m \matrix_(i, j) Q (delta_mx 0 i) (delta_mx 0 j)).

Used by 3 declarations in 3 files

GaussianAnalysis.convex.logdet_barrier: logsum_sc_barrier
GaussianAnalysis.convex.minimizers: continuous_ls_reduced
GaussianAnalysis.convex.ls_insertion: ins_hessianE

sectionsc_line

Context {R : realType} {N : nat}.
Variables (V : {vspace 'rV[R]_N}) (D : set 'rV[R]_N) (B : 'rV[R]_N -> R).
Hypothesis DV : rel_open_convex V D.

lemma rel_open_convex_segment source, line 637

forall {R : realType} {N : nat} [V : {vspace 'rV_N}] [D : set 'rV_N],
rel_open_convex V D ->
forall [z : 'rV_N] [h : 'rV[R]_N] [t s : R],
D z -> D (z + t *: h) -> 0 <= s <= t -> D (z + s *: h)

D contains the segment from z to z + t h.

Statement as written in the source

Lemma rel_open_convex_segment z h (t s : R) : D z -> D (z + t *: h) ->
  0 <= s <= t -> D (z + s *: h).

Used by 9 declarations in 1 file

this file: sc_hessian_line_ge, sc_hessian_line_le, sc_line_taylor_le, sc_dikin, sc_bregman_ge, sc_bregman_le, sc_function_convex, sc_barrier_grad_le, sc_barrier_contraction

lemma rel_open_convex_line source, line 653

forall {R : realType} {N : nat} [V : {vspace 'rV_N}] [D : set 'rV_N],
rel_open_convex V D ->
forall [z h : 'rV_N],
D z ->
h \in V ->
exists2 e : R,
  0 < e &
  forall t : join_Num_NumDomain_between_GRing_PzSemiRing_and_Num_SemiNormedZmodule R,
  `|t| < e -> D (z + t *: h)

D contains z + t h for t near 0, when z is in D and h in V.

Statement as written in the source

Lemma rel_open_convex_line z h : D z -> h \in V ->
  exists2 e : R, 0 < e & forall t, `|t| < e -> D (z + t *: h).

Used by 3 declarations in 2 files

this file: line_derive3, sc_dikin
GaussianAnalysis.convex.minimizers: ls_first_order

lemma line_derive3 main result source, line 668

forall {R : realType} {N : nat} [V : {vspace 'rV_N}] [D : set 'rV_N] [B : 'rV_N -> R],
rel_open_convex V D ->
forall [z h : 'rV_N] [phi phi1 phi2 phi3 : R -> R],
h \in V ->
(forall t : R, D (z + t *: h) -> B (z + t *: h) = phi t) ->
(forall t : R,
 D (z + t *: h) ->
 [/\ is_derive t 1 phi (phi1 t), is_derive t 1 phi1 (phi2 t) & is_derive t 1 phi2 (phi3 t)]) ->
forall [t : R],
D (z + t *: h) ->
[/\ is_derive (z + t *: h) h B (phi1 t), is_derive (z + t *: h) h ('D_h B) (phi2 t)
  & is_derive (z + t *: h) h ('D_h ('D_h B)) (phi3 t)]

The directional derivatives of a function that agrees on D, along a line, with a function of one variable with three derivatives.

Main result, as the README states it

If B agrees on D, along the line through z in the direction h of V, with a function of one variable that has three derivatives, these are the derivatives of B along h at the points of the line in D. A linear form on row vectors is mxdot g h and a bilinear form Q has Q h h = h M h^T, for the vector and the matrix of their values on the basis.

Statement as written in the source

Lemma line_derive3 z h (phi phi1 phi2 phi3 : R -> R) : h \in V ->
  (forall t, D (z + t *: h) -> B (z + t *: h) = phi t) ->
  (forall t, D (z + t *: h) -> [/\ is_derive t 1 phi (phi1 t),
     is_derive t 1 phi1 (phi2 t) & is_derive t 1 phi2 (phi3 t)]) ->
  forall t, D (z + t *: h) ->
  [/\ is_derive (z + t *: h) h B (phi1 t),
      is_derive (z + t *: h) h ('D_h B) (phi2 t) &
      is_derive (z + t *: h) h ('D_h ('D_h B)) (phi3 t)].

Used by 1 declaration in 1 file

GaussianAnalysis.convex.logdet_barrier: logsum_sc_barrier

Hypothesis scB : sc_function V D B.

lemma sc_line_derive source, line 707

forall {R : realType} {N : nat} [V : {vspace 'rV_N}] [D : set 'rV_N] [B : 'rV_N -> R],
sc_function V D B ->
forall [z h : 'rV[R]_N] [t : R],
D (z + t *: h) ->
h \in V ->
[/\ is_derive t 1
      (fun s : R =>
       B (z + s *: h))
      ('D_h B (z + t *: h)),
    is_derive t 1
      (fun s : R =>
       'D_h B (z + s *: h))
      ('D_h ('D_h B) (z + t *: h))
  & is_derive t 1
      (fun s : R =>
       'D_h ('D_h B) (z + s *: h))
      ('D_h ('D_h ('D_h B)) (z + t *: h))]

The derivatives of B along a line through D.

Statement as written in the source

Lemma sc_line_derive z h (t : R) : D (z + t *: h) -> h \in V ->
  [/\ is_derive t 1 (fun s => B (z + s *: h)) ('D_h B (z + t *: h)),
      is_derive t 1 (fun s => 'D_h B (z + s *: h))
        ('D_h ('D_h B) (z + t *: h)) &
      is_derive t 1 (fun s => 'D_h ('D_h B) (z + s *: h))
        ('D_h ('D_h ('D_h B)) (z + t *: h))].

Used by 8 declarations in 1 file

this file: sc_hessian_line_ge, sc_hessian_line_le, sc_line_taylor_le, sc_bregman_ge, sc_bregman_le, sc_function_convex, sc_barrier_grad_le, sc_barrier_contraction

lemma sc_hessian_line_ge main result source, line 722

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 [z h : 'rV_N] [t : R],
D z ->
h \in V ->
0 <= t ->
D (z + t *: h) ->
sc_norm B z h ^+ 2 / (1 + t * sc_norm B z h) ^+ 2 <= 'D_h ('D_h B) (z + t *: h)

The bounds of the proof of Lemma 2.15 of Koehler and Sohn on the second derivative along h, with r = sc_norm B z h.

Main result, as the README states it

Along a segment z + t h in D, with r = sc_norm B z h: r^2 / (1 + t r)^2 <= D^2 B(z + t h)[h,h], and D^2 B(z + t h)[h,h] <= r^2 / (1 - t r)^2 when t r < 1. The one-dimensional comparison behind it compares 1 / sqrt (psi + e) with t for a function psi >= 0 with psi'^2 <= 4 psi^3.

Statement as written in the source

Lemma sc_hessian_line_ge z h (t : R) : D z -> h \in V -> 0 <= t ->
  D (z + t *: h) ->
  sc_norm B z h ^+ 2 / (1 + t * sc_norm B z h) ^+ 2 <=
    'D_h ('D_h B) (z + t *: h).

Used by 1 declaration in 1 file

this file: sc_bregman_ge

lemma sc_hessian_line_le main result source, line 741

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 [z h : 'rV_N] [t : R],
D z ->
h \in V ->
0 <= t ->
D (z + t *: h) ->
t * sc_norm B z h < 1 ->
'D_h ('D_h B) (z + t *: h) <= sc_norm B z h ^+ 2 / (1 - t * sc_norm B z h) ^+ 2

Main result

Stated in the README together with sc_hessian_line_ge.

Statement as written in the source

Lemma sc_hessian_line_le z h (t : R) : D z -> h \in V -> 0 <= t ->
  D (z + t *: h) -> t * sc_norm B z h < 1 ->
  'D_h ('D_h B) (z + t *: h) <=
    sc_norm B z h ^+ 2 / (1 - t * sc_norm B z h) ^+ 2.

Used by 2 declarations in 1 file

this file: sc_dikin, sc_bregman_le

lemma bregman_div_add source, line 764

forall {R : realType} {N : nat} (B : 'rV_N -> R)
  (z h : 'rV[R]_N),
bregman_div B (z + h) z = B (z + h) - B z - 'D_h B z

Statement as written in the source

Lemma bregman_div_add z h :
  bregman_div B (z + h) z = B (z + h) - B z - 'D_h B z.

Used by 3 declarations in 1 file

this file: sc_bregman_ge, sc_bregman_le, sc_taylor3

lemma sc_line_taylor_le source, line 771

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 [z h : 'rV_N] [u K : R],
D z ->
h \in V ->
0 <= u ->
D (z + u *: h) ->
(forall v : join_Num_POrderNmodule_between_Algebra_BaseAddUMagma_and_Order_Preorder R,
 0 <= v <= u -> 'D_h ('D_h B) (z + v *: h) <= K) ->
B (z + u *: h) <= B z + u * 'D_h B z + u ^+ 2 / 2 * K

B lies above its tangents along a segment of D, with an upper bound by the second derivative: on the segment from z to z + u h, B (z + u h) <= B z + u D B(z)[h] + u^2 K / 2 when D^2 B <= K there.

Statement as written in the source

Lemma sc_line_taylor_le z h (u K : R) : D z -> h \in V -> 0 <= u ->
  D (z + u *: h) ->
  (forall v, 0 <= v <= u -> 'D_h ('D_h B) (z + v *: h) <= K) ->
  B (z + u *: h) <= B z + u * 'D_h B z + u ^+ 2 / 2 * K.

Used by 1 declaration in 1 file

this file: sc_dikin

lemma sc_dikin main result source, line 808

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 [z h : 'rV_N], D z -> h \in V -> sc_norm B z h < 1 -> D (z + h)

The Dikin ellipsoid (Nesterov and Nemirovskii, Theorem 2.1.1): if the local norm of h at z is less than 1, then z + h is in D.

Main result, as the README states it

The Dikin ellipsoid: if sc_norm B z h < 1 then z + h is in D (Nesterov-Nemirovskii, Theorem 2.1.1); proved from the bound above and the blow-up of B at the exit point of the segment.

Statement as written in the source

Lemma sc_dikin z h : D z -> h \in V -> sc_norm B z h < 1 -> D (z + h).

Used by 2 declarations in 1 file

this file: sc_bregman_le, sc_taylor3

lemma sc_bregman_ge main result source, line 900

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 [z h : 'rV_N],
D z -> h \in V -> D (z + h) -> sc_omega (sc_norm B z h) <= bregman_div B (z + h) z

The Bregman bounds of the proof of Lemma 2.15: sc_omega r <= D_B(z + h, z) <= sc_omega_star r, r = sc_norm B z h.

Main result, as the README states it

Lemma 2.15 of Koehler and Sohn: r - ln (1 + r) <= bregman_div B (z + h) z when z + h is in D, and bregman_div B (z + h) z <= - r - ln (1 - r) when r < 1; hence (i) if the Bregman divergence is at most 1/2 - ln (3/2) then r <= 1/2 and it is at least r^2 / 3, and (ii) if r <= 1/2 then z + h is in D and |B (z + h) - B z - D B(z)[h] - r^2 / 2| <= 2 r^3 / 3.

Statement as written in the source

Lemma sc_bregman_ge z h : D z -> h \in V -> D (z + h) ->
  sc_omega (sc_norm B z h) <= bregman_div B (z + h) z.

Used by 3 declarations in 2 files

GaussianAnalysis.probability.measurable_minimizer: ls_min_growth
this file: sc_bregman_small, sc_taylor3

lemma sc_bregman_le main result source, line 937

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 [z h : 'rV_N],
D z ->
h \in V -> sc_norm B z h < 1 -> bregman_div B (z + h) z <= sc_omega_star (sc_norm B z h)

Main result

Stated in the README together with sc_bregman_ge.

Statement as written in the source

Lemma sc_bregman_le z h : D z -> h \in V -> sc_norm B z h < 1 ->
  bregman_div B (z + h) z <= sc_omega_star (sc_norm B z h).

Used by 1 declaration in 1 file

this file: sc_taylor3

lemma sc_bregman_small main result source, line 977

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 [z h : 'rV_N],
D z ->
h \in V ->
D (z + h) ->
bregman_div B (z + h) z <= sc_omega 2^-1 ->
sc_norm B z h <= 2^-1 /\ sc_norm B z h ^+ 2 / 3 <= bregman_div B (z + h) z

Lemma 2.15 (i) of Koehler and Sohn: a small Bregman divergence bounds the local norm.

Main result

Stated in the README together with sc_bregman_ge.

Statement as written in the source

Lemma sc_bregman_small z h : D z -> h \in V -> D (z + h) ->
  bregman_div B (z + h) z <= sc_omega 2^-1 ->
  sc_norm B z h <= 2^-1 /\ sc_norm B z h ^+ 2 / 3%:R <= bregman_div B (z + h) z.

Used by 1 declaration in 1 file

GaussianAnalysis.convex.ls_insertion: ins_cost_lower

lemma sc_taylor3 main result source, line 991

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 [z h : 'rV_N],
D z ->
h \in V ->
sc_norm B z h <= 2^-1 ->
D (z + h) /\
`|B (z + h) - B z - 'D_h B z - sc_norm B z h ^+ 2 / 2| <= 2 * sc_norm B z h ^+ 3 / 3

Lemma 2.15 (ii): the Taylor expansion of order 2 with a remainder of order 3 in the local norm.

Main result

Stated in the README together with sc_bregman_ge.

Statement as written in the source

Lemma sc_taylor3 z h : D z -> h \in V -> sc_norm B z h <= 2^-1 ->
  D (z + h) /\
  `|B (z + h) - B z - 'D_h B z - sc_norm B z h ^+ 2 / 2| <=
    2 * sc_norm B z h ^+ 3 / 3%:R.

Used by 2 declarations in 2 files

this file: sc_function_continuous
GaussianAnalysis.convex.ls_insertion: ins_rem_le

lemma sc_function_convex main result source, line 1009

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 [z y : 'rV_N] [t : R],
D z -> D y -> 0 <= t <= 1 -> B (z + t *: (y - z)) <= (1 - t) * B z + t * B y

B is convex on D.

Main result, as the README states it

A self-concordant function is convex on D, and continuous at every point of D for the points of D.

Statement as written in the source

Lemma sc_function_convex z y (t : R) : D z -> D y -> 0 <= t <= 1 ->
  B (z + t *: (y - z)) <= (1 - t) * B z + t * B y.

Used by 1 declaration in 1 file

GaussianAnalysis.convex.minimizers: sc_sublevel_closed

lemma sc_function_continuous main result source, line 1040

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 [z : 'rV_N],
D z ->
forall [e : R],
0 < e -> exists2 d : R, 0 < d & forall y : 'rV_N, D y -> `|y - z| < d -> `|B y - B z| < e

B is continuous on D.

Main result

Stated in the README together with sc_function_convex.

Statement as written in the source

Lemma sc_function_continuous z : D z -> forall e : R, 0 < e ->
  exists2 d : R, 0 < d & forall y, D y -> `|y - z| < d -> `|B y - B z| < e.

Used by 6 declarations in 4 files

GaussianAnalysis.probability.measurable_minimizer: measurable_ls_min
GaussianAnalysis.convex.minimizers: sc_sublevel_closed, sc_minimizer
GaussianAnalysis.convex.barrier_lindeberg: loo_compare, Phi_meas
GaussianAnalysis.convex.ridge_comparison: ridge_comparison

sectionsc_barrier_lemmas

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

lemma sc_barrier_grad_le main result source, line 1124

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 y : 'rV_N], D z -> D y -> 'D_(y - z) B z <= theta

Lemma 2.10 of Koehler and Sohn, first part (Nesterov, Theorem 4.2.4): D B(z)[y - z] <= theta for z, y in D.

Main result, as the README states it

Lemma 2.10 of Koehler and Sohn, for a theta-self-concordant barrier with theta >= 0: D B(z)[y - z] <= theta for y, z in D (Nesterov, Theorem 4.2.4), and B ((1 - eps) x + eps x0) <= B x0 + theta ln (1 / eps) for x0, x in D and 0 < eps < 1.

Statement as written in the source

Lemma sc_barrier_grad_le z y : D z -> D y -> 'D_(y - z) B z <= theta.

Used by 1 declaration in 1 file

this file: sc_barrier_contraction

lemma sc_barrier_contraction main result source, line 1186

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 [x0 x : 'rV_N] [eps : R],
D x0 -> D x -> 0 < eps < 1 -> B ((1 - eps) *: x + eps *: x0) <= B x0 + theta * ln eps^-1

Lemma 2.10: contracting toward x0 costs at most theta ln (1 / eps).

Main result

Stated in the README together with sc_barrier_grad_le.

Statement as written in the source

Lemma sc_barrier_contraction x0 x (eps : R) : D x0 -> D x -> 0 < eps < 1 ->
  B ((1 - eps) *: x + eps *: x0) <= B x0 + theta * ln eps^-1.

Used by 1 declaration in 1 file

GaussianAnalysis.convex.barrier_removal: barrier_removal

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.