On this page
Least squares values with a ridge and without barrier
Imports 10 library modules and 24 external
- GaussianAnalysis.gaussian.measurable_matrix
- GaussianAnalysis.matrix.euclidean
- GaussianAnalysis.matrix.opnorm
- GaussianAnalysis.convex.self_concordant
- GaussianAnalysis.probability.tuple_rows
- GaussianAnalysis.convex.least_squares
- GaussianAnalysis.convex.feature_moments
- GaussianAnalysis.probability.lindeberg
- GaussianAnalysis.convex.barrier_lindeberg
- GaussianAnalysis.convex.barrier_removal
External: HB.structures, mathcomp.classical.all_ssreflect_compat, mathcomp.algebra.algebraic_hierarchy.ssralg, mathcomp.algebra.numeric_hierarchy.ssrnum, mathcomp.algebra.matrix, mathcomp.algebra.vector, mathcomp.algebra.sesquilinear, mathcomp.algebra.interval, mathcomp.classical.boolp, mathcomp.classical.classical_sets, mathcomp.classical.functions, mathcomp.reals.reals, mathcomp.analysis.ereal, mathcomp.analysis.topology_theory.topology, mathcomp.analysis.normedtype_theory.normedtype, 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
The comparison of ridge-regularized least squares values of Koehler and Sohn (arXiv 2608.27372, proposition at lines 6365-6416, proof at lines 6418-6460), as a concentration inequality: Theorem 2.9 for the values with a barrier (barrier_lindeberg.v), Lemma 2.11 to remove the barrier (barrier_removal.v), and Markov's inequality for the objective at a reference point. The weight gamma of the barrier and the contraction eps of Lemma 2.11 stay free; the paper fixes them as functions of n.
Setting: 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, and theta_0 is in D; mu and nu are (K, tau)-regular features with the same covariance Sigma, and lambda = opnorm Sigma; n > 0, beta > 0, gamma > 0, 0 < eps < 1 and 36 <= n gamma. Phi_Z(D; beta) is ls_value Z lambda beta D, Phi_Z(D, B; beta, gamma) is ls_barrier_value and Lref is ls_ref_scale lambda beta gamma D B (barrier_lindeberg.v).
- measurable_ls_value: Phi_Z(D; beta) is a measurable function of Z, as the value with a barrier of weight 0 (ls_value_barrierE of least_squares.v).
- markov_lt: P(f > M) <= E f / M for f >= 0 integrable and M > 0.
- ref_objective_mean: under mu^n,
E F_Z(theta_0, 0; beta) = theta_0 Sigma theta_0^T / 2 + beta lambda |theta_0|^2. - ridge_comparison: with c = E_(nu^n) Phi_Z(D, B; beta, gamma), for t > 0 and M > 0, the mu^n-probability that
|Phi_Z(D; beta) - c| > E + t + eps M + gamma B theta_0 + gamma theta ln (1 / eps)is at most
4 (1 + K^4)^2 Lref^2 / (n t^2) + (theta_0 Sigma theta_0^T / 2 + beta lambda |theta_0|^2) / M,
where E = 100 (1 + K^4)^2 Lref^2 ((n gamma)^(-1/2) + sqrt (dim V) (tau / lambda + 1) / n) is the bound of (2.12). The hypotheses are symmetric in mu and nu, so the same holds under nu^n.
Main results
| Results | Statement |
|---|---|
The comparison of ridge-regularized least squares values of Koehler and Sohn (proposition at lines 6365-6416), as a concentration inequality with the barrier weight gamma and the contraction eps left free: for mu, nu (K, tau)-regular with the same covariance, B >= 0 a theta-self-concordant barrier on D, theta_0 in D, t, M > 0 and 36 <= n gamma, the mu^n-probability that |Phi_Z(D; beta) - E_(nu^n) Phi_Z(D, B; beta, gamma)| exceeds the bound of (2.12) plus t + eps M + gamma B theta_0 + gamma theta ln (1 / eps) is at most 4 (1 + K^4)^2 Lref^2 / (n t^2) + (theta_0 Sigma theta_0^T / 2 + beta lambda |theta_0|^2) / M (Theorem 2.9, Lemma 2.11 and Markov's inequality for F_Z(theta_0, 0; beta), whose mean is the last numerator). | |
Phi_Z(D; beta) is the value with a barrier of weight 0, hence a measurable function of the features for D convex, relatively open and nonempty; Markov's inequality P(f > M) <= E f / M for f >= 0 integrable. |
Declarations7 exported
Context {R : realType} {N : nat}.
forall {R : realType} {N : nat} [V : {vspace 'rV_N}] [D : set 'rV_N] [n : nat] [lambda beta : R], rel_open_convex V D -> D !=set0 -> 0 <= lambda -> 0 <= beta -> measurable_fun [set: n.-tuple _] (fun Z : n.-tuple 'rV_N => ls_value Z lambda beta D)
Phi_Z(D; beta) is the value with a barrier of weight 0, hence a measurable function of the features for D convex, relatively open and nonempty; Markov's inequality P(f > M) <= E f / M for f >= 0 integrable.
Statement as written in the source
Lemma measurable_ls_value (V : {vspace 'rV[R]_N}) (D : set 'rV[R]_N) n (lambda beta : R) : rel_open_convex V D -> D !=set0 -> 0 <= lambda -> 0 <= beta -> measurable_fun setT (fun Z : n.-tuple 'rV[R]_N => ls_value Z lambda beta D).
Used by 1 declaration in 1 file
- this file: ridge_comparison
forall {R : realType} [d : measure_display] [T : measurableType d] [f : T -> R] (a : R), measurable_fun [set: T] f -> d.-measurable [set x | a < f x]
Statement as written in the source
Lemma measurable_set_lt d (T : measurableType d) (f : T -> R) (a : R) : measurable_fun setT f -> measurable [set x | a < f x].
Used by 2 declarations in 1 file
- this file: markov_lt, ridge_comparison
Context d (T : measurableType d) (R : realType) (P : probability T R).
forall [d : measure_display] [T : measurableType d] [R : realType] [P : probability T R] [f : T -> R] [M : R], 0 < M -> measurable_fun [set: T] f -> (forall x : T, 0 <= f x) -> P.-integrable [set: T] (EFin \o f) -> (P [set x | (M < f x)%R] <= (\int[P]_x f x / M)%:E)%E
Markov's inequality, for a strict inequality.
Stated in the README together with measurable_ls_value.
Statement as written in the source
Lemma markov_lt (f : T -> R) (M : R) : 0 < M -> measurable_fun setT f -> (forall x, 0 <= f x) -> P.-integrable setT (EFin \o f) -> (P [set x | (M < f x)%R] <= ((\int[P]_x f x) / M)%:E)%E.
Used by 1 declaration in 1 file
- this file: ridge_comparison
Context {R : realType} {N : nat}. Variables (K tau : R) (Sigma : 'M[R]_N) (mu : probability 'rV[R]_N R). Hypothesis rmu : regular_feature K tau Sigma mu.
forall {R : realType} {N : nat} [n : nat] (Z : n.-tuple 'rV_N) (lambda beta : R) (thr : 'rV_N), ls_objective Z lambda beta thr 0 = (n%:R *+ 2)^-1 * \sum_(j < n) mxdot (tnth Z j) thr ^+ 2 + beta * lambda * mxdot thr thr
Statement as written in the source
Lemma ref_objectiveE n (Z : n.-tuple 'rV[R]_N) (lambda beta : R) (thr : 'rV[R]_N) : ls_objective Z lambda beta thr 0 = (n%:R *+ 2)^-1 * \sum_(j < n) mxdot (tnth Z j) thr ^+ 2 + beta * lambda * mxdot thr thr.
Used by 3 declarations in 1 file
- this file: ref_objective_int, ref_objective_mean, ridge_comparison
forall {R : realType} {N : nat} [K tau : R] [Sigma : 'M_N] [mu : probability 'rV_N R], regular_feature K tau Sigma mu -> forall (n : nat) (lambda beta : R) (thr : 'rV_N), (tuple_prod (fun=> mu) n).-integrable [set: n.-tuple 'rV_N] (EFin \o (fun Z : n.-tuple 'rV_N => ls_objective Z lambda beta thr 0))
Statement as written in the source
Lemma ref_objective_int n (lambda beta : R) (thr : 'rV[R]_N) : (tuple_prod (fun=> mu) n).-integrable setT (EFin \o (fun Z => ls_objective Z lambda beta thr 0)).
Used by 1 declaration in 1 file
- this file: ridge_comparison
forall {R : realType} {N : nat} [K tau : R] [Sigma : 'M_N] [mu : probability 'rV_N R], regular_feature K tau Sigma mu -> forall [n : nat] (lambda beta : R) (thr : 'rV_N), (0 < n)%N -> \int[tuple_prod (fun=> mu) n]_Z ls_objective Z lambda beta thr 0 = mxdot (thr *m Sigma) thr / 2 + beta * lambda * mxdot thr thr
Stated in the README together with ridge_comparison.
Statement as written in the source
Lemma ref_objective_mean n (lambda beta : R) (thr : 'rV[R]_N) : (0 < n)%N -> \int[tuple_prod (fun=> mu) n]_Z ls_objective Z lambda beta thr 0 = mxdot (thr *m Sigma) thr / 2 + beta * lambda * mxdot thr thr.
Used by 1 declaration in 1 file
- this file: ridge_comparison
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). 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 eps : R) (thr : 'rV[R]_N). Hypotheses (n0 : (0 < n)%N) (b0 : 0 < beta) (g0 : 0 < gamma). Hypotheses (e01 : 0 < eps < 1) (Dthr : D thr). Local Notation lambda := (opnorm Sigma). Local Notation Phi Z := (ls_value Z (opnorm Sigma) beta D). Local Notation Psi Z := (ls_barrier_value Z (opnorm Sigma) beta D gamma B). Local Notation Lref := (ls_ref_scale (opnorm Sigma) beta gamma D B).
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 [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 eps : R] [thr : 'rV_N], (0 < n)%N -> 0 < beta -> 0 < gamma -> 0 < eps < 1 -> D thr -> forall [t M : R], 0 < t -> 0 < M -> 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 + (eps * M + gamma * B thr + gamma * theta * ln eps^-1) < `|ls_value Z (opnorm Sigma) beta D - \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) + (mxdot (thr *m Sigma) thr / 2 + beta * opnorm Sigma * mxdot thr thr) / M)%:E)%E
The comparison of ridge-regularized least squares values of Koehler and Sohn (proposition at lines 6365-6416), as a concentration inequality with the barrier weight gamma and the contraction eps left free: for mu, nu (K, tau)-regular with the same covariance, B >= 0 a theta-self-concordant barrier on D, theta_0 in D, t, M > 0 and 36 <= n gamma, the mu^n-probability that |Phi_Z(D; beta) - E_(nu^n) Phi_Z(D, B; beta, gamma)| exceeds the bound of (2.12) plus t + eps M + gamma B theta_0 + gamma theta ln (1 / eps) is at most 4 (1 + K^4)^2 Lref^2 / (n t^2) + (theta_0 Sigma theta_0^T / 2 + beta lambda |theta_0|^2) / M (Theorem 2.9, Lemma 2.11 and Markov's inequality for F_Z(theta_0, 0; beta), whose mean is the last numerator).
Statement as written in the source
Theorem ridge_comparison (t M : R) : 0 < t -> 0 < M -> 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 / lambda + 1) / n%:R) + t + (eps * M + gamma * B thr + gamma * theta * ln eps^-1) < `|Phi Z - \int[tuple_prod (fun=> nu) n]_Z Psi Z|)%R] <= (4 * (1 + K ^+ 4) ^+ 2 * Lref ^+ 2 / (n%:R * t ^+ 2) + (mxdot (thr *m Sigma) thr / 2 + beta * lambda * mxdot thr thr) / M)%:E)%E.