On this page

Constrained least squares with features, and regular features

GaussianAnalysis.convex.least_squareslibrary/convex/least_squares.v254 lines9 lemmas and theorems, 7 definitionssource

Imports 3 library modules and 17 external

External: HB.structures, mathcomp.classical.all_ssreflect_compat, mathcomp.algebra.algebraic_hierarchy.ssralg, mathcomp.algebra.numeric_hierarchy.ssrnum, mathcomp.algebra.matrix, mathcomp.algebra.sesquilinear, 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.measure_theory.measure, mathcomp.analysis.lebesgue_measure, mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral, mathcomp.analysis.probability_theory.probability

Imported by 9

Required by 17 files of the paper proofs

The objects of the Lindeberg argument of Koehler and Sohn (Universality and sharp thresholds for ellipsoid fitting, arXiv 2608.27372, section 2.2): n features Z_1, ..., Z_n in 'rV[R]_N, the ridge-regularized least squares objective in (theta, b), its infimum over theta in a convex set D with an optional barrier B, and the regular features of their Definition 2.5. Features are n-tuples, so that their law is tuple_prod of probability/lindeberg.v; <x, y> is mxdot x y and |x|^2 is mxdot x x.

`ls_objective Z lambda beta theta b`	F_Z(theta, b; beta), the average (2 n)^-1 sum_i (b - <Z_i, theta>)^2 plus the ridge term beta (lambda \|theta\|^2 + b^2)
`ls_loss Z P theta b`	sum_(i in P) (b - <Z_i, theta>)^2
`ls_ridge Z P s lambda beta theta b`	s ls_loss Z P theta b + beta (lambda \|theta\|^2 + b^2)
`ls_barrier_objective Z P s lambda beta gamma B theta b`	ls_ridge Z P s lambda beta theta b + gamma B theta; with P the indices other than i and s = (2 n)^-1, the leave-one-out objective F^(i) of the paper
`ls_barrier_value Z lambda beta D gamma B`	Phi_Z(D, B; beta, gamma), the infimum of F_Z(theta, b; beta) + gamma B theta over theta in D and b real
`ls_value Z lambda beta D`	Phi_Z(D; beta), the infimum of F_Z(theta, b; beta) over theta in D and b real; Phi_Z(D) is ls_value Z lambda 0 D, for any lambda
`regular_feature K tau Sigma mu`	the law mu on 'rV[R]_N is a (K, tau)-regular feature with covariance Sigma: lambda = opnorm Sigma > 0, (F1) E <Z, theta>^4 <= K^4 lambda^2 \|theta\|^4, mean 0, E <Z, theta> <Z, theta'> = theta Sigma theta'^T and (F2) Var (Z T Z^T) <= tau^2 \|T\|_F^2 for T symmetric

The paper's lambda is the operator norm opnorm Sigma; the definitions take it as a parameter, so that they do not depend on a law.

Main results, for lambda, beta, gamma >= 0 and B >= 0 on D:

ls_objective_ge0: F_Z(theta, b; beta) >= 0.
ls_barrier_value_le, ls_barrier_value_ge0: Phi_Z(D, B; beta, gamma) is at most F_Z(theta, b; beta) + gamma B theta for every theta in D and every real b, and it is nonnegative.
ls_value_barrierE: Phi_Z(D; beta) is the value with a barrier of weight 0; ls_value_le and ls_value_ge0 are the same bounds for it.
ls_barrier_value_mono, ls_value_mono: the values are nondecreasing in beta.

Over an empty D both values are 0 (ls_barrier_value_empty).

Elsewhere in the library. The values are measurable functions of the n-tuple Z when D is nonempty, convex and relatively open and B >= 0 is continuous on D (measurable_ls_barrier_value in barrier_lindeberg.v, measurable_ls_value in ridge_comparison.v), and so is the minimizer (measurable_ls_min, probability/measurable_minimizer.v). For a regular feature, the fourth moments of the linear forms are finite and every measurable g with |g z| <= a + b |z|^4 is integrable (reg_int4, reg_integrable in feature_moments.v); under the hypotheses of Theorem 2.9, Phi_Z(D, B; beta, gamma) is integrable for n independent regular features (int_Phi, barrier_lindeberg.v). Gaussian features are regular (gauss_regular_feature, gauss_feature.v).

Main results

Results	Statement
ls_lossls_ridgels_barrier_objective	The least squares objective with a selection `P` of the features and a weight `s`: `s sum_(i in P) (b - <Z_i, theta>)^2 + beta (lambda \|theta\|^2 + b^2) + gamma B theta`; with `P` the indices other than `i` and `s = 1 / (2 n)` it is the leave-one-out objective of the Lindeberg argument.

Declarations16 exported

sectionleast_squares

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

definition ls_objective source, line 85

Type

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

Definition

Definition ls_objective n (Z : n.-tuple 'rV[R]_N) (lambda beta : R)
    (theta : 'rV[R]_N) (b : R) : R :=
  (n%:R *+ 2)^-1 * \sum_(i < n) (b - mxdot (tnth Z i) theta) ^+ 2 +
  beta * (lambda * mxdot theta theta + b ^+ 2).

Used by 19 declarations in 5 files

this file: ls_barrier_value, ls_value, ls_objective_ge0, ls_barrier_value_le, ls_barrier_value_ge0, ls_barrier_value_mono, ls_value_le
GaussianAnalysis.convex.ls_insertion: ins_objective
GaussianAnalysis.convex.barrier_removal: ls_objective_convex, barrier_removal, barrier_removal_compare
GaussianAnalysis.convex.barrier_lindeberg: ls_barrier_valueE, objective_ge0, Phi_ge0, Phi_le
GaussianAnalysis.convex.ridge_comparison: ref_objectiveE, ref_objective_int, ref_objective_mean, ridge_comparison

definition ls_loss main result source, line 90

Type

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

Definition

Definition ls_loss n (Z : n.-tuple 'rV[R]_N) (P : pred 'I_n)
    (theta : 'rV[R]_N) (b : R) : R :=
  \sum_(i < n | P i) (b - mxdot (tnth Z i) theta) ^+ 2.

Main result, as the README states it

The least squares objective with a selection P of the features and a weight s: s sum_(i in P) (b - <Z_i, theta>)^2 + beta (lambda |theta|^2 + b^2) + gamma B theta; with P the indices other than i and s = 1 / (2 n) it is the leave-one-out objective of the Lindeberg argument.

Used by 9 declarations in 5 files

GaussianAnalysis.probability.measurable_minimizer: ls_reduced_tuple_set
this file: ls_ridge
GaussianAnalysis.convex.minimizers: ls_ridge_expand, ls_ridge_bopt, continuous_ls_reduced
GaussianAnalysis.convex.ls_insertion: ins_hform_ridge, ins_objective, ins_size_le
GaussianAnalysis.convex.barrier_lindeberg: measurable_ls_reduced

definition ls_ridge main result source, line 94

Type

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

Definition

Definition ls_ridge n (Z : n.-tuple 'rV[R]_N) (P : pred 'I_n)
    (s lambda beta : R) (theta : 'rV[R]_N) (b : R) : R :=
  s * ls_loss Z P theta b + beta * (lambda * mxdot theta theta + b ^+ 2).

Main result

Stated in the README together with ls_loss.

Used by 22 declarations in 5 files

GaussianAnalysis.probability.measurable_minimizer: ls_reduced, ls_min_exists, ls_reduced_tuple_set
this file: ls_barrier_objective
GaussianAnalysis.convex.minimizers: ls_ridge_expand, ls_ridge_bopt, ls_ridge_ge0, ls_ridge_coercive, continuous_ls_reduced, convex_ls_reduced, ls_barrier_minimizer, ls_first_order, ls_taylor
GaussianAnalysis.convex.ls_insertion: ins_hform_ridge, ins_ridge_ge, ins_objective, ins_cost_lower, ins_size_le
GaussianAnalysis.convex.barrier_lindeberg: measurable_ls_reduced, ls_ridge_ge0', ls_barrier_valueE, measurable_ls_barrier_value

definition ls_barrier_objective main result source, line 98

Type

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

Definition

Definition ls_barrier_objective n (Z : n.-tuple 'rV[R]_N) (P : pred 'I_n)
    (s lambda beta gamma : R) B (theta : 'rV[R]_N) (b : R) : R :=
  ls_ridge Z P s lambda beta theta b + gamma * B theta.

Main result

Stated in the README together with ls_loss.

Used by 16 declarations in 4 files

GaussianAnalysis.probability.measurable_minimizer: ls_reduced_le, ls_minP, ls_min_growth
GaussianAnalysis.convex.minimizers: ls_barrier_minimizer, ls_first_order, ls_taylor
GaussianAnalysis.convex.ls_insertion: ins_cost, ins_objective, ins_taylor, ins_cost_set, ins_cost_bounds, ins_cost_upper, ins_cost_lower, ins_size_le
GaussianAnalysis.convex.barrier_lindeberg: loo_compare, loo_variance

definition ls_barrier_value source, line 102

Type

forall {R : realType} {N : nat} [n : nat],
n.-tuple 'rV_N -> R -> R -> set 'rV_N -> R -> ('rV_N -> R) -> R

Definition

Definition ls_barrier_value n (Z : n.-tuple 'rV[R]_N) (lambda beta : R) D
    (gamma : R) B : R :=
  inf [set ls_objective Z lambda beta theta b + gamma * B theta |
       theta in D & b in [set: R]].

Used by 23 declarations in 5 files

this file: ls_value_barrierE, ls_barrier_value_empty, ls_barrier_value_le, ls_barrier_value_ge0, ls_barrier_value_mono
GaussianAnalysis.convex.ls_insertion: ins_cost, ins_cost_set
GaussianAnalysis.convex.barrier_removal: barrier_removal, barrier_removal_compare
GaussianAnalysis.convex.barrier_lindeberg: ls_barrier_valueE, measurable_ls_barrier_value, loo_compare, Phi_ge0, Phi_le, Phi_meas, int_Phi, int_Phi_set, barrier_lindeberg_mean, loo_variance, barrier_lindeberg_variance, barrier_lindeberg_concentration
GaussianAnalysis.convex.ridge_comparison: measurable_ls_value, ridge_comparison

definition ls_value source, line 107

Type

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

Definition

Definition ls_value n (Z : n.-tuple 'rV[R]_N) (lambda beta : R) D : R :=
  inf [set ls_objective Z lambda beta theta b | theta in D & b in [set: R]].

Used by 8 declarations in 3 files

this file: ls_value_barrierE, ls_value_le, ls_value_ge0, ls_value_mono
GaussianAnalysis.convex.barrier_removal: barrier_removal, barrier_removal_compare
GaussianAnalysis.convex.ridge_comparison: measurable_ls_value, ridge_comparison

sectionleast_squares_values

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

lemma ls_objective_ge0 source, line 116

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

Statement as written in the source

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

Used by 5 declarations in 3 files

this file: ls_barrier_value_le, ls_barrier_value_ge0, ls_barrier_value_mono
GaussianAnalysis.convex.barrier_removal: barrier_removal
GaussianAnalysis.convex.ridge_comparison: ridge_comparison

lemma ls_value_barrierE main result source, line 126

forall {R : realType} {N : nat} [n : nat] (Z : n.-tuple 'rV_N) 
  (lambda beta : R) (D : set 'rV_N) (B : 'rV_N -> R),
ls_value Z lambda beta D = ls_barrier_value Z lambda beta D 0 B

Phi_Z(D; beta) is the value with a barrier of weight 0.

Main result

Stated in the README together with measurable_ls_value.

Statement as written in the source

Lemma ls_value_barrierE n (Z : n.-tuple 'rV[R]_N) (lambda beta : R)
    (D : set 'rV[R]_N) (B : 'rV[R]_N -> R) :
  ls_value Z lambda beta D = ls_barrier_value Z lambda beta D 0 B.

Used by 4 declarations in 2 files

this file: ls_value_le, ls_value_ge0, ls_value_mono
GaussianAnalysis.convex.ridge_comparison: measurable_ls_value

lemma ls_barrier_value_empty source, line 135

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

Statement as written in the source

Lemma ls_barrier_value_empty n (Z : n.-tuple 'rV[R]_N) (lambda beta : R) D
    (gamma : R) B :
  ~ (D !=set0) -> ls_barrier_value Z lambda beta D gamma B = 0.

Used by 2 declarations in 1 file

this file: ls_barrier_value_ge0, ls_barrier_value_mono

lemma ls_barrier_value_le source, line 144

forall {R : realType} {N : nat} [n : nat] (Z : n.-tuple 'rV_N) 
  [lambda beta : R] [D : set 'rV_N] [gamma : R] [B : 'rV_N -> R] 
  [th : 'rV_N] (b : R),
0 <= lambda ->
0 <= beta ->
0 <= gamma ->
(forall z : 'rV_N, D z -> 0 <= B z) ->
D th ->
ls_barrier_value Z lambda beta D gamma B <= ls_objective Z lambda beta th b + gamma * B th

Statement as written in the source

Lemma ls_barrier_value_le n (Z : n.-tuple 'rV[R]_N) (lambda beta : R) D
    (gamma : R) B th b :
  0 <= lambda -> 0 <= beta -> 0 <= gamma -> (forall z, D z -> 0 <= B z) ->
  D th ->
  ls_barrier_value Z lambda beta D gamma B <=
    ls_objective Z lambda beta th b + gamma * B th.

Used by 1 declaration in 1 file

this file: ls_value_le

lemma ls_barrier_value_ge0 source, line 159

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

Statement as written in the source

Lemma ls_barrier_value_ge0 n (Z : n.-tuple 'rV[R]_N) (lambda beta : R) D
    (gamma : R) B :
  0 <= lambda -> 0 <= beta -> 0 <= gamma -> (forall z, D z -> 0 <= B z) ->
  0 <= ls_barrier_value Z lambda beta D gamma B.

Used by 1 declaration in 1 file

this file: ls_value_ge0

lemma ls_barrier_value_mono source, line 174

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

Statement as written in the source

Lemma ls_barrier_value_mono n (Z : n.-tuple 'rV[R]_N) (lambda beta beta' : R)
    D (gamma : R) B :
  0 <= lambda -> 0 <= beta -> beta <= beta' -> 0 <= gamma ->
  (forall z, D z -> 0 <= B z) ->
  ls_barrier_value Z lambda beta D gamma B <=
    ls_barrier_value Z lambda beta' D gamma B.

Used by 1 declaration in 1 file

this file: ls_value_mono

lemma ls_value_le source, line 201

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

Statement as written in the source

Lemma ls_value_le n (Z : n.-tuple 'rV[R]_N) (lambda beta : R) D th b :
  0 <= lambda -> 0 <= beta -> D th ->
  ls_value Z lambda beta D <= ls_objective Z lambda beta th b.

lemma ls_value_ge0 source, line 212

forall {R : realType} {N : nat} [n : nat] (Z : n.-tuple 'rV_N) 
  [lambda beta : R] (D : set 'rV_N),
0 <= lambda -> 0 <= beta -> 0 <= ls_value Z lambda beta D

Statement as written in the source

Lemma ls_value_ge0 n (Z : n.-tuple 'rV[R]_N) (lambda beta : R) D :
  0 <= lambda -> 0 <= beta -> 0 <= ls_value Z lambda beta D.

lemma ls_value_mono source, line 222

forall {R : realType} {N : nat} [n : nat] (Z : n.-tuple 'rV_N) 
  [lambda beta beta' : R] (D : set 'rV_N),
0 <= lambda ->
0 <= beta -> beta <= beta' -> ls_value Z lambda beta D <= ls_value Z lambda beta' D

Statement as written in the source

Lemma ls_value_mono n (Z : n.-tuple 'rV[R]_N) (lambda beta beta' : R) D :
  0 <= lambda -> 0 <= beta -> beta <= beta' ->
  ls_value Z lambda beta D <= ls_value Z lambda beta' D.

sectionregular_feature

Context {R : realType} {N : nat}.
Local Open Scope ereal_scope.

definition regular_feature source, line 241

Type

forall {R : realType} {N : nat}, R -> R -> 'M_N -> probability 'rV_N R -> Prop

Definition

Definition regular_feature (K tau : R) (Sigma : 'M[R]_N)
    (mu : probability 'rV[R]_N R) : Prop :=
  [/\ (0 < opnorm Sigma)%R,
      forall theta : 'rV[R]_N,
        'E_mu[fun z => (mxdot z theta ^+ 4)%R] <=
          (K ^+ 4 * opnorm Sigma ^+ 2 * mxdot theta theta ^+ 2)%:E,
      forall theta : 'rV[R]_N, 'E_mu[fun z => mxdot z theta] = 0,
      forall theta theta' : 'rV[R]_N,
        'E_mu[fun z => (mxdot z theta * mxdot z theta')%R] =
          (mxdot (theta *m Sigma) theta')%:E &
      forall T : 'M[R]_N, T \is symmetricmx ->
        'V_mu[fun z => mxdot z (z *m T)] <= (tau ^+ 2 * frobenius T ^+ 2)%:E].

Used by 12 declarations in 3 files

GaussianAnalysis.convex.gauss_feature: gauss_regular_feature
GaussianAnalysis.convex.barrier_lindeberg: ins_l_var, insertion_compare, loo_compare, hybrid_regular, int_Phi, int_Phi_set, barrier_lindeberg_mean, int_P4, barrier_lindeberg_variance
GaussianAnalysis.convex.feature_mixture: mixture_regular_feature_dot, mixture_regular_feature

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.