On this page

Universality of barrier-regularized least squares

GaussianAnalysis.convex.barrier_lindeberglibrary/convex/barrier_lindeberg.v1,576 lines37 lemmas and theorems, 2 definitionssource

Imports 12 library modules and 28 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.rat, mathcomp.algebra.interval, mathcomp.classical.boolp, mathcomp.classical.classical_sets, mathcomp.classical.functions, mathcomp.reals.reals, mathcomp.analysis.ereal, mathcomp.analysis.topology_theory.topology, mathcomp.analysis.normedtype_theory.normedtype, mathcomp.analysis.sequences, mathcomp.analysis.derive, mathcomp.analysis.realfun, mathcomp.analysis.exp, mathcomp.analysis.measure_theory.measure, mathcomp.analysis.lebesgue_measure, mathcomp.analysis.measurable_realfun, mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral, mathcomp.analysis.probability_theory.probability, mathcomp.algebra.ring_tactic, mathcomp.algebra.field_tactic, mathcomp.algebra.arithmetic_tactic

Imported by 2

Required by 3 files of the paper proofs

Theorem 2.9 of Koehler and Sohn (arXiv 2608.27372, lines 1282-1344, proof lines 1637-2116 and 3809-4225), in the paper's abstract feature form, for two laws mu and nu of features on 'rV[R]_N that are (K, tau)-regular with the same covariance Sigma (regular_feature of least_squares.v), with lambda = opnorm Sigma and tau >= 0. D is nonempty, convex and relatively open with directions V (rel_open_convex), B >= 0 is a self-concordant function on D (sc_function), beta, gamma > 0 and n > 0. Phi Z is the value ls_barrier_value Z lambda beta D gamma B of the features Z, and

Lref = (1 + 1 / beta) (1 + inf_(theta in D) (lambda |theta|^2
       + gamma B theta))

is ls_ref_scale lambda beta gamma D B. The paper asks D to be bounded and B to be a barrier; the proof uses neither.

hybrid mu nu k the laws of the coordinates of the Lindeberg argument: mu before the coordinate k, nu from k on

barrier_lindeberg_mean, (2.12): if 36 <= n gamma, then

|E_(mu^n) Phi - E_(nu^n) Phi| <= 100 (1 + K^4)^2 Lref^2
  ((n gamma)^(-1/2) + sqrt (dim V) (tau / lambda + 1) / n).

barrier_lindeberg_variance, (2.13): Var_(mu^n) Phi <= 4 (1 + K^4)^2 Lref^2 / n.
barrier_lindeberg_concentration, (2.14): for t > 0 and 36 <= n gamma, Phi is within the bound of (2.12) plus t of E_(nu^n) Phi, except on an event of mu^n-probability at most 4 (1 + K^4)^2 Lref^2 / (n t^2).

The hypotheses are symmetric in mu and nu, so the last two hold for nu.

The proof is the paper's. measurable_ls_barrier_value: Phi is a measurable function of the features (an infimum over a countable dense subset of D). lindeberg_telescope: the replacement argument for an integrable functional with bounds that depend on the other coordinates. insertion_compare (Propositions 2.14 and 2.16): the comparison of the means of an insertion cost under mu and nu, from its pointwise bounds (ls_insertion.v) and the moment calculus of feature_moments.v; le_amgm turns the Cauchy-Schwarz step into an infimum over a weight. loo_compare and loo_variance: the same for the value, at the leave-one-out minimizer of minimizers.v.

Main results

Results	Statement
measurable_ls_barrier_valuemeasurable_inf_rel_open	The value `Phi_Z(D, B; beta, gamma)` of the barrier-regularized problem is a measurable function of the features `Z`, for `D` convex and relatively open and `B >= 0` continuous on `D`: an infimum over `D` of an upper semicontinuous family is the infimum over a countable dense subset.
lindeberg_telescopehybridintegral_tuple_prod_freege0_integral_tuple_prod_tnth	Lindeberg's replacement for a nonnegative integrable functional `F` of `n` independent coordinates, with bounds `b_i` that may depend on the other coordinates: if `\|E_mu F(x^(i <- t)) - E_nu F(x^(i <- t))\| <= b_i x` for all `i` and `x`, then `\|E_(mu^n) F - E_(nu^n) F\| <= sum_i E b_i` under the hybrid law with `mu` before `i` and `nu` after. The integral of a function that does not depend on a coordinate does not depend on its law, and the coordinate `j` of `tuple_prod rho n` has law `rho j`.
insertion_compareloo_compareloo_variance	Propositions 2.14 and 2.16 of Koehler and Sohn: for two regular features with the same covariance, the means of the cost of inserting one feature differ by at most `(4 + 48 (1 + K^4) S^2) / (n sqrt (n gamma)) + 4 sqrt (1 + K^4) sqrt (dim V) (tau / lambda + 1) S / (beta n^2)`, where `S = lambda \|theta_m\|^2 + b_m^2` is the size of the leave-one-out minimizer; for the value itself the same holds with `S` replaced by its bound `((2 n)^-1 sum_(j <> i) <x_j, theta_ref>^2 + beta lambda \|theta_ref\|^2 + gamma B theta_ref) / beta`, and the variance in the coordinate `i` is at most `2 (1 + K^4) / n^2` times the square of that bound.
barrier_lindeberg_meanbarrier_lindeberg_variancebarrier_lindeberg_concentrationls_ref_scale	Theorem 2.9 of Koehler and Sohn, for `mu`, `nu` `(K, tau)`-regular with the same covariance, `D` convex, relatively open and nonempty (not necessarily bounded), `B >= 0` self-concordant on `D`, `beta, gamma > 0` and `Lref = (1 + 1/beta) (1 + inf_D (lambda \|theta\|^2 + gamma B theta))`: if `36 <= n gamma`, `\|E_(mu^n) Phi - E_(nu^n) Phi\| <= 100 (1 + K^4)^2 Lref^2 ((n gamma)^(-1/2) + sqrt (dim V) (tau / lambda + 1) / n)`; `Var_(mu^n) Phi <= 4 (1 + K^4)^2 Lref^2 / n`; and `Phi` is within that bound plus `t` of `E_(nu^n) Phi` outside an event of `mu^n`-probability at most `4 (1 + K^4)^2 Lref^2 / (n t^2)`.

Declarations39 exported, 1 local

sectionmeasurable_inf

Context {R : realType} {N : nat} d (T : measurableType d).

lemma orthonormal_entry_le1 source, line 71

forall {R : realType} {N : nat} [k : nat] [E : 'M_(k, N)] (l : 'I_k) (j : 'I_N),
E *m E^T = 1%:M -> `|E l j| <= 1

The entries of a matrix with orthonormal rows are at most 1.

Statement as written in the source

Lemma orthonormal_entry_le1 k (E : 'M[R]_(k, N)) l j :
  E *m E^T = 1%:M -> `|E l j| <= 1.

Used by 2 declarations in 2 files

GaussianAnalysis.probability.measurable_minimizer: rel_open_dense_seq
this file: measurable_inf_rel_open

lemma measurable_inf_rel_open main result source, line 88

forall {R : realType} {N : nat} [d : measure_display] [T : measurableType d]
  [V : {vspace 'rV_N}] [D : set 'rV_N] [g : T -> 'rV_N -> R],
rel_open_convex V D ->
D !=set0 ->
(forall th : 'rV_N, measurable_fun [set: T] (g^~ th)) ->
(forall (t : T) (th : 'rV_N),
 D th ->
 forall e : R,
 0 < e ->
 exists2 dl : R,
   0 < dl & forall th' : 'rV_N, D th' -> `|th' - th| < dl -> g t th' < g t th + e) ->
(forall (t : T) (th : 'rV_N), D th -> 0 <= g t th) ->
measurable_fun [set: T] (fun t : T => inf [set g t th | th in D])

An infimum over a relatively open convex set of an upper semicontinuous family of measurable functions is measurable: it is the infimum over the countable dense set of the points theta_0 + q E, q rational.

Main result

Stated in the README together with measurable_ls_barrier_value.

Statement as written in the source

Lemma measurable_inf_rel_open (V : {vspace 'rV[R]_N}) (D : set 'rV[R]_N)
    (g : T -> 'rV[R]_N -> R) :
  rel_open_convex V D -> D !=set0 ->
  (forall th, measurable_fun setT (g ^~ th)) ->
  (forall t th, D th -> forall e : R, 0 < e -> exists2 dl : R, 0 < dl &
     forall th', D th' -> `|th' - th| < dl -> g t th' < g t th + e) ->
  (forall t th, D th -> 0 <= g t th) ->
  measurable_fun setT (fun t => inf [set g t th | th in D]).

Used by 1 declaration in 1 file

this file: measurable_ls_barrier_value

sectionmeasurable_values

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

lemma measurable_mxdot_tnth source, line 178

forall {R : realType} {N : nat} [n : nat] (i : 'I_n) (th : 'rV_N),
measurable_fun [set: n.-tuple _]
  (fun Z : n.-tuple 'rV_N => mxdot (tnth Z i) th)

Statement as written in the source

Lemma measurable_mxdot_tnth n (i : 'I_n) (th : 'rV[R]_N) :
  measurable_fun setT (fun Z : n.-tuple 'rV[R]_N => mxdot (tnth Z i) th).

Used by 3 declarations in 2 files

this file: measurable_ls_reduced, barrier_lindeberg_mean
GaussianAnalysis.convex.ridge_comparison: ridge_comparison

lemma measurable_sum_pred source, line 186

forall {R : realType} [d : measure_display] [T : measurableType d] 
  [n : nat] [P : pred 'I_n] [h : 'I_n -> T -> R],
(forall i : 'I_n, P i -> measurable_fun [set: T] (h i)) ->
measurable_fun [set: T] (fun x : T => \sum_(i < n | P i) h i x)

Statement as written in the source

Lemma measurable_sum_pred d (T : measurableType d) n (P : pred 'I_n)
    (h : 'I_n -> T -> R) :
  (forall i, P i -> measurable_fun setT (h i)) ->
  measurable_fun setT (fun x => \sum_(i < n | P i) h i x).

Used by 2 declarations in 2 files

GaussianAnalysis.probability.measurable_minimizer: measurable_ls_bopt_min
this file: measurable_ls_reduced

lemma measurable_ls_reduced source, line 200

forall {R : realType} {N : nat} [n : nat] (P : pred 'I_n) (s lambda beta : R) (th : 'rV_N),
measurable_fun [set: n.-tuple _]
  (fun Z : n.-tuple 'rV_N => ls_ridge Z P s lambda beta th (ls_bopt Z P s beta th))

Statement as written in the source

Lemma measurable_ls_reduced n (P : pred 'I_n) (s lambda beta : R)
    (th : 'rV[R]_N) :
  measurable_fun setT (fun Z : n.-tuple 'rV[R]_N =>
    ls_ridge Z P s lambda beta th (ls_bopt Z P s beta th)).

Used by 2 declarations in 2 files

GaussianAnalysis.probability.measurable_minimizer: measurable_ls_reduced_at
this file: measurable_ls_barrier_value

sectionls_value_measurable

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.
Hypothesis D0 : D !=set0.
Hypothesis B0 : forall z, D z -> 0 <= B z.
Hypothesis Bc : forall z, D z -> forall e : R, 0 < e ->
  exists2 dl : R, 0 < dl & forall y, D y -> `|y - z| < dl -> `|B y - B z| < e.

lemma ls_ridge_ge0' source, line 232

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

Statement as written in the source

Lemma ls_ridge_ge0' n (Z : n.-tuple 'rV[R]_N) (P : pred 'I_n)
    (s lambda beta : R) th b :
  0 <= s -> 0 <= lambda -> 0 <= beta -> 0 <= ls_ridge Z P s lambda beta th b.

Used by 2 declarations in 1 file

this file: ls_barrier_valueE, measurable_ls_barrier_value

lemma ls_barrier_valueE source, line 243

forall {R : realType} {N : nat} [D : set 'rV_N] [B : 'rV_N -> R],
D !=set0 ->
(forall z : 'rV_N, D z -> 0 <= B z) ->
forall [n : nat] (Z : n.-tuple 'rV_N) [lambda beta gamma : R],
(0 < n)%N ->
0 <= lambda ->
0 <= beta ->
0 <= gamma ->
ls_barrier_value Z lambda beta D gamma B =
inf
  [set ls_ridge Z predT (n%:R *+ 2)^-1 lambda beta th
         (ls_bopt Z predT (n%:R *+ 2)^-1 beta th) +
       gamma * B th
     | th in D]

The value is the infimum over D of the objective with the optimal b.

Statement as written in the source

Lemma ls_barrier_valueE n (Z : n.-tuple 'rV[R]_N) (lambda beta gamma : R) :
  (0 < n)%N -> 0 <= lambda -> 0 <= beta -> 0 <= gamma ->
  ls_barrier_value Z lambda beta D gamma B =
  inf [set ls_ridge Z predT (n%:R *+ 2)^-1 lambda beta th
         (ls_bopt Z predT (n%:R *+ 2)^-1 beta th) + gamma * B th | th in D].

Used by 1 declaration in 1 file

this file: measurable_ls_barrier_value

lemma measurable_ls_barrier_value main result source, line 283

forall {R : realType} {N : nat} [V : {vspace 'rV_N}] [D : set 'rV_N] [B : 'rV_N -> R],
rel_open_convex V D ->
D !=set0 ->
(forall z : 'rV_N, D z -> 0 <= B z) ->
(forall z : 'rV_N,
 D z ->
 forall e : R,
 0 < e ->
 exists2 dl : R, 0 < dl & forall y : 'rV_N, D y -> `|y - z| < dl -> `|B y - B z| < e) ->
forall [n : nat] [lambda beta gamma : R],
0 <= lambda ->
0 <= beta ->
0 <= gamma ->
measurable_fun [set: n.-tuple _]
  (fun Z : n.-tuple 'rV_N => ls_barrier_value Z lambda beta D gamma B)

The values Phi_Z(D, B; beta, gamma) are measurable functions of the features.

Main result, as the README states it

The value Phi_Z(D, B; beta, gamma) of the barrier-regularized problem is a measurable function of the features Z, for D convex and relatively open and B >= 0 continuous on D: an infimum over D of an upper semicontinuous family is the infimum over a countable dense subset.

Statement as written in the source

Lemma measurable_ls_barrier_value n (lambda beta gamma : R) :
  0 <= lambda -> 0 <= beta -> 0 <= gamma ->
  measurable_fun setT
    (fun Z : n.-tuple 'rV[R]_N => ls_barrier_value Z lambda beta D gamma B).

Used by 4 declarations in 2 files

this file: loo_compare, Phi_meas
GaussianAnalysis.convex.ridge_comparison: measurable_ls_value, ridge_comparison

sectiontelescoping

Context d (T : measurableType d) (R : realType).
Local Open Scope ereal_scope.

definition hybrid main result source, line 334

Type

forall [d : measure_display] [T : measurableType d] [R : realType],
probability T R -> probability T R -> nat -> nat -> probability T R

Definition

Definition hybrid (mu nu : probability T R) (k : nat) (j : nat) :
    probability T R :=
  if (j < k)%N then mu else nu.

The hybrid law: mu for the coordinates < k, nu for the others.

Main result

Stated in the README together with lindeberg_telescope.

Used by 3 declarations in 1 file

this file: lindeberg_telescope, hybrid_regular, barrier_lindeberg_mean

lemma probability_inhabited source, line 338

forall [d : measure_display] [T : measurableType d] [R : realType],
probability T R -> exists _ : T, True

Statement as written in the source

Lemma probability_inhabited (mu : probability T R) : exists t : T, True.

Used by 1 declaration in 1 file

this file: integral_tuple_prod_free

lemma integral_tuple_prod_free main result source, line 348

forall [d : measure_display] [T : measurableType d] [R : realType]
  [rho rho' : nat -> probability T R] [n : nat] [i : 'I_n] [G : n.-tuple T -> \bar R],
measurable_fun [set: n.-tuple _] G ->
(forall (x : n.-tuple T) (t : T), G (tuple_set x i t) = G x) ->
(forall j : nat, j != i -> rho j = rho' j) ->
(\int[tuple_prod rho n]_x G x)%E = (\int[tuple_prod rho' n]_x G x)%E

The integral of a function that does not depend on the coordinate i does not depend on the law of that coordinate.

Main result

Stated in the README together with lindeberg_telescope.

Statement as written in the source

Lemma integral_tuple_prod_free (rho rho' : nat -> probability T R) n
    (i : 'I_n) (G : n.-tuple T -> \bar R) :
  measurable_fun setT G -> (forall x t, G (tuple_set x i t) = G x) ->
  (forall j, j != nat_of_ord i -> rho j = rho' j) ->
  \int[tuple_prod rho n]_x G x = \int[tuple_prod rho' n]_x G x.

Used by 1 declaration in 1 file

this file: lindeberg_telescope

lemma tnth_tuple_set source, line 379

forall [d : measure_display] [T : measurableType d] [n : nat] (x : n.-tuple T) 
  (i : 'I_n) (t : T),
tnth (tuple_set x i t) i = t

Statement as written in the source

Lemma tnth_tuple_set n (x : n.-tuple T) (i : 'I_n) (t : T) :
  tnth (tuple_set x i t) i = t.

Used by 2 declarations in 1 file

this file: ge0_integral_tuple_prod_tnth, int_Phi_set

lemma tnth_tuple_set_neq source, line 383

forall [d : measure_display] [T : measurableType d] [n : nat] (x : n.-tuple T) 
  [i j : 'I_n] (t : T),
j != i -> tnth (tuple_set x i t) j = tnth x j

Statement as written in the source

Lemma tnth_tuple_set_neq n (x : n.-tuple T) (i j : 'I_n) (t : T) :
  j != i -> tnth (tuple_set x i t) j = tnth x j.

Used by 3 declarations in 2 files

GaussianAnalysis.probability.measurable_minimizer: ls_bopt_tuple_set, ls_reduced_tuple_set
this file: int_Phi_set

lemma ge0_integral_tuple_prod_tnth main result source, line 388

forall [d : measure_display] [T : measurableType d] [R : realType]
  (rho : nat -> probability T R) [n : nat] (j : 'I_n) [g : T -> \bar R],
measurable_fun [set: T] g ->
(forall t : T, (0%R <= g t)%E) ->
(\int[tuple_prod rho n]_x g (tnth x j))%E = (\int[rho j]_t g t)%E

The law of the coordinate j of tuple_prod rho n is rho j.

Main result

Stated in the README together with lindeberg_telescope.

Statement as written in the source

Lemma ge0_integral_tuple_prod_tnth (rho : nat -> probability T R) n
    (j : 'I_n) (g : T -> \bar R) :
  measurable_fun setT g -> (forall t, 0 <= g t) ->
  \int[tuple_prod rho n]_x g (tnth x j) = \int[rho j]_t g t.

Used by 2 declarations in 1 file

this file: integrable_tuple_prod_tnth, Rintegral_tuple_prod_tnth

lemma integrable_tuple_prod_tnth source, line 401

forall [d : measure_display] [T : measurableType d] [R : realType]
  [rho : nat -> probability T R] [n : nat] [j : 'I_n] [g : T -> R],
(rho j).-integrable [set: T] (EFin \o g) ->
(tuple_prod rho n).-integrable [set: n.-tuple T]
  (EFin \o (fun x : n.-tuple T => g (tnth x j)))

Statement as written in the source

Lemma integrable_tuple_prod_tnth (rho : nat -> probability T R) n
    (j : 'I_n) (g : T -> R) :
  (rho j).-integrable setT (EFin \o g) ->
  (tuple_prod rho n).-integrable setT (EFin \o (fun x => g (tnth x j))).

Used by 5 declarations in 2 files

this file: int_Phi, barrier_lindeberg_mean, int_P4
GaussianAnalysis.convex.ridge_comparison: ref_objective_int, ref_objective_mean

lemma Rintegral_tuple_prod_tnth source, line 413

forall [d : measure_display] [T : measurableType d] [R : realType]
  (rho : nat -> probability T R) [n : nat] (j : 'I_n) [g : T -> R],
measurable_fun [set: T] g ->
(forall t : T, 0 <= g t) -> \int[tuple_prod rho n]_x g (tnth x j) = \int[rho j]_t g t

Statement as written in the source

Lemma Rintegral_tuple_prod_tnth (rho : nat -> probability T R) n
    (j : 'I_n) (g : T -> R) :
  measurable_fun setT g -> (forall t, 0 <= g t)%R ->
  (\int[tuple_prod rho n]_x g (tnth x j) = \int[rho j]_t g t)%R.

Used by 3 declarations in 2 files

this file: barrier_lindeberg_mean, int_P4
GaussianAnalysis.convex.ridge_comparison: ref_objective_mean

lemma lindeberg_telescope main result source, line 428

forall [d : measure_display] [T : measurableType d] [R : realType]
  [mu nu : probability T R] [n : nat] [F : n.-tuple T -> R] [b : 'I_n -> n.-tuple T -> R],
measurable_fun [set: n.-tuple _] F ->
(forall x : n.-tuple T, 0 <= F x) ->
(forall k : nat,
 (k <= n)%N -> (tuple_prod (hybrid mu nu k) n).-integrable [set: n.-tuple T] (EFin \o F)) ->
(forall (i : 'I_n) (x : n.-tuple T),
 mu.-integrable [set: T] (fun t : T => (F (tuple_set x i t))%:E) /\
 nu.-integrable [set: T] (fun t : T => (F (tuple_set x i t))%:E)) ->
(forall i : 'I_n,
 measurable_fun [set: n.-tuple _] (b i)) ->
(forall i : 'I_n,
 (tuple_prod (hybrid mu nu i) n).-integrable [set: n.-tuple T] (EFin \o b i)) ->
(forall (i : 'I_n) (x : n.-tuple T),
 `|\int[mu]_t F (tuple_set x i t) - \int[nu]_t F (tuple_set x i t)| <= b i x) ->
`|\int[tuple_prod (fun=> mu) n]_x F x - \int[tuple_prod (fun=> nu) n]_x F x| <=
\sum_(i < n) \int[tuple_prod (hybrid mu nu i) n]_x b i x

Lindeberg's replacement with integrable functionals and bounds that depend on the other coordinates: for F >= 0, replacing the laws mu of the coordinates by nu changes the expectation of F by at most sum_i E_(hybrid i) b_i, if b_i bounds the change of the integral in the coordinate i.

Main result, as the README states it

Lindeberg's replacement for a nonnegative integrable functional F of n independent coordinates, with bounds b_i that may depend on the other coordinates: if |E_mu F(x^(i <- t)) - E_nu F(x^(i <- t))| <= b_i x for all i and x, then |E_(mu^n) F - E_(nu^n) F| <= sum_i E b_i under the hybrid law with mu before i and nu after. The integral of a function that does not depend on a coordinate does not depend on its law, and the coordinate j of tuple_prod rho n has law rho j.

Statement as written in the source

Lemma lindeberg_telescope (mu nu : probability T R) n (F : n.-tuple T -> R)
    (b : 'I_n -> n.-tuple T -> R) :
  measurable_fun setT F -> (forall x, (0 <= F x)%R) ->
  (forall k, (k <= n)%N ->
     (tuple_prod (hybrid mu nu k) n).-integrable setT (EFin \o F)) ->
  (forall (i : 'I_n) x,
     mu.-integrable setT (fun t => (F (tuple_set x i t))%:E) /\
     nu.-integrable setT (fun t => (F (tuple_set x i t))%:E)) ->
  (forall i : 'I_n, measurable_fun setT (b i)) ->
  (forall i : 'I_n,
     (tuple_prod (hybrid mu nu i) n).-integrable setT (EFin \o b i)) ->
  (forall (i : 'I_n) x, (`|\int[mu]_t F (tuple_set x i t) -
                 \int[nu]_t F (tuple_set x i t)| <= b i x)%R) ->
  (`|\int[tuple_prod (fun=> mu) n]_x F x - \int[tuple_prod (fun=> nu) n]_x F x|
    <= \sum_(i < n) \int[tuple_prod (hybrid mu nu i) n]_x b i x)%R.

Used by 1 declaration in 1 file

this file: barrier_lindeberg_mean

sectionreal_bounds

Context {R : realType}.

lemma le_amgm source, line 525

forall {R : realType} [X A B : R],
0 <= A ->
0 <= B ->
(forall e : join_Num_POrderNmodule_between_Algebra_BaseAddUMagma_and_Order_Preorder R,
 0 < e -> X <= e * A + B / e) ->
X <= 2 * Num.ExtraDef.sqrtr (A * B)

If X <= e A + B / e for every e > 0, then X <= 2 sqrt (A B).

Statement as written in the source

Lemma le_amgm (X A B : R) : 0 <= A -> 0 <= B ->
  (forall e, 0 < e -> X <= e * A + B / e) -> X <= 2 * Num.sqrt (A * B).

Used by 1 declaration in 1 file

this file: insertion_compare

lemma inv_diff_le source, line 563

forall {R : realType} [a b c : R],
0 < c -> c <= a -> c <= b -> `|a^-1 - b^-1| <= `|a - b| / c ^+ 2

The difference of two inverses.

Statement as written in the source

Lemma inv_diff_le (a b c : R) : 0 < c -> c <= a -> c <= b ->
  `|a^-1 - b^-1| <= `|a - b| / c ^+ 2.

Used by 1 declaration in 1 file

this file: insertion_compare

lemma le_weighted_sqr source, line 581

forall {R : realType} (x y : R) [e : R], 0 < e -> x * y <= (e * x ^+ 2 + y ^+ 2 / e) / 2

A product bounded by squares, with a free weight.

Statement as written in the source

Lemma le_weighted_sqr (x y e : R) : 0 < e ->
  x * y <= (e * x ^+ 2 + y ^+ 2 / e) / 2.

Used by 1 declaration in 1 file

this file: insertion_compare

sectioninsertion_compare

Context {R : realType} {N : nat}.
Variables (K tau : R) (Sigma : 'M[R]_N) (mu nu : probability 'rV[R]_N R).
Hypotheses (rmu : regular_feature K tau Sigma mu)
  (rnu : regular_feature K tau Sigma nu) (tau0 : 0 <= tau).
Variables (n k : nat) (beta gamma : R).
Hypotheses (n0 : (0 < n)%N) (b0 : 0 < beta) (g0 : 0 < gamma).
Variables (f : 'rV[R]_N -> R) (thm v : 'rV[R]_N) (bm c0 : R) (T : 'M[R]_N).
Hypothesis mf : measurable_fun setT f.
Hypothesis fb : forall z, 0 <= f z <= (bm - mxdot z thm) ^+ 2 / (2 * n%:R).
Hypothesis l0 : forall z, 0 <= c0 - 2 * mxdot z v + mxdot z (z *m T).
Hypothesis fq : forall z,
  `|f z - (bm - mxdot z thm) ^+ 2 /
     (2 * (n%:R + (c0 - 2 * mxdot z v + mxdot z (z *m T))))| <=
  (2 + 3 * (bm - mxdot z thm) ^+ 4) / (n%:R * Num.sqrt (n%:R * gamma)).
Hypotheses (Tsym : T \is symmetricmx)
  (Tf : frobenius T ^+ 2 <= k%:R / (4 * beta ^+ 2 * opnorm Sigma ^+ 2))
  (vv : mxdot v v <= k%:R / (4 * beta ^+ 2 * opnorm Sigma)).
Local Notation lambda := (opnorm Sigma).
Local Notation S := (opnorm Sigma * mxdot thm thm + bm ^+ 2).
Local Notation rho := (Num.sqrt k%:R * (tau / opnorm Sigma + 1) / beta).

lemma ins_l_var source, line 617

forall {R : realType} {N : nat} [K tau : R] [Sigma : 'M_N] [mu : probability 'rV_N R],
regular_feature K tau Sigma mu ->
0 <= tau ->
forall [k : nat] [beta : R],
0 < beta ->
forall [v : 'rV_N] (c0 : R) [T : 'M_N],
T \is symmetricmx ->
frobenius T ^+ 2 <= k%:R / (4 * beta ^+ 2 * opnorm Sigma ^+ 2) ->
mxdot v v <= k%:R / (4 * beta ^+ 2 * opnorm Sigma) ->
forall [rr : probability 'rV_N R],
regular_feature K tau Sigma rr ->
\int[rr]_z
   (c0 - 2 * mxdot z v + mxdot z (z *m T) -
    \int[rr]_y (c0 - 2 * mxdot y v + mxdot y (y *m T)))
   ^+ 2 <=
2 * (Num.ExtraDef.sqrtr k%:R * (tau / opnorm Sigma + 1) / beta) ^+ 2

Proposition 2.16: the variance of l(z) is at most 2 rho^2.

Statement as written in the source

Lemma ins_l_var (rr : probability 'rV[R]_N R) :
  regular_feature K tau Sigma rr ->
  \int[rr]_z ((c0 - 2 * mxdot z v + mxdot z (z *m T) -
     \int[rr]_y (c0 - 2 * mxdot y v + mxdot y (y *m T))) ^+ 2) <=
  2 * rho ^+ 2.

Used by 1 declaration in 1 file

this file: insertion_compare

lemma insertion_compare main result source, line 648

forall {R : realType} {N : nat} [K tau : R] [Sigma : 'M_N] [mu nu : probability 'rV_N R],
regular_feature K tau Sigma mu ->
regular_feature K tau Sigma nu ->
0 <= tau ->
forall [n k : nat] [beta gamma : R],
(0 < n)%N ->
0 < beta ->
0 < gamma ->
forall [f : 'rV_N -> R] [thm v : 'rV_N] [bm c0 : R] [T : 'M_N],
measurable_fun [set: 'rV_N] f ->
(forall z : 'rV_N, 0 <= f z <= (bm - mxdot z thm) ^+ 2 / (2 * n%:R)) ->
(forall z : 'rV_N, 0 <= c0 - 2 * mxdot z v + mxdot z (z *m T)) ->
(forall z : 'rV_N,
 `|f z - (bm - mxdot z thm) ^+ 2 / (2 * (n%:R + (c0 - 2 * mxdot z v + mxdot z (z *m T))))| <=
 (2 + 3 * (bm - mxdot z thm) ^+ 4) / (n%:R * Num.ExtraDef.sqrtr (n%:R * gamma))) ->
T \is symmetricmx ->
frobenius T ^+ 2 <= k%:R / (4 * beta ^+ 2 * opnorm Sigma ^+ 2) ->
mxdot v v <= k%:R / (4 * beta ^+ 2 * opnorm Sigma) ->
`|\int[mu]_z f z - \int[nu]_z f z| <=
(4 + 48 * (1 + K ^+ 4) * (opnorm Sigma * mxdot thm thm + bm ^+ 2) ^+ 2) /
(n%:R * Num.ExtraDef.sqrtr (n%:R * gamma)) +
4 * Num.ExtraDef.sqrtr (1 + K ^+ 4) *
(Num.ExtraDef.sqrtr k%:R * (tau / opnorm Sigma + 1) / beta) *
(opnorm Sigma * mxdot thm thm + bm ^+ 2) / n%:R ^+ 2

Propositions 2.14 and 2.16: the comparison of the insertion costs.

Main result, as the README states it

Propositions 2.14 and 2.16 of Koehler and Sohn: for two regular features with the same covariance, the means of the cost of inserting one feature differ by at most (4 + 48 (1 + K^4) S^2) / (n sqrt (n gamma)) + 4 sqrt (1 + K^4) sqrt (dim V) (tau / lambda + 1) S / (beta n^2), where S = lambda |theta_m|^2 + b_m^2 is the size of the leave-one-out minimizer; for the value itself the same holds with S replaced by its bound ((2 n)^-1 sum_(j <> i) <x_j, theta_ref>^2 + beta lambda |theta_ref|^2 + gamma B theta_ref) / beta, and the variance in the coordinate i is at most 2 (1 + K^4) / n^2 times the square of that bound.

Statement as written in the source

Lemma insertion_compare :
  `|\int[mu]_z f z - \int[nu]_z f z| <=
  (4 + 48 * (1 + K ^+ 4) * S ^+ 2) / (n%:R * Num.sqrt (n%:R * gamma)) +
  4 * Num.sqrt (1 + K ^+ 4) * rho * S / n%:R ^+ 2.

Used by 1 declaration in 1 file

this file: loo_compare

sectionreference_scale

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

definition ls_ref_scale main result source, line 815

Type

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

Definition

Definition ls_ref_scale (lambda beta gamma : R) (D : set 'rV[R]_N)
    (B : 'rV[R]_N -> R) : R :=
  (1 + beta^-1) * (1 + inf [set lambda * mxdot th th + gamma * B th | th in D]).

The reference scale of the paper, (2.11).

Main result

Stated in the README together with barrier_lindeberg_mean.

Used by 6 declarations in 2 files

this file: ref_point, barrier_lindeberg_mean, ref_moment_bound, barrier_lindeberg_variance, barrier_lindeberg_concentration
GaussianAnalysis.convex.ridge_comparison: ridge_comparison

sectionbarrier_lindeberg

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).
Hypotheses (B0 : forall z, D z -> 0 <= B z) (D0 : D !=set0).
Variables (K tau : R) (Sigma : 'M[R]_N) (mu nu : probability 'rV[R]_N R).
Hypotheses (rmu : regular_feature K tau Sigma mu)
  (rnu : regular_feature K tau Sigma nu) (tau0 : 0 <= tau).
Variables (n : nat) (beta gamma : R).
Hypotheses (n0 : (0 < n)%N) (b0 : 0 < beta) (g0 : 0 < gamma).
Local Notation lambda := (opnorm Sigma).
Local Notation Phi Z := (ls_barrier_value Z (opnorm Sigma) beta D gamma B).
Local Notation s := ((n%:R *+ 2)^-1 : R).
Local Notation Sbar thr i x :=
  ((s * \sum_(j < n | j != i) mxdot (tnth x j) thr ^+ 2 +
    beta * opnorm Sigma * mxdot thr thr + gamma * B thr) / beta).
Local Notation bnd Sb :=
  ((4 + 48 * (1 + K ^+ 4) * Sb ^+ 2) / (n%:R * Num.sqrt (n%:R * gamma)) +
   4 * Num.sqrt (1 + K ^+ 4) *
     (Num.sqrt (\dim V)%:R * (tau / opnorm Sigma + 1) / beta) * Sb /
   n%:R ^+ 2).

lemma loo_compare main result source, line 845

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 -> 0 <= B z) ->
D !=set0 ->
forall [K tau : R] [Sigma : 'M_N] [mu nu : probability 'rV_N R],
regular_feature K tau Sigma mu ->
regular_feature K tau Sigma nu ->
0 <= tau ->
forall [n : nat] [beta gamma : R],
(0 < n)%N ->
0 < beta ->
0 < gamma ->
forall [thr : 'rV_N] (i : 'I_n) (x : n.-tuple 'rV_N),
D thr ->
36 <= n%:R * gamma ->
`|\int[mu]_t ls_barrier_value (tuple_set x i t) (opnorm Sigma) beta D gamma B -
  \int[nu]_t ls_barrier_value (tuple_set x i t) (opnorm Sigma) beta D gamma B| <=
(4 +
 48 * (1 + K ^+ 4) *
 ((((n%:R *+ 2)^-1 : R) * \sum_(j < n | j != i) mxdot (tnth x j) thr ^+ 2 +
   beta * opnorm Sigma * mxdot thr thr + gamma * B thr) /
  beta)
 ^+ 2) /
(n%:R * Num.ExtraDef.sqrtr (n%:R * gamma)) +
4 * Num.ExtraDef.sqrtr (1 + K ^+ 4) *
(Num.ExtraDef.sqrtr (\dim V)%:R * (tau / opnorm Sigma + 1) / beta) *
((((n%:R *+ 2)^-1 : R) * \sum_(j < n | j != i) mxdot (tnth x j) thr ^+ 2 +
  beta * opnorm Sigma * mxdot thr thr + gamma * B thr) /
 beta) /
n%:R ^+ 2

The comparison in the coordinate i, the other coordinates being fixed.

Main result

Stated in the README together with insertion_compare.

Statement as written in the source

Lemma loo_compare (thr : 'rV[R]_N) (i : 'I_n) (x : n.-tuple 'rV[R]_N) :
  D thr -> 36 <= n%:R * gamma ->
  `|\int[mu]_t Phi (tuple_set x i t) - \int[nu]_t Phi (tuple_set x i t)| <=
  bnd (Sbar thr i x).

Used by 1 declaration in 1 file

this file: barrier_lindeberg_mean

let objective_ge0 section-local source, line 938

Let objective_ge0 (Z : n.-tuple 'rV[R]_N) th b :
  0 <= ls_objective Z lambda beta th b.

Used by 2 declarations in 1 file

this file: Phi_ge0, Phi_le

lemma Phi_ge0 source, line 947

forall {R : realType} {N : nat} [D : set 'rV_N] [B : 'rV_N -> R],
(forall z : 'rV_N, D z -> 0 <= B z) ->
D !=set0 ->
forall (Sigma : 'M_N) [n : nat] [beta gamma : R],
0 < beta ->
0 < gamma ->
forall Z : n.-tuple 'rV_N, 0 <= ls_barrier_value Z (opnorm Sigma) beta D gamma B

Statement as written in the source

Lemma Phi_ge0 (Z : n.-tuple 'rV[R]_N) : 0 <= Phi Z.

Used by 3 declarations in 1 file

this file: int_Phi, int_Phi_set, barrier_lindeberg_mean

lemma Phi_le source, line 957

forall {R : realType} {N : nat} [D : set 'rV_N] [B : 'rV_N -> R],
(forall z : 'rV_N, D z -> 0 <= B z) ->
forall (Sigma : 'M_N) [n : nat] [beta gamma : R],
0 < beta ->
0 < gamma ->
forall [thr : 'rV_N] (Z : n.-tuple 'rV_N),
D thr ->
ls_barrier_value Z (opnorm Sigma) beta D gamma B <=
((n%:R *+ 2)^-1 : R) * \sum_(j < n) mxdot (tnth Z j) thr ^+ 2 +
(beta * opnorm Sigma * mxdot thr thr + gamma * B thr)

Statement as written in the source

Lemma Phi_le (thr : 'rV[R]_N) (Z : n.-tuple 'rV[R]_N) : D thr ->
  Phi Z <= s * \sum_(j < n) mxdot (tnth Z j) thr ^+ 2 +
    (beta * lambda * mxdot thr thr + gamma * B thr).

Used by 2 declarations in 1 file

this file: int_Phi, int_Phi_set

lemma Phi_meas source, line 972

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 -> 0 <= B z) ->
D !=set0 ->
forall (Sigma : 'M_N) [n : nat] [beta gamma : R],
0 < beta ->
0 < gamma ->
measurable_fun [set: n.-tuple _]
  (fun Z : n.-tuple 'rV_N => ls_barrier_value Z (opnorm Sigma) beta D gamma B)

Statement as written in the source

Lemma Phi_meas : measurable_fun setT (fun Z : n.-tuple 'rV[R]_N => Phi Z).

Used by 6 declarations in 1 file

this file: int_Phi, int_Phi_set, barrier_lindeberg_mean, loo_variance, barrier_lindeberg_variance, barrier_lindeberg_concentration

lemma hybrid_regular source, line 980

forall {R : realType} {N : nat} [K tau : R] [Sigma : 'M_N] [mu nu : probability 'rV_N R],
regular_feature K tau Sigma mu ->
regular_feature K tau Sigma nu ->
forall k j : nat, regular_feature K tau Sigma (hybrid mu nu k j)

Statement as written in the source

Lemma hybrid_regular k j : regular_feature K tau Sigma (hybrid mu nu k j).

Used by 1 declaration in 1 file

this file: barrier_lindeberg_mean

lemma int_Phi source, line 983

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 -> 0 <= B z) ->
D !=set0 ->
forall [K tau : R] [Sigma : 'M_N] (n : nat) [beta gamma : R],
0 < beta ->
0 < gamma ->
forall [rho : nat -> probability 'rV_N R],
(forall j : nat, regular_feature K tau Sigma (rho j)) ->
(tuple_prod rho n).-integrable [set: n.-tuple 'rV_N]
  (EFin \o (fun Z : n.-tuple 'rV_N => ls_barrier_value Z (opnorm Sigma) beta D gamma B))

Statement as written in the source

Lemma int_Phi (rho : nat -> probability 'rV[R]_N R) :
  (forall j, regular_feature K tau Sigma (rho j)) ->
  (tuple_prod rho n).-integrable setT (EFin \o (fun Z => Phi Z)).

Used by 2 declarations in 1 file

this file: barrier_lindeberg_mean, barrier_lindeberg_variance

lemma int_Phi_set source, line 1001

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 -> 0 <= B z) ->
D !=set0 ->
forall [K tau : R] [Sigma : 'M_N] [n : nat] [beta gamma : R],
0 < beta ->
0 < gamma ->
forall [rr : probability 'rV_N R] (i : 'I_n) (x : n.-tuple 'rV_N),
regular_feature K tau Sigma rr ->
rr.-integrable [set: 'rV_N]
  (fun t : 'rV_N => (ls_barrier_value (tuple_set x i t) (opnorm Sigma) beta D gamma B)%:E)

Statement as written in the source

Lemma int_Phi_set (rr : probability 'rV[R]_N R) (i : 'I_n)
    (x : n.-tuple 'rV[R]_N) :
  regular_feature K tau Sigma rr ->
  rr.-integrable setT (fun t => (Phi (tuple_set x i t))%:E).

Used by 1 declaration in 1 file

this file: barrier_lindeberg_mean

Local Notation Lref := (ls_ref_scale (opnorm Sigma) beta gamma D B).

lemma ref_point source, line 1031

forall {R : realType} {N : nat} [D : set 'rV_N] [B : 'rV_N -> R],
(forall z : 'rV_N, D z -> 0 <= B z) ->
D !=set0 ->
forall (Sigma : 'M_N) [beta gamma : R],
0 < beta ->
0 < gamma ->
exists2 thr : 'rV_N,
  D thr &
  [/\ 0 <= inf [set opnorm Sigma * mxdot th th + gamma * B th | th in D],
      opnorm Sigma * mxdot thr thr + gamma * B thr <=
      1 + inf [set opnorm Sigma * mxdot th th + gamma * B th | th in D]
    & 1 + beta^-1 <= ls_ref_scale (opnorm Sigma) beta gamma D B]

A reference point at which lambda |theta|^2 + gamma B theta is at most one more than its infimum.

Statement as written in the source

Lemma ref_point : exists2 thr, D thr &
  [/\ 0 <= inf [set lambda * mxdot th th + gamma * B th | th in D],
      lambda * mxdot thr thr + gamma * B thr <=
        1 + inf [set lambda * mxdot th th + gamma * B th | th in D] &
      1 + beta^-1 <= Lref].

Used by 2 declarations in 1 file

this file: barrier_lindeberg_mean, barrier_lindeberg_variance

lemma sum_pred_sqr_le source, line 1051

forall {R : realType} [n : nat] (P : pred 'I_n) [a : 'I_n -> R],
(forall j : 'I_n, 0 <= a j) ->
(\sum_(j < n | P j) a j) ^+ 2 <= n%:R * \sum_(j < n) a j ^+ 2

(Sum_(j in P) a_j)^2 <= n sum_j a_j^2.

Statement as written in the source

Lemma sum_pred_sqr_le (P : pred 'I_n) (a : 'I_n -> R) :
  (forall j, 0 <= a j) ->
  (\sum_(j < n | P j) a j) ^+ 2 <= n%:R * \sum_(j < n) a j ^+ 2.

Used by 2 declarations in 1 file

this file: barrier_lindeberg_mean, Sbar_sqr_le

theorem barrier_lindeberg_mean main result source, line 1068

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 -> 0 <= B z) ->
D !=set0 ->
forall [K tau : R] [Sigma : 'M_N] [mu nu : probability 'rV_N R],
regular_feature K tau Sigma mu ->
regular_feature K tau Sigma nu ->
0 <= tau ->
forall [n : nat] [beta gamma : R],
(0 < n)%N ->
0 < beta ->
0 < gamma ->
36 <= n%:R * gamma ->
`|\int[tuple_prod (fun=> mu) n]_Z ls_barrier_value Z (opnorm Sigma) beta D gamma B -
  \int[tuple_prod (fun=> nu) n]_Z ls_barrier_value Z (opnorm Sigma) beta D gamma B| <=
100 * (1 + K ^+ 4) ^+ 2 * ls_ref_scale (opnorm Sigma) beta gamma D B ^+ 2 *
((Num.ExtraDef.sqrtr (n%:R * gamma))^-1 +
 Num.ExtraDef.sqrtr (\dim V)%:R * (tau / opnorm Sigma + 1) / n%:R)

Theorem 2.9, (2.12).

Main result, as the README states it

Theorem 2.9 of Koehler and Sohn, for mu, nu (K, tau)-regular with the same covariance, D convex, relatively open and nonempty (not necessarily bounded), B >= 0 self-concordant on D, beta, gamma > 0 and Lref = (1 + 1/beta) (1 + inf_D (lambda |theta|^2 + gamma B theta)): if 36 <= n gamma, |E_(mu^n) Phi - E_(nu^n) Phi| <= 100 (1 + K^4)^2 Lref^2 ((n gamma)^(-1/2) + sqrt (dim V) (tau / lambda + 1) / n); Var_(mu^n) Phi <= 4 (1 + K^4)^2 Lref^2 / n; and Phi is within that bound plus t of E_(nu^n) Phi outside an event of mu^n-probability at most 4 (1 + K^4)^2 Lref^2 / (n t^2).

Statement as written in the source

Theorem barrier_lindeberg_mean : 36 <= n%:R * gamma ->
  `|\int[tuple_prod (fun=> mu) n]_Z Phi Z -
    \int[tuple_prod (fun=> nu) n]_Z Phi Z| <=
  100 * (1 + K ^+ 4) ^+ 2 * Lref ^+ 2 *
  ((Num.sqrt (n%:R * gamma))^-1 +
   Num.sqrt (\dim V)%:R * (tau / opnorm Sigma + 1) / n%:R).

Used by 1 declaration in 1 file

this file: barrier_lindeberg_concentration

lemma loo_variance main result source, line 1306

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 -> 0 <= B z) ->
D !=set0 ->
forall [K tau : R] [Sigma : 'M_N] [mu : probability 'rV_N R],
regular_feature K tau Sigma mu ->
forall [n : nat] [beta gamma : R],
(0 < n)%N ->
0 < beta ->
0 < gamma ->
forall [thr : 'rV_N] (i : 'I_n) (x : n.-tuple 'rV_N),
D thr ->
('V_mu[(fun t : 'rV_N => ls_barrier_value (tuple_set x i t) (opnorm Sigma) beta D gamma B)] <=
 (2 * (1 + K ^+ 4) / n%:R ^+ 2 *
  ((((n%:R *+ 2)^-1 : R) * \sum_(j < n | j != i) mxdot (tnth x j) thr ^+ 2 +
    beta * opnorm Sigma * mxdot thr thr + gamma * B thr) /
   beta)
  ^+ 2)%:E)%E

The variance in the coordinate i, the other coordinates being fixed.

Main result

Stated in the README together with insertion_compare.

Statement as written in the source

Lemma loo_variance (thr : 'rV[R]_N) (i : 'I_n) (x : n.-tuple 'rV[R]_N) :
  D thr ->
  ('V_mu[fun t => Phi (tuple_set x i t)] <=
    (2 * (1 + K ^+ 4) / n%:R ^+ 2 * (Sbar thr i x) ^+ 2)%:E)%E.

Used by 1 declaration in 1 file

this file: barrier_lindeberg_variance

lemma Sbar_sqr_le source, line 1367

forall {R : realType} {N : nat} (B : 'rV_N -> R) (Sigma : 'M_N) 
  [n : nat] [beta : R] (gamma : R),
0 < beta ->
forall (thr : 'rV_N) (i : 'I_n) (x : n.-tuple 'rV_N),
((((n%:R *+ 2)^-1 : R) * \sum_(j < n | j != i) mxdot (tnth x j) thr ^+ 2 +
  beta * opnorm Sigma * mxdot thr thr + gamma * B thr) /
 beta)
^+ 2 <=
(2 * ((n%:R *+ 2)^-1 : R) ^+ 2 * n%:R * \sum_(j < n) mxdot (tnth x j) thr ^+ 4 +
 2 * (beta * opnorm Sigma * mxdot thr thr + gamma * B thr) ^+ 2) /
beta ^+ 2

Statement as written in the source

Lemma Sbar_sqr_le (thr : 'rV[R]_N) (i : 'I_n) (x : n.-tuple 'rV[R]_N) :
  (Sbar thr i x) ^+ 2 <=
  (2 * s ^+ 2 * n%:R * \sum_(j < n) mxdot (tnth x j) thr ^+ 4 +
   2 * (beta * lambda * mxdot thr thr + gamma * B thr) ^+ 2) / beta ^+ 2.

Used by 1 declaration in 1 file

this file: barrier_lindeberg_variance

lemma int_P4 source, line 1387

forall {R : realType} {N : nat} [K tau : R] [Sigma : 'M_N] (n : nat)
  [rho : nat -> probability 'rV_N R] (thr : 'rV_N),
(forall j : nat, regular_feature K tau Sigma (rho j)) ->
(tuple_prod rho n).-integrable [set: n.-tuple 'rV_N]
  (EFin \o (fun x : n.-tuple 'rV_N => \sum_(j < n) mxdot (tnth x j) thr ^+ 4)) /\
\int[tuple_prod rho n]_x \sum_(j < n) mxdot (tnth x j) thr ^+ 4 <=
n%:R * (K ^+ 4 * opnorm Sigma ^+ 2 * mxdot thr thr ^+ 2)

Statement as written in the source

Lemma int_P4 (rho : nat -> probability 'rV[R]_N R) (thr : 'rV[R]_N) :
  (forall j, regular_feature K tau Sigma (rho j)) ->
  (tuple_prod rho n).-integrable setT
    (EFin \o (fun x => \sum_(j < n) mxdot (tnth x j) thr ^+ 4)) /\
  \int[tuple_prod rho n]_x (\sum_(j < n) mxdot (tnth x j) thr ^+ 4) <=
    n%:R * (K ^+ 4 * lambda ^+ 2 * mxdot thr thr ^+ 2).

Used by 1 declaration in 1 file

this file: barrier_lindeberg_variance

lemma ref_moment_bound source, line 1410

forall {R : realType} {N : nat} [D : set 'rV_N] [B : 'rV_N -> R],
(forall z : 'rV_N, D z -> 0 <= B z) ->
forall [K tau : R] [Sigma : 'M_N] [mu : probability 'rV_N R],
regular_feature K tau Sigma mu ->
forall [n : nat] [beta gamma : R],
(0 < n)%N ->
0 < beta ->
0 < gamma ->
forall [thr : 'rV_N],
D thr ->
opnorm Sigma * mxdot thr thr + gamma * B thr <=
1 + inf [set opnorm Sigma * mxdot th th + gamma * B th | th in D] ->
(2 * ((n%:R *+ 2)^-1 : R) ^+ 2 * n%:R *
 (n%:R * (K ^+ 4 * opnorm Sigma ^+ 2 * mxdot thr thr ^+ 2)) +
 2 * (beta * opnorm Sigma * mxdot thr thr + gamma * B thr) ^+ 2) /
beta ^+ 2 <= 2 * (1 + K ^+ 4) * ls_ref_scale (opnorm Sigma) beta gamma D B ^+ 2

E Sbar^2 <= 2 (1 + K^4) Lref^2 at a reference point.

Statement as written in the source

Lemma ref_moment_bound (thr : 'rV[R]_N) : D thr ->
  opnorm Sigma * mxdot thr thr + gamma * B thr <=
    1 + inf [set opnorm Sigma * mxdot th th + gamma * B th | th in D] ->
  (2 * s ^+ 2 * n%:R * (n%:R * (K ^+ 4 * lambda ^+ 2 * mxdot thr thr ^+ 2)) +
   2 * (beta * lambda * mxdot thr thr + gamma * B thr) ^+ 2) / beta ^+ 2 <=
  2 * (1 + K ^+ 4) * Lref ^+ 2.

Used by 1 declaration in 1 file

this file: barrier_lindeberg_variance

theorem barrier_lindeberg_variance main result source, line 1463

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 -> 0 <= B z) ->
D !=set0 ->
forall [K tau : R] [Sigma : 'M_N] [mu : probability 'rV_N R],
regular_feature K tau Sigma mu ->
forall [n : nat] [beta gamma : R],
(0 < n)%N ->
0 < beta ->
0 < gamma ->
('V_(tuple_prod (fun=> mu) n)[(fun Z : n.-tuple 'rV_N =>
                               ls_barrier_value Z (opnorm Sigma) beta D gamma B)] <=
 (4 * (1 + K ^+ 4) ^+ 2 * ls_ref_scale (opnorm Sigma) beta gamma D B ^+ 2 / n%:R)%:E)%E

Theorem 2.9, (2.13): the variance of the value, for the law mu (and, the hypotheses being symmetric, for nu).

Main result

Stated in the README together with barrier_lindeberg_mean.

Statement as written in the source

Theorem barrier_lindeberg_variance :
  ('V_(tuple_prod (fun=> mu) n)[fun Z => Phi Z] <=
    (4 * (1 + K ^+ 4) ^+ 2 * Lref ^+ 2 / n%:R)%:E)%E.

Used by 1 declaration in 1 file

this file: barrier_lindeberg_concentration

theorem barrier_lindeberg_concentration main result source, line 1525

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 -> 0 <= B z) ->
D !=set0 ->
forall [K tau : R] [Sigma : 'M_N] [mu nu : probability 'rV_N R],
regular_feature K tau Sigma mu ->
regular_feature K tau Sigma nu ->
0 <= tau ->
forall [n : nat] [beta gamma : R],
(0 < n)%N ->
0 < beta ->
0 < gamma ->
forall [t : R],
0 < t ->
36 <= n%:R * gamma ->
(tuple_prod (fun=> mu) n
   [set Z | (100 * (1 + K ^+ 4) ^+ 2 * ls_ref_scale (opnorm Sigma) beta gamma D B ^+ 2 *
             ((Num.ExtraDef.sqrtr (n%:R * gamma))^-1 +
              Num.ExtraDef.sqrtr (\dim V)%:R * (tau / opnorm Sigma + 1) / n%:R) +
             t <
             `|ls_barrier_value Z (opnorm Sigma) beta D gamma B -
               \int[tuple_prod (fun=> nu) n]_Z0
                  ls_barrier_value Z0 (opnorm Sigma) beta D gamma B|)%R] <=
 (4 * (1 + K ^+ 4) ^+ 2 * ls_ref_scale (opnorm Sigma) beta gamma D B ^+ 2 / (n%:R * t ^+ 2))%:E)%E

Theorem 2.9, (2.14), for the law mu (and, the hypotheses being symmetric, for nu): the value is close to the mean of the value under nu^n.

Main result

Stated in the README together with barrier_lindeberg_mean.

Statement as written in the source

Theorem barrier_lindeberg_concentration (t : R) :
  0 < t -> 36 <= n%:R * gamma ->
  (tuple_prod (fun=> mu) n
     [set Z | (100 * (1 + K ^+ 4) ^+ 2 * Lref ^+ 2 *
        ((Num.sqrt (n%:R * gamma))^-1 +
         Num.sqrt (\dim V)%:R * (tau / opnorm Sigma + 1) / n%:R) + t <
        `|Phi Z - \int[tuple_prod (fun=> nu) n]_Z Phi Z|)%R] <=
   (4 * (1 + K ^+ 4) ^+ 2 * Lref ^+ 2 / (n%:R * t ^+ 2))%:E)%E.

Used by 1 declaration in 1 file

GaussianAnalysis.convex.ridge_comparison: ridge_comparison

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.