On this page

Moments of regular features

GaussianAnalysis.convex.feature_momentslibrary/convex/feature_moments.v544 lines42 lemmas and theoremssource

Imports 6 library modules and 21 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.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 4

Required by 3 files of the paper proofs

The moment calculus behind Propositions 2.14 and 2.16 of Koehler and Sohn (arXiv 2608.27372): for a (K, tau)-regular feature mu on 'rV[R]_N with covariance Sigma (regular_feature of least_squares.v) and lambda = opnorm Sigma, the polynomials of degree at most 4 in the coordinates are integrable, and the first two moments of the linear forms and of the quadratic forms z |-> z T z^T depend only on Sigma. Integrals are Rintegral, with values in R.

reg_integrable: a measurable g with |g z| <= a + b |z|^4 is integrable.
reg_mean, reg_cov: E <z, theta> = 0 and E <z, theta> <z, theta'> = theta Sigma theta'^T.
reg_quad_mean: E z T z^T = sum_b (e_b Sigma) . T_(., b), a function of Sigma and T only; reg_quad_var: for T symmetric, E (z T z^T - E z T z^T)^2 <= tau^2 |T|_F^2.
reg_resid2: E (b - <z, theta>)^2 = b^2 + theta Sigma theta^T; reg_resid4: E (b - <z, theta>)^4 <= 8 (1 + K^4) S^2 with S = lambda |theta|^2 + b^2.
reg_ell_mean, reg_ell_var: for l z = c - 2 <v, z> + z T z^T with T symmetric, E l z = c + E z T z^T and E (l z - E l)^2 <= 2 tau^2 |T|_F^2 + 8 lambda |v|^2.
form_le_opnorm: v Sigma v^T <= opnorm Sigma |v|^2.

Main results

Results	Statement
reg_integrablereg_meanreg_covreg_quad_meanreg_quad_var	For a `(K, tau)`-regular feature `mu` with covariance `Sigma` (Koehler-Sohn, Definition 2.5): every measurable `g` with `\|g z\| <= a + b \|z\|^4` is integrable, `E <z, theta> = 0`, `E <z, theta> <z, theta'> = theta Sigma theta'^T`, `E z T z^T` depends only on `Sigma` and `T`, and `E (z T z^T - E z T z^T)^2 <= tau^2 \|T\|_F^2` for `T` symmetric.
reg_resid2reg_resid4reg_ell_meanreg_ell_varform_le_opnorm	`E (b - <z, theta>)^2 = b^2 + theta Sigma theta^T`, `E (b - <z, theta>)^4 <= 8 (1 + K^4) (lambda \|theta\|^2 + b^2)^2` with `lambda = opnorm Sigma`, and for `l z = c - 2 <z, v> + z T z^T` with `T` symmetric, `E l = c + E z T z^T` and `E (l - E l)^2 <= 2 tau^2 \|T\|_F^2 + 8 lambda \|v\|^2`; `v Sigma v^T <= opnorm Sigma \|v\|^2`.

Declarations42 exported

sectionRintegral_helpers

Context d (U : measurableType d) (R : realType) (P : probability U R).

lemma Rintegral_EFin source, line 50

forall [d : measure_display] [U : measurableType d] [R : realType] 
  [P : probability U R] [f : U -> R],
P.-integrable [set: U] (EFin \o f) -> (\int[P]_x f x)%:E = (\int[P]_x (f x)%:E)%E

Statement as written in the source

Lemma Rintegral_EFin (f : U -> R) :
  P.-integrable setT (EFin \o f) -> (\int[P]_x f x)%:E = (\int[P]_x (f x)%:E)%E.

Used by 8 declarations in 5 files

this file: reg_moment4, reg_quad_var
GaussianAnalysis.convex.gauss_feature: gauss_regular_feature
GaussianAnalysis.convex.barrier_lindeberg: lindeberg_telescope, loo_variance, barrier_lindeberg_variance
GaussianAnalysis.convex.ridge_comparison: markov_lt
GaussianAnalysis.convex.feature_mixture: quad_expectation

lemma integrable_cst_prob source, line 54

forall [d : measure_display] [U : measurableType d] [R : realType] 
  (P : probability U R) (c : R),
P.-integrable [set: U] (EFin \o cst c)

Statement as written in the source

Lemma integrable_cst_prob (c : R) : P.-integrable setT (EFin \o cst c).

Used by 15 declarations in 5 files

this file: reg_integrable, reg_resid2, reg_resid4, reg_ell_int, reg_ell_mean
GaussianAnalysis.convex.gauss_feature: gauss_regular_feature
GaussianAnalysis.convex.barrier_lindeberg: insertion_compare, loo_compare, int_Phi, int_Phi_set, barrier_lindeberg_mean, barrier_lindeberg_variance
GaussianAnalysis.convex.ridge_comparison: ref_objective_int, ref_objective_mean
GaussianAnalysis.convex.feature_mixture: moment4_integrable

lemma Rintegral_cst_prob source, line 57

forall [d : measure_display] [U : measurableType d] [R : realType] 
  (P : probability U R) (c : R),
\int[P]__ c = c

Statement as written in the source

Lemma Rintegral_cst_prob (c : R) : \int[P]_x c = c.

Used by 10 declarations in 4 files

this file: Rintegral_sumr, reg_resid2, reg_resid4, reg_ell_mean
GaussianAnalysis.convex.gauss_feature: gauss_regular_feature
GaussianAnalysis.convex.barrier_lindeberg: insertion_compare, loo_compare, barrier_lindeberg_mean, barrier_lindeberg_variance
GaussianAnalysis.convex.ridge_comparison: ref_objective_mean

lemma integrableR_sum source, line 60

forall [d : measure_display] [U : measurableType d] [R : realType] 
  [P : probability U R] [I : Type] (s : seq I) [h : I -> U -> R],
(forall i : I, P.-integrable [set: U] (EFin \o h i)) ->
P.-integrable [set: U] (EFin \o (fun x : U => \sum_(i <- s) h i x))

Statement as written in the source

Lemma integrableR_sum I (s : seq I) (h : I -> U -> R) :
  (forall i, P.-integrable setT (EFin \o h i)) ->
  P.-integrable setT (EFin \o (fun x => \sum_(i <- s) h i x)).

Used by 8 declarations in 4 files

this file: Rintegral_sumr
GaussianAnalysis.convex.gauss_feature: gauss_diag_moments, gauss_quad_moments
GaussianAnalysis.convex.barrier_lindeberg: int_Phi, barrier_lindeberg_mean, int_P4
GaussianAnalysis.convex.ridge_comparison: ref_objective_int, ref_objective_mean

lemma Rintegral_sumr source, line 70

forall [d : measure_display] [U : measurableType d] [R : realType] 
  [P : probability U R] [I : Type] (s : seq I) [h : I -> U -> R],
(forall i : I, P.-integrable [set: U] (EFin \o h i)) ->
\int[P]_x \sum_(i <- s) h i x = \sum_(i <- s) \int[P]_x h i x

Statement as written in the source

Lemma Rintegral_sumr I (s : seq I) (h : I -> U -> R) :
  (forall i, P.-integrable setT (EFin \o h i)) ->
  \int[P]_x (\sum_(i <- s) h i x) = \sum_(i <- s) \int[P]_x h i x.

Used by 7 declarations in 5 files

this file: reg_quad_mean
GaussianAnalysis.convex.gauss_feature: gauss_diag_moments, gauss_mxdot_moments
GaussianAnalysis.convex.barrier_lindeberg: barrier_lindeberg_mean, int_P4
GaussianAnalysis.convex.ridge_comparison: ref_objective_mean
GaussianAnalysis.convex.feature_mixture: quad_expectation

lemma integrableRD source, line 81

forall [d : measure_display] [U : measurableType d] [R : realType] 
  [P : probability U R] [f g : U -> R],
P.-integrable [set: U] (EFin \o f) ->
P.-integrable [set: U] (EFin \o g) ->
P.-integrable [set: U] (EFin \o (fun x : U => f x + g x))

Statement as written in the source

Lemma integrableRD (f g : U -> R) :
  P.-integrable setT (EFin \o f) -> P.-integrable setT (EFin \o g) ->
  P.-integrable setT (EFin \o (fun x => f x + g x)).

Used by 6 declarations in 2 files

GaussianAnalysis.convex.barrier_lindeberg: insertion_compare, int_Phi, int_Phi_set, barrier_lindeberg_mean, barrier_lindeberg_variance
GaussianAnalysis.convex.ridge_comparison: ref_objective_int

lemma integrableRB source, line 89

forall [d : measure_display] [U : measurableType d] [R : realType] 
  [P : probability U R] [f g : U -> R],
P.-integrable [set: U] (EFin \o f) ->
P.-integrable [set: U] (EFin \o g) ->
P.-integrable [set: U] (EFin \o (fun x : U => f x - g x))

Statement as written in the source

Lemma integrableRB (f g : U -> R) :
  P.-integrable setT (EFin \o f) -> P.-integrable setT (EFin \o g) ->
  P.-integrable setT (EFin \o (fun x => f x - g x)).

Used by 2 declarations in 2 files

GaussianAnalysis.convex.gauss_feature: gauss_regular_feature
GaussianAnalysis.convex.barrier_lindeberg: insertion_compare

lemma integrableRZl source, line 97

forall [d : measure_display] [U : measurableType d] [R : realType] 
  [P : probability U R] (c : R) [f : U -> R],
P.-integrable [set: U] (EFin \o f) ->
P.-integrable [set: U] (EFin \o (fun x : U => c * f x))

Statement as written in the source

Lemma integrableRZl (c : R) (f : U -> R) :
  P.-integrable setT (EFin \o f) ->
  P.-integrable setT (EFin \o (fun x => c * f x)).

Used by 12 declarations in 4 files

this file: integrableRZr
GaussianAnalysis.convex.gauss_feature: gauss_diag_moments, gauss_quad_moments, gauss_mxdot_moments, gauss_regular_feature
GaussianAnalysis.convex.barrier_lindeberg: insertion_compare, int_Phi, int_Phi_set, barrier_lindeberg_mean, barrier_lindeberg_variance
GaussianAnalysis.convex.ridge_comparison: ref_objective_int, ref_objective_mean

lemma integrableRZr source, line 106

forall [d : measure_display] [U : measurableType d] [R : realType] 
  [P : probability U R] (c : R) [f : U -> R],
P.-integrable [set: U] (EFin \o f) ->
P.-integrable [set: U] (EFin \o (fun x : U => f x * c))

Statement as written in the source

Lemma integrableRZr (c : R) (f : U -> R) :
  P.-integrable setT (EFin \o f) ->
  P.-integrable setT (EFin \o (fun x => f x * c)).

Used by 4 declarations in 1 file

GaussianAnalysis.convex.barrier_lindeberg: insertion_compare, loo_compare, loo_variance, barrier_lindeberg_variance

sectionlinear_forms

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

lemma continuous_mxdotl source, line 119

forall {R : realType} {N : nat} [th : 'rV_N], continuous ((mxdot (n:=N))^~ th)

Statement as written in the source

Lemma continuous_mxdotl (th : 'rV[R]_N) :
  continuous (fun z : 'rV[R]_N => mxdot z th).

Used by 2 declarations in 2 files

this file: measurable_mxdotl
GaussianAnalysis.convex.barrier_lindeberg: measurable_mxdot_tnth

lemma measurable_mxdotl source, line 130

forall {R : realType} {N : nat} (th : 'rV_N),
measurable_fun [set: 'rV_N]
  ((mxdot (n:=N))^~ th)

Statement as written in the source

Lemma measurable_mxdotl (th : 'rV[R]_N) :
  measurable_fun setT (fun z : 'rV[R]_N => mxdot z th).

Used by 16 declarations in 5 files

this file: measurable_quad, reg_int4, reg_int_sqr, reg_int_lin, reg_int_lin2, reg_int_resid2, reg_int_ell2, reg_int_resid4
GaussianAnalysis.convex.gauss_feature: gauss_regular_feature
GaussianAnalysis.convex.barrier_lindeberg: barrier_lindeberg_mean, int_P4
GaussianAnalysis.convex.ridge_comparison: ref_objective_mean
GaussianAnalysis.convex.feature_mixture: moment4_int4, moment4_int_lin, moment4_int_lin2, mixture_regular_feature_dot

lemma mxdot_quadE source, line 135

forall {R : realType} {N : nat} (T : 'M_N) (z : 'rV_N),
mxdot z (z *m T) = \sum_b mxdot z 'e_b * mxdot z (col b T)^T

A quadratic form is a sum of products of two linear forms.

Statement as written in the source

Lemma mxdot_quadE (T : 'M[R]_N) (z : 'rV[R]_N) :
  mxdot z (z *m T) = \sum_b mxdot z (delta_mx 0 b) * mxdot z (col b T)^T.

Used by 3 declarations in 2 files

this file: measurable_quad, reg_quad_mean
GaussianAnalysis.convex.feature_mixture: quad_expectation

lemma measurable_quad source, line 143

forall {R : realType} {N : nat} (T : 'M_N),
measurable_fun [set: 'rV_N]
  (fun z : 'rV_N => mxdot z (z *m T))

Statement as written in the source

Lemma measurable_quad (T : 'M[R]_N) :
  measurable_fun setT (fun z : 'rV[R]_N => mxdot z (z *m T)).

Used by 8 declarations in 3 files

this file: measurable_norm2, reg_int_quad, reg_int_quad2, reg_int_ell2
GaussianAnalysis.convex.gauss_feature: gauss_mxdot_moments, gauss_regular_feature
GaussianAnalysis.convex.feature_mixture: moment4_int_quad, moment4_Lfun2_quad

lemma measurable_norm2 source, line 152

forall {R : realType} {N : nat},
measurable_fun [set: 'rV_N]
  (fun z : 'rV_N => mxdot z z)

Statement as written in the source

Lemma measurable_norm2 : measurable_fun setT (fun z : 'rV[R]_N => mxdot z z).

Used by 2 declarations in 2 files

this file: reg_int_norm4
GaussianAnalysis.convex.feature_mixture: moment4_int_norm4

lemma mxdot_sqr_sum source, line 160

forall {R : realType} {N : nat} (z : 'rV_N),
mxdot z z ^+ 2 <= N%:R * \sum_a mxdot z 'e_a ^+ 4

Statement as written in the source

Lemma mxdot_sqr_sum (z : 'rV[R]_N) :
  mxdot z z ^+ 2 <= N%:R * \sum_a mxdot z (delta_mx 0 a) ^+ 4.

Used by 2 declarations in 2 files

this file: reg_int_norm4
GaussianAnalysis.convex.feature_mixture: moment4_int_norm4

lemma quad_le_frobenius source, line 173

forall {R : realType} {N : nat} (T : 'M_N) (z : 'rV_N),
`|mxdot z (z *m T)| <= frobenius T * mxdot z z

Statement as written in the source

Lemma quad_le_frobenius (T : 'M[R]_N) (z : 'rV[R]_N) :
  `|mxdot z (z *m T)| <= frobenius T * mxdot z z.

Used by 5 declarations in 3 files

this file: reg_int_quad, quad_sqr_le
GaussianAnalysis.convex.gauss_feature: gauss_mxdot_moments, gauss_regular_feature
GaussianAnalysis.convex.feature_mixture: moment4_int_quad

lemma form_le_opnorm main result source, line 181

forall {R : realType} {N : nat} (Sigma : 'M_N) (v : 'rV_N),
mxdot (v *m Sigma) v <= opnorm Sigma * mxdot v v

Main result

Stated in the README together with reg_resid2.

Statement as written in the source

Lemma form_le_opnorm (Sigma : 'M[R]_N) (v : 'rV[R]_N) :
  mxdot (v *m Sigma) v <= opnorm Sigma * mxdot v v.

Used by 2 declarations in 2 files

this file: reg_ell_var
GaussianAnalysis.convex.gauss_feature: gauss_regular_feature

sectionregular_moments

Context {R : realType} {N : nat}.
Variables (K tau : R) (Sigma : 'M[R]_N) (mu : probability 'rV[R]_N R).
Hypothesis reg : regular_feature K tau Sigma mu.
Local Notation lambda := (opnorm Sigma).

lemma reg_lambda_gt0 source, line 200

forall {R : realType} {N : nat} [K tau : R] [Sigma : 'M_N] [mu : probability 'rV_N R],
regular_feature K tau Sigma mu -> 0 < opnorm Sigma

Statement as written in the source

Lemma reg_lambda_gt0 : 0 < lambda.

Used by 7 declarations in 2 files

this file: reg_resid4
GaussianAnalysis.convex.barrier_lindeberg: ins_l_var, insertion_compare, loo_compare, barrier_lindeberg_mean, loo_variance, ref_moment_bound

lemma reg_int4 source, line 203

forall {R : realType} {N : nat} [K tau : R] [Sigma : 'M_N] [mu : probability 'rV_N R],
regular_feature K tau Sigma mu ->
forall th : 'rV_N, mu.-integrable [set: 'rV_N] (EFin \o (fun z : 'rV_N => mxdot z th ^+ 4))

Statement as written in the source

Lemma reg_int4 (th : 'rV[R]_N) :
  mu.-integrable setT (EFin \o (fun z => mxdot z th ^+ 4)).

Used by 5 declarations in 2 files

this file: reg_moment4, reg_int_norm4, reg_resid4
GaussianAnalysis.convex.barrier_lindeberg: barrier_lindeberg_mean, int_P4

lemma reg_moment4 source, line 215

forall {R : realType} {N : nat} [K tau : R] [Sigma : 'M_N] [mu : probability 'rV_N R],
regular_feature K tau Sigma mu ->
forall th : 'rV_N,
\int[mu]_z mxdot z th ^+ 4 <= K ^+ 4 * opnorm Sigma ^+ 2 * mxdot th th ^+ 2

Statement as written in the source

Lemma reg_moment4 (th : 'rV[R]_N) :
  \int[mu]_z (mxdot z th ^+ 4) <= K ^+ 4 * lambda ^+ 2 * mxdot th th ^+ 2.

Used by 3 declarations in 2 files

this file: reg_resid4
GaussianAnalysis.convex.barrier_lindeberg: barrier_lindeberg_mean, int_P4

lemma reg_int_norm4 source, line 223

forall {R : realType} {N : nat} [K tau : R] [Sigma : 'M_N] [mu : probability 'rV_N R],
regular_feature K tau Sigma mu ->
mu.-integrable [set: 'rV_N] (EFin \o (fun z : 'rV_N => mxdot z z ^+ 2))

Statement as written in the source

Lemma reg_int_norm4 : mu.-integrable setT (EFin \o (fun z => mxdot z z ^+ 2)).

Used by 1 declaration in 1 file

this file: reg_integrable

lemma reg_integrable main result source, line 237

forall {R : realType} {N : nat} [K tau : R] [Sigma : 'M_N] [mu : probability 'rV_N R],
regular_feature K tau Sigma mu ->
forall [g : 'rV_N -> R] [a b : R],
measurable_fun [set: 'rV_N] g ->
(forall z : 'rV_N, `|g z| <= a + b * mxdot z z ^+ 2) ->
mu.-integrable [set: 'rV_N] (EFin \o g)

Domination by a + b |z|^4.

Main result, as the README states it

For a (K, tau)-regular feature mu with covariance Sigma (Koehler-Sohn, Definition 2.5): every measurable g with |g z| <= a + b |z|^4 is integrable, E <z, theta> = 0, E <z, theta> <z, theta'> = theta Sigma theta'^T, E z T z^T depends only on Sigma and T, and E (z T z^T - E z T z^T)^2 <= tau^2 |T|_F^2 for T symmetric.

Statement as written in the source

Lemma reg_integrable (g : 'rV[R]_N -> R) (a b : R) :
  measurable_fun setT g -> (forall z, `|g z| <= a + b * mxdot z z ^+ 2) ->
  mu.-integrable setT (EFin \o g).

Used by 8 declarations in 1 file

this file: reg_int_sqr, reg_int_lin, reg_int_lin2, reg_int_quad, reg_int_quad2, reg_int_resid2, reg_int_ell2, reg_int_resid4

lemma le1_sqr source, line 250

forall {R : realType} [x : R], 0 <= x -> x <= 1 + x ^+ 2

Statement as written in the source

Lemma le1_sqr (x : R) : 0 <= x -> x <= 1 + x ^+ 2.

Used by 13 declarations in 3 files

this file: reg_int_sqr, reg_int_lin, reg_int_lin2, reg_int_quad, reg_int_resid2, reg_int_ell2
GaussianAnalysis.convex.gauss_feature: gauss_diag_moments, gauss_quad_moments, gauss_mxdot_moments, gauss_regular_feature
GaussianAnalysis.convex.feature_mixture: moment4_int_lin, moment4_int_lin2, moment4_int_quad

lemma reg_int_sqr source, line 253

forall {R : realType} {N : nat} [K tau : R] [Sigma : 'M_N] [mu : probability 'rV_N R],
regular_feature K tau Sigma mu ->
forall th : 'rV_N, mu.-integrable [set: 'rV_N] (EFin \o (fun z : 'rV_N => mxdot z th ^+ 2))

Statement as written in the source

Lemma reg_int_sqr (th : 'rV[R]_N) :
  mu.-integrable setT (EFin \o (fun z => mxdot z th ^+ 2)).

Used by 5 declarations in 3 files

this file: reg_ell_var
GaussianAnalysis.convex.barrier_lindeberg: int_Phi, int_Phi_set
GaussianAnalysis.convex.ridge_comparison: ref_objective_int, ref_objective_mean

lemma reg_int_lin source, line 264

forall {R : realType} {N : nat} [K tau : R] [Sigma : 'M_N] [mu : probability 'rV_N R],
regular_feature K tau Sigma mu ->
forall th : 'rV_N, mu.-integrable [set: 'rV_N] (EFin \o (mxdot (n:=N))^~ th)

Statement as written in the source

Lemma reg_int_lin (th : 'rV[R]_N) :
  mu.-integrable setT (EFin \o (fun z => mxdot z th)).

Used by 3 declarations in 1 file

this file: reg_resid2, reg_ell_int, reg_ell_mean

lemma reg_int_lin2 source, line 276

forall {R : realType} {N : nat} [K tau : R] [Sigma : 'M_N] [mu : probability 'rV_N R],
regular_feature K tau Sigma mu ->
forall th th' : 'rV_N,
mu.-integrable [set: 'rV_N] (EFin \o (fun z : 'rV_N => mxdot z th * mxdot z th'))

Statement as written in the source

Lemma reg_int_lin2 (th th' : 'rV[R]_N) :
  mu.-integrable setT (EFin \o (fun z => mxdot z th * mxdot z th')).

Used by 2 declarations in 1 file

this file: reg_quad_mean, reg_resid2

lemma reg_int_quad source, line 293

forall {R : realType} {N : nat} [K tau : R] [Sigma : 'M_N] [mu : probability 'rV_N R],
regular_feature K tau Sigma mu ->
forall T : 'M_N, mu.-integrable [set: 'rV_N] (EFin \o (fun z : 'rV_N => mxdot z (z *m T)))

Statement as written in the source

Lemma reg_int_quad (T : 'M[R]_N) :
  mu.-integrable setT (EFin \o (fun z => mxdot z (z *m T))).

Used by 2 declarations in 1 file

this file: reg_ell_int, reg_ell_mean

lemma quad_sqr_le source, line 303

forall {R : realType} {N : nat} (T : 'M_N) (z : 'rV_N),
mxdot z (z *m T) ^+ 2 <= frobenius T ^+ 2 * mxdot z z ^+ 2

Statement as written in the source

Lemma quad_sqr_le (T : 'M[R]_N) (z : 'rV[R]_N) :
  mxdot z (z *m T) ^+ 2 <= frobenius T ^+ 2 * mxdot z z ^+ 2.

Used by 4 declarations in 3 files

this file: reg_int_quad2, reg_int_ell2
GaussianAnalysis.convex.gauss_feature: gauss_regular_feature
GaussianAnalysis.convex.feature_mixture: moment4_Lfun2_quad

lemma reg_int_quad2 source, line 311

forall {R : realType} {N : nat} [K tau : R] [Sigma : 'M_N] [mu : probability 'rV_N R],
regular_feature K tau Sigma mu ->
forall (T : 'M_N) (c : R),
mu.-integrable [set: 'rV_N] (EFin \o (fun z : 'rV_N => (mxdot z (z *m T) - c) ^+ 2))

Statement as written in the source

Lemma reg_int_quad2 (T : 'M[R]_N) (c : R) :
  mu.-integrable setT (EFin \o (fun z => (mxdot z (z *m T) - c) ^+ 2)).

Used by 2 declarations in 1 file

this file: reg_quad_var, reg_ell_var

lemma reg_int_resid2 source, line 322

forall {R : realType} {N : nat} [K tau : R] [Sigma : 'M_N] [mu : probability 'rV_N R],
regular_feature K tau Sigma mu ->
forall (th : 'rV_N) (b : R),
mu.-integrable [set: 'rV_N] (EFin \o (fun z : 'rV_N => (b - mxdot z th) ^+ 2))

Statement as written in the source

Lemma reg_int_resid2 (th : 'rV[R]_N) (b : R) :
  mu.-integrable setT (EFin \o (fun z => (b - mxdot z th) ^+ 2)).

Used by 2 declarations in 1 file

GaussianAnalysis.convex.barrier_lindeberg: insertion_compare, loo_compare

lemma reg_int_ell2 source, line 335

forall {R : realType} {N : nat} [K tau : R] [Sigma : 'M_N] [mu : probability 'rV_N R],
regular_feature K tau Sigma mu ->
forall (c : R) (v : 'rV_N) (T : 'M_N) (d : R),
mu.-integrable [set: 'rV_N]
  (EFin \o (fun z : 'rV_N => (c - 2 * mxdot z v + mxdot z (z *m T) - d) ^+ 2))

Statement as written in the source

Lemma reg_int_ell2 (c : R) (v : 'rV[R]_N) (T : 'M[R]_N) (d : R) :
  mu.-integrable setT
    (EFin \o (fun z => (c - 2 * mxdot z v + mxdot z (z *m T) - d) ^+ 2)).

Used by 2 declarations in 2 files

this file: reg_ell_var
GaussianAnalysis.convex.barrier_lindeberg: insertion_compare

lemma reg_mean main result source, line 360

forall {R : realType} {N : nat} [K tau : R] [Sigma : 'M_N] [mu : probability 'rV_N R],
regular_feature K tau Sigma mu -> forall th : 'rV_N, \int[mu]_z mxdot z th = 0

Main result

Stated in the README together with reg_integrable.

Statement as written in the source

Lemma reg_mean (th : 'rV[R]_N) : \int[mu]_z mxdot z th = 0.

Used by 2 declarations in 1 file

this file: reg_resid2, reg_ell_mean

lemma reg_cov main result source, line 366

forall {R : realType} {N : nat} [K tau : R] [Sigma : 'M_N] [mu : probability 'rV_N R],
regular_feature K tau Sigma mu ->
forall th th' : 'rV_N, \int[mu]_z (mxdot z th * mxdot z th') = mxdot (th *m Sigma) th'

Main result

Stated in the README together with reg_integrable.

Statement as written in the source

Lemma reg_cov (th th' : 'rV[R]_N) :
  \int[mu]_z (mxdot z th * mxdot z th') = mxdot (th *m Sigma) th'.

Used by 4 declarations in 2 files

this file: reg_quad_mean, reg_resid2, reg_ell_var
GaussianAnalysis.convex.ridge_comparison: ref_objective_mean

lemma reg_quad_mean main result source, line 373

forall {R : realType} {N : nat} [K tau : R] [Sigma : 'M_N] [mu : probability 'rV_N R],
regular_feature K tau Sigma mu ->
forall T : 'M_N, \int[mu]_z mxdot z (z *m T) = \sum_b mxdot ('e_b *m Sigma) (col b T)^T

Main result

Stated in the README together with reg_integrable.

Statement as written in the source

Lemma reg_quad_mean (T : 'M[R]_N) :
  \int[mu]_z mxdot z (z *m T) =
  \sum_b mxdot (delta_mx 0 b *m Sigma) (col b T)^T.

Used by 2 declarations in 1 file

this file: reg_ell_mean, reg_ell_var

lemma reg_quad_var main result source, line 382

forall {R : realType} {N : nat} [K tau : R] [Sigma : 'M_N] [mu : probability 'rV_N R],
regular_feature K tau Sigma mu ->
forall [T : 'M_N],
T \is symmetricmx ->
\int[mu]_z (mxdot z (z *m T) - \int[mu]_y mxdot y (y *m T)) ^+ 2 <=
tau ^+ 2 * frobenius T ^+ 2

Main result

Stated in the README together with reg_integrable.

Statement as written in the source

Lemma reg_quad_var (T : 'M[R]_N) : T \is symmetricmx ->
  \int[mu]_z ((mxdot z (z *m T) - \int[mu]_y mxdot y (y *m T)) ^+ 2) <=
  tau ^+ 2 * frobenius T ^+ 2.

Used by 1 declaration in 1 file

this file: reg_ell_var

lemma reg_resid2 main result source, line 391

forall {R : realType} {N : nat} [K tau : R] [Sigma : 'M_N] [mu : probability 'rV_N R],
regular_feature K tau Sigma mu ->
forall (th : 'rV_N) (b : R),
\int[mu]_z (b - mxdot z th) ^+ 2 = b ^+ 2 + mxdot (th *m Sigma) th

Main result, as the README states it

E (b - <z, theta>)^2 = b^2 + theta Sigma theta^T, E (b - <z, theta>)^4 <= 8 (1 + K^4) (lambda |theta|^2 + b^2)^2 with lambda = opnorm Sigma, and for l z = c - 2 <z, v> + z T z^T with T symmetric, E l = c + E z T z^T and E (l - E l)^2 <= 2 tau^2 |T|_F^2 + 8 lambda |v|^2; v Sigma v^T <= opnorm Sigma |v|^2.

Statement as written in the source

Lemma reg_resid2 (th : 'rV[R]_N) (b : R) :
  \int[mu]_z ((b - mxdot z th) ^+ 2) = b ^+ 2 + mxdot (th *m Sigma) th.

Used by 1 declaration in 1 file

GaussianAnalysis.convex.barrier_lindeberg: insertion_compare

lemma resid4_le source, line 412

forall {R : realType} (b y : R), (b - y) ^+ 4 <= 8 * b ^+ 4 + 8 * y ^+ 4

Statement as written in the source

Lemma resid4_le (b y : R) : (b - y) ^+ 4 <= 8 * b ^+ 4 + 8 * y ^+ 4.

Used by 2 declarations in 1 file

this file: reg_int_resid4, reg_resid4

lemma reg_int_resid4 source, line 429

forall {R : realType} {N : nat} [K tau : R] [Sigma : 'M_N] [mu : probability 'rV_N R],
regular_feature K tau Sigma mu ->
forall (th : 'rV_N) (b : R),
mu.-integrable [set: 'rV_N] (EFin \o (fun z : 'rV_N => (b - mxdot z th) ^+ 4))

Statement as written in the source

Lemma reg_int_resid4 (th : 'rV[R]_N) (b : R) :
  mu.-integrable setT (EFin \o (fun z => (b - mxdot z th) ^+ 4)).

Used by 3 declarations in 2 files

this file: reg_resid4
GaussianAnalysis.convex.barrier_lindeberg: insertion_compare, loo_variance

lemma reg_resid4 main result source, line 444

forall {R : realType} {N : nat} [K tau : R] [Sigma : 'M_N] [mu : probability 'rV_N R],
regular_feature K tau Sigma mu ->
forall (th : 'rV_N) (b : R),
\int[mu]_z (b - mxdot z th) ^+ 4 <=
8 * (1 + K ^+ 4) * (opnorm Sigma * mxdot th th + b ^+ 2) ^+ 2

Main result

Stated in the README together with reg_resid2.

Statement as written in the source

Lemma reg_resid4 (th : 'rV[R]_N) (b : R) :
  \int[mu]_z ((b - mxdot z th) ^+ 4) <=
  8 * (1 + K ^+ 4) * (lambda * mxdot th th + b ^+ 2) ^+ 2.

Used by 2 declarations in 1 file

GaussianAnalysis.convex.barrier_lindeberg: insertion_compare, loo_variance

lemma reg_ell_int source, line 481

forall {R : realType} {N : nat} [K tau : R] [Sigma : 'M_N] [mu : probability 'rV_N R],
regular_feature K tau Sigma mu ->
forall (c : R) (v : 'rV_N) (T : 'M_N),
mu.-integrable [set: 'rV_N]
  (EFin \o (fun z : 'rV_N => c - 2 * mxdot z v + mxdot z (z *m T)))

Statement as written in the source

Lemma reg_ell_int (c : R) (v : 'rV[R]_N) (T : 'M[R]_N) :
  mu.-integrable setT
    (EFin \o (fun z => c - 2 * mxdot z v + mxdot z (z *m T))).

lemma reg_ell_mean main result source, line 493

forall {R : realType} {N : nat} [K tau : R] [Sigma : 'M_N] [mu : probability 'rV_N R],
regular_feature K tau Sigma mu ->
forall (c : R) (v : 'rV_N) (T : 'M_N),
\int[mu]_z (c - 2 * mxdot z v + mxdot z (z *m T)) =
c + \sum_b mxdot ('e_b *m Sigma) (col b T)^T

Main result

Stated in the README together with reg_resid2.

Statement as written in the source

Lemma reg_ell_mean (c : R) (v : 'rV[R]_N) (T : 'M[R]_N) :
  \int[mu]_z (c - 2 * mxdot z v + mxdot z (z *m T)) =
  c + \sum_b mxdot (delta_mx 0 b *m Sigma) (col b T)^T.

Used by 2 declarations in 2 files

this file: reg_ell_var
GaussianAnalysis.convex.barrier_lindeberg: insertion_compare

lemma reg_ell_var main result source, line 510

forall {R : realType} {N : nat} [K tau : R] [Sigma : 'M_N] [mu : probability 'rV_N R],
regular_feature K tau Sigma mu ->
forall (c : R) (v : 'rV_N) [T : 'M_N],
T \is symmetricmx ->
\int[mu]_z
   (c - 2 * mxdot z v + mxdot z (z *m T) -
    \int[mu]_y (c - 2 * mxdot y v + mxdot y (y *m T)))
   ^+ 2 <=
2 * tau ^+ 2 * frobenius T ^+ 2 + 8 * opnorm Sigma * mxdot v v

Main result

Stated in the README together with reg_resid2.

Statement as written in the source

Lemma reg_ell_var (c : R) (v : 'rV[R]_N) (T : 'M[R]_N) : T \is symmetricmx ->
  \int[mu]_z ((c - 2 * mxdot z v + mxdot z (z *m T) -
     \int[mu]_y (c - 2 * mxdot y v + mxdot y (y *m T))) ^+ 2) <=
  2 * tau ^+ 2 * frobenius T ^+ 2 + 8 * lambda * mxdot v v.

Used by 1 declaration in 1 file

GaussianAnalysis.convex.barrier_lindeberg: ins_l_var

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.