On this page

Gaussian features are regular

GaussianAnalysis.convex.gauss_featurelibrary/convex/gauss_feature.v522 lines8 lemmas and theoremssource

Imports 12 library modules and 22 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.exp, 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

Required by 1 files of the paper proofs

extension/Features/Regular.v

(2.10) of Koehler and Sohn (arXiv 2608.27372): the centered Gaussian law with covariance S^T S, the law of x S for x of law gauss k, is a (3^(1/4), sqrt 2 opnorm (S^T S))-regular feature (regular_feature of least_squares.v) when S != 0. The moments needed are those of the quadratic forms of a standard Gaussian vector.

gauss_quad_moments: for A symmetric and x of law gauss k, E x A x^T = tr A and E (x A x^T)^2 = (tr A)^2 + 2 |A|_F^2, by the spectral theorem and the invariance of gauss k under orthogonal maps.
gauss_mxdot_moments: E <x, a> = 0, E <x, a> <x, b> = <a, b> and E <x, a>^4 = 3 |a|^4.
gauss_regular_feature: (2.10), for a law nu given by its values, nu A = gauss k [set x | A (x S)].

Main results

Results	Statement
gauss_quad_momentsgauss_mxdot_momentsgauss_coord_moments	For `x` of law `gauss k` and `A` symmetric, `E x A x^T = tr A` and `E (x A x^T)^2 = (tr A)^2 + 2 \|A\|_F^2` (spectral theorem and orthogonal invariance of `gauss k`); `E <x, a> = 0`, `E <x, a> <x, b> = <a, b>` and `E <x, a>^4 = 3 \|a\|^4`.
gauss_regular_featureopnorm_sqr_le	(2.10) of Koehler and Sohn: for `S != 0` and a law `nu` on `'rV[R]_N` with `nu A = gauss k [set x \| A (x S)]`, `nu` is a `(3^(1/4), sqrt 2 opnorm (S^T S))`-regular feature with covariance `S^T S`; `opnorm S ^ 2 <= opnorm (S^T S)`.

Declarations8 exported

sectiongauss_quadratic

Context {R : realType}.
Local Notation N := (@normal_prob R 0 1).

lemma mxdot_self_le_norm source, line 45

forall {R : realType} [k : nat] (x : 'rV_k), mxdot x x <= k%:R * `|x| ^+ 2

Statement as written in the source

Lemma mxdot_self_le_norm k (x : 'rV[R]_k) : mxdot x x <= k%:R * `|x| ^+ 2.

Used by 1 declaration in 1 file

this file: gauss_integrable4

lemma gauss_integrable4 source, line 56

forall {R : realType} [k : nat] [g : 'rV_k -> R] [a b : R],
measurable_fun [set: 'rV_k] g ->
(forall x : 'rV_k, `|g x| <= a + b * mxdot x x ^+ 2) ->
(gauss k).-integrable [set: 'rV_k] (EFin \o g)

Domination by a + b |x|^4.

Statement as written in the source

Lemma gauss_integrable4 k (g : 'rV[R]_k -> R) (a b : R) :
  measurable_fun setT g -> (forall x, `|g x| <= a + b * mxdot x x ^+ 2) ->
  (gauss k).-integrable setT (EFin \o g).

Used by 4 declarations in 1 file

this file: gauss_diag_moments, gauss_quad_moments, gauss_mxdot_moments, gauss_regular_feature

lemma gauss_coord_moments main result source, line 84

forall {R : realType} [k : nat] (j l : 'I_k),
\int[gauss k]_y (y 0 j ^+ 2 * y 0 l ^+ 2) = (if j == l then 3 else 1 : R)

Main result

Stated in the README together with gauss_quad_moments.

Statement as written in the source

Lemma gauss_coord_moments k (j l : 'I_k) :
  \int[gauss k]_y (y 0 j ^+ 2 * y 0 l ^+ 2) = (if j == l then 3 else 1 : R).

Used by 1 declaration in 1 file

this file: gauss_diag_moments

lemma gauss_diag_moments source, line 123

forall {R : realType} [k : nat] (d : 'rV_k),
\int[gauss k]_y \sum_j d 0 j * y 0 j ^+ 2 = \sum_j d 0 j /\
\int[gauss k]_y (\sum_j d 0 j * y 0 j ^+ 2) ^+ 2 =
(\sum_j d 0 j) ^+ 2 + 2 * \sum_j d 0 j ^+ 2

Statement as written in the source

Lemma gauss_diag_moments k (d : 'rV[R]_k) :
  \int[gauss k]_y (\sum_j d 0 j * y 0 j ^+ 2) = \sum_j d 0 j /\
  \int[gauss k]_y (\sum_j d 0 j * y 0 j ^+ 2) ^+ 2 =
    (\sum_j d 0 j) ^+ 2 + 2 * \sum_j d 0 j ^+ 2.

Used by 1 declaration in 1 file

this file: gauss_quad_moments

lemma gauss_quad_moments main result source, line 175

forall {R : realType} [k : nat] [A : 'M_k],
A \is symmetricmx ->
\int[gauss k]_x mxdot x (x *m A) = \tr A /\
\int[gauss k]_x mxdot x (x *m A) ^+ 2 = \tr A ^+ 2 + 2 * mxdot A A

Main result, as the README states it

For x of law gauss k and A symmetric, E x A x^T = tr A and E (x A x^T)^2 = (tr A)^2 + 2 |A|_F^2 (spectral theorem and orthogonal invariance of gauss k); E <x, a> = 0, E <x, a> <x, b> = <a, b> and E <x, a>^4 = 3 |a|^4.

Statement as written in the source

Lemma gauss_quad_moments k (A : 'M[R]_k) : A \is symmetricmx ->
  \int[gauss k]_x mxdot x (x *m A) = \tr A /\
  \int[gauss k]_x mxdot x (x *m A) ^+ 2 = \tr A ^+ 2 + 2 * mxdot A A.

Used by 2 declarations in 1 file

this file: gauss_mxdot_moments, gauss_regular_feature

lemma gauss_mxdot_moments main result source, line 235

forall {R : realType} [k : nat] (a b : 'rV_k),
[/\ \int[gauss k]_x mxdot x a = 0, \int[gauss k]_x (mxdot x a * mxdot x b) = mxdot a b
  & \int[gauss k]_x mxdot x a ^+ 4 = 3 * mxdot a a ^+ 2]

Main result

Stated in the README together with gauss_quad_moments.

Statement as written in the source

Lemma gauss_mxdot_moments k (a b : 'rV[R]_k) :
  [/\ \int[gauss k]_x mxdot x a = 0,
      \int[gauss k]_x (mxdot x a * mxdot x b) = mxdot a b &
      \int[gauss k]_x mxdot x a ^+ 4 = 3 * mxdot a a ^+ 2].

Used by 1 declaration in 1 file

this file: gauss_regular_feature

sectionopnorm_gram

Context {R : realType}.

lemma opnorm_sqr_le main result source, line 292

forall {R : realType} [m n : nat] (S0 : 'M_(m, n)), opnorm S0 ^+ 2 <= opnorm (S0^T *m S0)

Main result

Stated in the README together with gauss_regular_feature.

Statement as written in the source

Lemma opnorm_sqr_le m n (S : 'M[R]_(m, n)) : opnorm S ^+ 2 <= opnorm (S^T *m S).

Used by 1 declaration in 1 file

this file: gauss_regular_feature

sectiongauss_regular

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

theorem gauss_regular_feature main result source, line 316

forall {R : realType} {N : nat} [k : nat] [S0 : 'M_(k, N)] [nu : probability 'rV_N R],
(forall A : set 'rV_N,
 (measure_matrix_display default_measure_display).-measurable A ->
 nu A = gauss k (mulmx^~ S0 @^-1` A)) ->
S0 != 0 ->
regular_feature (3 `^ (1 / 4)) (Num.ExtraDef.sqrtr 2 * opnorm (S0^T *m S0)) (S0^T *m S0) nu

(2.10): a Gaussian feature is regular.

Main result, as the README states it

(2.10) of Koehler and Sohn: for S != 0 and a law nu on 'rV[R]_N with nu A = gauss k [set x | A (x S)], nu is a (3^(1/4), sqrt 2 opnorm (S^T S))-regular feature with covariance S^T S; opnorm S ^ 2 <= opnorm (S^T S).

Statement as written in the source

Theorem gauss_regular_feature k (S : 'M[R]_(k, N))
    (nu : probability 'rV[R]_N R) :
  (forall A, measurable A -> nu A = gauss k ((fun x => x *m S) @^-1` A)) ->
  S != 0 ->
  regular_feature (3 `^ (1 / 4)) (Num.sqrt 2 * opnorm (S^T *m S))
    (S^T *m S) nu.

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.