On this page

Whitening

GaussianAnalysis.matrix.whiteninglibrary/matrix/whitening.v113 lines4 lemmas and theorems, 1 definitionsource

Imports 2 library modules and 10 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.reals.reals, mathcomp.algebra.ring_tactic

Imported by 1

GaussianAnalysis.fourier.small_ball

Let S be a real symmetric matrix whose quadratic form is bounded below: b |x|^2 <= x S x^T for every row vector x, with b > 0. If S = P^T diag (d) P is its spectral decomposition, the matrix W = diag (d)^(-1/2) P whitens S: W S W^T = 1 (whitening_mxP), and |x W| <= |x| / sqrt b for every row vector x (frobenius_whitening_mx). For b = 1, W does not increase norms (whitening_exists).

whitening_mx S diag_mx (\row_i (Num.sqrt (d 0 i))^-1) *m P for the chosen spectral decomposition S = P^T diag_mx d P (sym_spectralmx, sym_spectral_diag)

Main results

Results	Statement
whitening_mxwhitening_mxPfrobenius_whitening_mxsym_spectral_diag_ge	Whitening: if `S` is symmetric and `b \|x\|^2 <= x S x^T` for all row vectors `x`, with `b > 0`, then the eigenvalues of `S` are at least `b`, and `W = diag(d)^(-1/2) P`, for the spectral decomposition `S = P^T diag(d) P`, satisfies `W S W^T = 1` and `\|x W\| <= \|x\| / sqrt b`.
whitening_exists	The case `b = 1`: a symmetric `S` with `\|x\|^2 <= x S x^T` has a `W` with `W S W^T = 1` and `\|x W\| <= \|x\|` for all `x`.

Declarations5 exported

sectionwhitening_matrix

Variable R : realType.
Implicit Types n : nat.

definition whitening_mx main result source, line 35

Type

forall [R : realType] [n : nat], 'M_n -> 'M_n

Definition

Definition whitening_mx n (S : 'M[R]_n) : 'M[R]_n :=
  diag_mx (\row_i (Num.sqrt (sym_spectral_diag S 0 i))^-1) *m sym_spectralmx S.

Main result, as the README states it

Whitening: if S is symmetric and b |x|^2 <= x S x^T for all row vectors x, with b > 0, then the eigenvalues of S are at least b, and W = diag(d)^(-1/2) P, for the spectral decomposition S = P^T diag(d) P, satisfies W S W^T = 1 and |x W| <= |x| / sqrt b.

Used by 3 declarations in 1 file

this file: whitening_mxP, frobenius_whitening_mx, whitening_exists

lemma sym_spectral_diag_ge main result source, line 39

forall [R : realType] [n : nat] [S0 : 'M_n] [b : R],
S0 \is symmetricmx ->
(forall x : 'rV_n, b * mxdot x x <= mxdot (x *m S0) x) ->
forall i : 'I_n, b <= sym_spectral_diag S0 0 i

A lower bound on the quadratic form bounds the eigenvalues below.

Main result

Stated in the README together with whitening_mx.

Statement as written in the source

Lemma sym_spectral_diag_ge n (S : 'M[R]_n) (b : R) : S \is symmetricmx ->
  (forall x : 'rV[R]_n, b * mxdot x x <= mxdot (x *m S) x) ->
  forall i, b <= sym_spectral_diag S 0 i.

Used by 2 declarations in 1 file

this file: whitening_mxP, frobenius_whitening_mx

lemma whitening_mxP main result source, line 52

forall [R : realType] [n : nat] [S0 : 'M_n] [b : R],
0 < b ->
S0 \is symmetricmx ->
(forall x : 'rV_n, b * mxdot x x <= mxdot (x *m S0) x) ->
whitening_mx S0 *m S0 *m (whitening_mx S0)^T = 1%:M

Main result

Stated in the README together with whitening_mx.

Statement as written in the source

Lemma whitening_mxP n (S : 'M[R]_n) (b : R) : 0 < b -> S \is symmetricmx ->
  (forall x : 'rV[R]_n, b * mxdot x x <= mxdot (x *m S) x) ->
  whitening_mx S *m S *m (whitening_mx S)^T = 1%:M.

Used by 1 declaration in 1 file

this file: whitening_exists

lemma frobenius_whitening_mx main result source, line 74

forall [R : realType] [n : nat] [S0 : 'M_n] [b : R],
0 < b ->
S0 \is symmetricmx ->
(forall x : 'rV_n, b * mxdot x x <= mxdot (x *m S0) x) ->
forall x : 'rV_n,
frobenius (x *m whitening_mx S0) <= (Num.ExtraDef.sqrtr b)^-1 * frobenius x

Main result

Stated in the README together with whitening_mx.

Statement as written in the source

Lemma frobenius_whitening_mx n (S : 'M[R]_n) (b : R) :
    0 < b -> S \is symmetricmx ->
  (forall x : 'rV[R]_n, b * mxdot x x <= mxdot (x *m S) x) ->
  forall x : 'rV[R]_n,
    frobenius (x *m whitening_mx S) <= (Num.sqrt b)^-1 * frobenius x.

Used by 1 declaration in 1 file

this file: whitening_exists

theorem whitening_exists main result source, line 99

forall [R : realType] [n : nat] [S0 : 'M_n],
S0 \is symmetricmx ->
(forall x : 'rV_n, mxdot x x <= mxdot (x *m S0) x) ->
exists W : 'M_n,
  W *m S0 *m W^T = 1%:M /\ (forall x : 'rV_n, frobenius (x *m W) <= frobenius x)

The whitening of a matrix that dominates the identity.

Main result, as the README states it

The case b = 1: a symmetric S with |x|^2 <= x S x^T has a W with W S W^T = 1 and |x W| <= |x| for all x.

Statement as written in the source

Theorem whitening_exists n (S : 'M[R]_n) : S \is symmetricmx ->
  (forall x : 'rV[R]_n, mxdot x x <= mxdot (x *m S) x) ->
  exists W : 'M[R]_n,
    W *m S *m W^T = 1%:M /\
    forall x : 'rV[R]_n, frobenius (x *m W) <= frobenius x.

Used by 2 declarations in 1 file

GaussianAnalysis.fourier.small_ball: vector_small_ball, vector_small_ball_variance

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.