GaussianAnalysisRocq library documentation
Main resultsGlossary
On this page
GaussianAnalysismatrixreal_spectral

The spectral theorem for real symmetric matrices

GaussianAnalysis.matrix.real_spectrallibrary/matrix/real_spectral.v476 lines35 lemmas and theorems, 3 definitionssource
Imports 1 library modules and 14 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.analysis.topology_theory.topology, mathcomp.analysis.normedtype_theory.normedtype, mathcomp.analysis.derive, mathcomp.algebra.ring_tactic, mathcomp.algebra.field_tactic

Imported by 31
Required by 35 files of the paper proofs

Every real symmetric matrix A is orthogonally diagonalizable: A = P^T *m diag_mx d *m P with P orthogonal (symmetric_spectral). The proof is the analytic one and works over any realType: the quadratic form of A attains its maximum on the compact unit sphere, a maximizer is an eigenvector, and the Householder reflection that sends it to the first basis vector splits off one dimension. No complex number is used.

The Frobenius norm is compared with mx_norm, the norm of MathComp-Analysis on matrices (the largest absolute value of an entry): mx_norm A <= frobenius A <= sqrt (m n) mx_norm A (mx_norm_le_frobenius, frobenius_le_mx_norm). So the topology of 'M[R]_(m, n) is the topology of the Frobenius norm, and the unit sphere is compact (compact_unit_sphere).

householder wthe Householder reflection 1 - (2 / mxdot w w) *: (w *m w^T) of w : 'cV[R]_n, equal to 1 when w = 0
sym_spectralmx Aan orthogonal matrix P such that A = P^T *m diag_mx (sym_spectral_diag A) *m P when A is symmetric
sym_spectral_diag Athe eigenvalues of A, in the order of the rows of sym_spectralmx A

Main results

ResultsStatementUsed by theories/
symmetric_spectral
Spectral theorem: every real symmetric matrix is P^T diag(d) P with P orthogonal, over any realType. Proved by maximizing the quadratic form on the unit sphere and splitting off a dimension with a Householder reflection.Spectral/SymmetricDiagonalization
mx_norm_le_frobeniusfrobenius_le_mx_normcompact_unit_sphere
mx_norm A <= frobenius A <= sqrt (m n) mx_norm A, where mx_norm is the norm of MathComp-Analysis on matrices (the largest absolute value of an entry), so the Frobenius norm defines the topology of 'M[R]_(m, n); the unit sphere of 'rV[R]_n is compact.through symmetric_spectral
rayleigh_maxsymmetric_eigenvector
The quadratic form attains its maximum on the unit sphere; for a symmetric matrix a maximizer is an eigenvector.through symmetric_spectral
spectral_tracespectral_mxdotspectral_formspectral_form_lespectral_psdspectral_form_abs
If A = P^T diag(d) P with P orthogonal: the trace is the sum of the d_i, the squared Frobenius norm is the sum of the d_i^2, x^T A x = sum_i d_i (P x)_i^2, and x^T A x <= b x^T x for all x if and only if every d_i <= b (likewise for lower bounds, positive semidefiniteness and absolute values).Spectral/SymmetricDiagonalization, Spectral/Cutoff; spectral_form_le inside the library only
spectral_expmxtrace_ABAB_le
If A = P^T diag(d) P with P orthogonal, then A^k = P^T diag(d^k) P. For symmetric A, B: tr(ABAB) <= tr(A^2 B^2).Feature/DiagonalTrace; spectral_exp inside the library only

Declarations38 exported

lemma, theoremdefinitioninstancelocal
sectionsymmetricmx
Variable R : fieldType.
lemma symmetricmxP source, line 47 
forall [R : fieldType] [n : nat] (A : 'M_n), reflect (A^T = A) (A \is symmetricmx)
Statement as written in the source
Lemma symmetricmxP n (A : 'M[R]_n) : reflect (A^T = A) (A \is symmetricmx).
Used by 86 declarations in 27 files
lemma symmetricmx_conj source, line 52 
forall [R : fieldType] [m n : nat] [A : 'M_n] (P : 'M_(m, n)),
A \is symmetricmx -> P *m A *m P^T \is symmetricmx
Statement as written in the source
Lemma symmetricmx_conj m n (A : 'M[R]_n) (P : 'M[R]_(m, n)) :
  A \is symmetricmx -> P *m A *m P^T \is symmetricmx.
Used by 7 declarations in 5 files
sectiontrace_inequality
Variable R : realFieldType.
lemma mxtrace_ABAB_le main result source, line 64 
forall [R : realFieldType] [n : nat] [A B : 'M_n],
A \is symmetricmx -> B \is symmetricmx -> \tr (A *m B *m A *m B) <= \tr (A *m A *m B *m B)
Main result

Stated in the README together with spectral_exp.

Statement as written in the source
Lemma mxtrace_ABAB_le n (A B : 'M[R]_n) :
  A \is symmetricmx -> B \is symmetricmx ->
  \tr (A *m B *m A *m B) <= \tr (A *m A *m B *m B).
sectiontopology
Variable R : realType.
Implicit Types m n : nat.
lemma entry_le_mx_norm source, line 88 
forall [R : realType] [m n : nat] (A : 'M_(m, n)) (i : 'I_m) (j : 'I_n),
`|A i j| <= mx_norm A
Statement as written in the source
Lemma entry_le_mx_norm m n (A : 'M[R]_(m, n)) i j : `|A i j| <= mx_norm A.
Used by 1 declaration in 1 file
lemma mx_norm_le_frobenius main result source, line 91 
forall [R : realType] [m n : nat] (A : 'M_(m, n)), mx_norm A <= frobenius A
Main result, as the README states it

mx_norm A <= frobenius A <= sqrt (m n) mx_norm A, where mx_norm is the norm of MathComp-Analysis on matrices (the largest absolute value of an entry), so the Frobenius norm defines the topology of 'M[R]_(m, n); the unit sphere of 'rV[R]_n is compact.

Used in theories/ by: through symmetric_spectral
Statement as written in the source
Lemma mx_norm_le_frobenius m n (A : 'M[R]_(m, n)) : mx_norm A <= frobenius A.
Used by 3 declarations in 3 files
lemma frobenius_le_mx_norm main result source, line 97 
forall [R : realType] [m n : nat] (A : 'M_(m, n)),
frobenius A <= Num.ExtraDef.sqrtr (m * n)%:R * mx_norm A
Main result

Stated in the README together with mx_norm_le_frobenius.

Statement as written in the source
Lemma frobenius_le_mx_norm m n (A : 'M[R]_(m, n)) :
  frobenius A <= Num.sqrt (m * n)%:R * mx_norm A.
Used by 2 declarations in 2 files
lemma continuous_form source, line 109 
forall [R : realType] [n : nat] [A : 'M_n],
continuous (fun w : 'rV_n => (w *m A *m w^T) 0 0)
Statement as written in the source
Lemma continuous_form n (A : 'M[R]_n) :
  continuous (fun w : 'rV[R]_n => (w *m A *m w^T) 0 0).
Used by 4 declarations in 3 files
lemma continuous_mxdot source, line 127 
forall [R : realType] [n : nat], continuous (fun w : 'rV_n => mxdot w w)
Statement as written in the source
Lemma continuous_mxdot n : continuous (fun w : 'rV[R]_n => mxdot w w).
Used by 1 declaration in 1 file
lemma compact_unit_sphere main result source, line 134 
forall [R : realType] [n : nat], compact [set w | mxdot w w = 1]
Main result

Stated in the README together with mx_norm_le_frobenius.

Statement as written in the source
Lemma compact_unit_sphere n : compact [set w : 'rV[R]_n | mxdot w w = 1].
Used by 1 declaration in 1 file
sectionhouseholder
Variable R : realFieldType.
Implicit Types n : nat.
definition householder source, line 152
Type
forall [R : realFieldType] [n : nat], 'cV_n -> 'M_n
Definition
Definition householder n (w : 'cV[R]_n) : 'M[R]_n :=
  1%:M - (2 / mxdot w w) *: (w *m w^T).
Used by 10 declarations in 3 files
lemma householder0 source, line 155 
forall (R : realFieldType) (n : nat), householder (0 : 'cV_n) = 1%:M
Statement as written in the source
Lemma householder0 n : householder (0 : 'cV[R]_n) = 1%:M.
Used by 2 declarations in 1 file
lemma householder_tr source, line 158 
forall [R : realFieldType] [n : nat] (w : 'cV_n), (householder w)^T = householder w
Statement as written in the source
Lemma householder_tr n (w : 'cV[R]_n) : (householder w)^T = householder w.
Used by 5 declarations in 3 files
lemma householder_sym source, line 161 
forall [R : realFieldType] [n : nat] (w : 'cV_n), householder w \is symmetricmx
Statement as written in the source
Lemma householder_sym n (w : 'cV[R]_n) : householder w \is symmetricmx.
lemma householderK source, line 164 
forall [R : realFieldType] [n : nat] (w : 'cV_n), householder w *m householder w = 1%:M
Statement as written in the source
Lemma householderK n (w : 'cV[R]_n) : householder w *m householder w = 1%:M.
Used by 2 declarations in 1 file
lemma householder_orthogonal source, line 179 
forall [R : realFieldType] [n : nat] (w : 'cV_n), householder w \is orthogonalmx
Statement as written in the source
Lemma householder_orthogonal n (w : 'cV[R]_n) : householder w \is orthogonalmx.
Used by 3 declarations in 3 files
lemma householder_swap source, line 182 
forall [R : realFieldType] [n : nat] [u v : 'cV_n],
mxdot u u = mxdot v v -> householder (u - v) *m u = v
Statement as written in the source
Lemma householder_swap n (u v : 'cV[R]_n) :
  mxdot u u = mxdot v v -> householder (u - v) *m u = v.
Used by 3 declarations in 3 files
sectionspectral
Variable R : realType.
Implicit Types n : nat.
lemma householderN source, line 202 
forall [R : realType] [n : nat] (w : 'cV_n), householder (- w) = householder w
Statement as written in the source
Lemma householderN n (w : 'cV[R]_n) : householder (- w) = householder w.
Used by 1 declaration in 1 file
lemma mxdot_mulmx_sym source, line 207 
forall [R : realType] [n : nat] [M : 'M_n] (x y : 'cV_n),
M \is symmetricmx -> mxdot (M *m x) y = mxdot x (M *m y)
Statement as written in the source
Lemma mxdot_mulmx_sym n (M : 'M[R]_n) (x y : 'cV[R]_n) :
  M \is symmetricmx -> mxdot (M *m x) y = mxdot x (M *m y).
Used by 2 declarations in 2 files
lemma psd_form_eq0 source, line 212 
forall [R : realType] [n : nat] [M : 'M_n] [v : 'cV_n],
M \is symmetricmx ->
(forall x : 'cV_n, 0 <= mxdot x (M *m x)) -> mxdot v (M *m v) = 0 -> M *m v = 0

A nonnegative symmetric form vanishes at v only if M v = 0.

Statement as written in the source
Lemma psd_form_eq0 n (M : 'M[R]_n) (v : 'cV[R]_n) :
  M \is symmetricmx -> (forall x : 'cV[R]_n, 0 <= mxdot x (M *m x)) ->
  mxdot v (M *m v) = 0 -> M *m v = 0.
Used by 2 declarations in 2 files
lemma rayleigh_max main result source, line 236 
forall [R : realType] [n : nat] (A : 'M_n.+1),
exists2 v : 'cV_n.+1,
  mxdot v v = 1 & forall x : 'cV_n.+1, mxdot x (A *m x) <= mxdot v (A *m v) * mxdot x x
Main result, as the README states it

The quadratic form attains its maximum on the unit sphere; for a symmetric matrix a maximizer is an eigenvector.

Used in theories/ by: through symmetric_spectral
Statement as written in the source
Lemma rayleigh_max n (A : 'M[R]_n.+1) :
  exists2 v : 'cV[R]_n.+1, mxdot v v = 1 &
    forall x : 'cV[R]_n.+1, mxdot x (A *m x) <= mxdot v (A *m v) * mxdot x x.
Used by 2 declarations in 2 files
lemma symmetric_eigenvector main result source, line 260 
forall [R : realType] [n : nat] [A : 'M_n.+1],
A \is symmetricmx -> exists2 v : 'cV_n.+1, mxdot v v = 1 & A *m v = mxdot v (A *m v) *: v
Main result

Stated in the README together with rayleigh_max.

Statement as written in the source
Lemma symmetric_eigenvector n (A : 'M[R]_n.+1) : A \is symmetricmx ->
  exists2 v : 'cV[R]_n.+1, mxdot v v = 1 & A *m v = mxdot v (A *m v) *: v.
Used by 1 declaration in 1 file
lemma symmetric_block_of_eigen source, line 277 
forall [R : realType] [k : nat] [M : 'M_(1 + k)] [l : R],
M \is symmetricmx ->
M *m col_mx 1%:M 0 = l *: col_mx 1%:M 0 ->
M = block_mx l%:M 0 0 (drsubmx M) /\ drsubmx M \is symmetricmx
Statement as written in the source
Lemma symmetric_block_of_eigen k (M : 'M[R]_(1 + k)) (l : R) :
  M \is symmetricmx -> M *m col_mx 1%:M 0 = l *: col_mx 1%:M 0 ->
  M = block_mx l%:M 0 0 (drsubmx M) /\ drsubmx M \is symmetricmx.
Used by 1 declaration in 1 file
lemma symmetric_spectral main result source, line 295 
forall [R : realType] [n : nat] [A : 'M_n],
A \is symmetricmx ->
exists2 P : 'M_n, P \is orthogonalmx & exists d : 'rV_n, A = P^T *m diag_mx d *m P
Main result, as the README states it

Spectral theorem: every real symmetric matrix is P^T diag(d) P with P orthogonal, over any realType. Proved by maximizing the quadratic form on the unit sphere and splitting off a dimension with a Householder reflection.

Used in theories/ by: Spectral/SymmetricDiagonalization
Statement as written in the source
Lemma symmetric_spectral n (A : 'M[R]_n) : A \is symmetricmx ->
  exists2 P : 'M[R]_n, P \is orthogonalmx &
    exists d : 'rV[R]_n, A = P^T *m diag_mx d *m P.
Used by 17 declarations in 11 files
sectionspectral_consequences
Variable R : realType.
Implicit Types n : nat.
lemma spectral_eigenvector source, line 341 
forall [R : realType] [n : nat] [A P : 'M_n] [d : 'rV_n] (i : 'I_n),
P \is orthogonalmx -> A = P^T *m diag_mx d *m P -> A *m (row i P)^T = d 0 i *: (row i P)^T
Statement as written in the source
Lemma spectral_eigenvector n (A P : 'M[R]_n) (d : 'rV[R]_n) i :
  P \is orthogonalmx -> A = P^T *m diag_mx d *m P ->
  A *m (row i P)^T = d 0 i *: (row i P)^T.
Used by 6 declarations in 5 files
lemma orthogonalmx_row_unit source, line 354 
forall [R : realType] [n : nat] [P : 'M_n] (i : 'I_n),
P \is orthogonalmx -> mxdot (row i P)^T (row i P)^T = 1
Statement as written in the source
Lemma orthogonalmx_row_unit n (P : 'M[R]_n) i :
  P \is orthogonalmx -> mxdot (row i P)^T (row i P)^T = 1.
Used by 6 declarations in 5 files
lemma spectral_trace main result source, line 362 
forall [R : realType] [n : nat] [A P : 'M_n] [d : 'rV_n],
P \is orthogonalmx -> A = P^T *m diag_mx d *m P -> \tr A = \sum_i d 0 i
Main result, as the README states it

If A = P^T diag(d) P with P orthogonal: the trace is the sum of the d_i, the squared Frobenius norm is the sum of the d_i^2, x^T A x = sum_i d_i (P x)_i^2, and x^T A x <= b x^T x for all x if and only if every d_i <= b (likewise for lower bounds, positive semidefiniteness and absolute values).

Used in theories/ by: Spectral/SymmetricDiagonalization, Spectral/Cutoff; spectral_form_le inside the library only
Statement as written in the source
Lemma spectral_trace n (A P : 'M[R]_n) (d : 'rV[R]_n) :
  P \is orthogonalmx -> A = P^T *m diag_mx d *m P -> \tr A = \sum_i d 0 i.
Used by 9 declarations in 8 files
lemma spectral_mxdot main result source, line 369 
forall [R : realType] [n : nat] [A P : 'M_n] [d : 'rV_n],
P \is orthogonalmx -> A = P^T *m diag_mx d *m P -> mxdot A A = \sum_i d 0 i ^+ 2
Main result

Stated in the README together with spectral_trace.

Statement as written in the source
Lemma spectral_mxdot n (A P : 'M[R]_n) (d : 'rV[R]_n) :
  P \is orthogonalmx -> A = P^T *m diag_mx d *m P ->
  mxdot A A = \sum_i d 0 i ^+ 2.
Used by 4 declarations in 4 files
lemma spectral_form main result source, line 378 
forall [R : realType] [n : nat] [A P : 'M_n] [d : 'rV_n] (x : 'cV_n),
A = P^T *m diag_mx d *m P -> mxdot x (A *m x) = \sum_i d 0 i * (P *m x) i 0 ^+ 2
Main result

Stated in the README together with spectral_trace.

Statement as written in the source
Lemma spectral_form n (A P : 'M[R]_n) (d : 'rV[R]_n) (x : 'cV[R]_n) :
  A = P^T *m diag_mx d *m P ->
  mxdot x (A *m x) = \sum_i d 0 i * (P *m x) i 0 ^+ 2.
Used by 4 declarations in 3 files
lemma spectral_form_le main result source, line 386 
forall [R : realType] [n : nat] [A P : 'M_n] [d : 'rV_n] (b : R),
P \is orthogonalmx ->
A = P^T *m diag_mx d *m P ->
(forall x : 'cV_n, mxdot x (A *m x) <= b * mxdot x x) <-> (forall i : 'I_n, d 0 i <= b)
Main result

Stated in the README together with spectral_trace.

Statement as written in the source
Lemma spectral_form_le n (A P : 'M[R]_n) (d : 'rV[R]_n) (b : R) :
  P \is orthogonalmx -> A = P^T *m diag_mx d *m P ->
  (forall x : 'cV[R]_n, mxdot x (A *m x) <= b * mxdot x x) <->
  (forall i, d 0 i <= b).
Used by 8 declarations in 5 files
lemma spectral_form_ge source, line 398 
forall [R : realType] [n : nat] [A P : 'M_n] [d : 'rV_n] (b : R),
P \is orthogonalmx ->
A = P^T *m diag_mx d *m P ->
(forall x : 'cV_n, b * mxdot x x <= mxdot x (A *m x)) <-> (forall i : 'I_n, b <= d 0 i)
Statement as written in the source
Lemma spectral_form_ge n (A P : 'M[R]_n) (d : 'rV[R]_n) (b : R) :
  P \is orthogonalmx -> A = P^T *m diag_mx d *m P ->
  (forall x : 'cV[R]_n, b * mxdot x x <= mxdot x (A *m x)) <->
  (forall i, b <= d 0 i).
Used by 9 declarations in 5 files
lemma spectral_psd main result source, line 410 
forall [R : realType] [n : nat] [A P : 'M_n] [d : 'rV_n],
P \is orthogonalmx ->
A = P^T *m diag_mx d *m P ->
(forall x : 'cV_n, 0 <= mxdot x (A *m x)) <-> (forall i : 'I_n, 0 <= d 0 i)
Main result

Stated in the README together with spectral_trace.

Statement as written in the source
Lemma spectral_psd n (A P : 'M[R]_n) (d : 'rV[R]_n) :
  P \is orthogonalmx -> A = P^T *m diag_mx d *m P ->
  (forall x : 'cV[R]_n, 0 <= mxdot x (A *m x)) <-> (forall i, 0 <= d 0 i).
Used by 9 declarations in 7 files
lemma spectral_form_abs main result source, line 418 
forall [R : realType] [n : nat] [A P : 'M_n] [d : 'rV_n] (b : R),
P \is orthogonalmx ->
A = P^T *m diag_mx d *m P ->
(forall x : 'cV_n, `|mxdot x (A *m x)| <= b * mxdot x x) <->
(forall i : 'I_n, `|d 0 i| <= b)
Main result

Stated in the README together with spectral_trace.

Statement as written in the source
Lemma spectral_form_abs n (A P : 'M[R]_n) (d : 'rV[R]_n) (b : R) :
  P \is orthogonalmx -> A = P^T *m diag_mx d *m P ->
  (forall x : 'cV[R]_n, `|mxdot x (A *m x)| <= b * mxdot x x) <->
  (forall i, `|d 0 i| <= b).
Used by 3 declarations in 1 file
lemma spectral_exp main result source, line 436 
forall [R : realType] [n : nat] [A P : 'M_n] [d : 'rV_n] (k : nat),
P \is orthogonalmx ->
A = P^T *m diag_mx d *m P -> A ^+ k = P^T *m diag_mx (\row_i d 0 i ^+ k) *m P
Main result, as the README states it

If A = P^T diag(d) P with P orthogonal, then A^k = P^T diag(d^k) P. For symmetric A, B: tr(ABAB) <= tr(A^2 B^2).

Used in theories/ by: Feature/DiagonalTrace; spectral_exp inside the library only
Statement as written in the source
Lemma spectral_exp n (A P : 'M[R]_n) (d : 'rV[R]_n) k :
  P \is orthogonalmx -> A = P^T *m diag_mx d *m P ->
  A ^+ k = P^T *m diag_mx (\row_i d 0 i ^+ k) *m P.
Used by 5 declarations in 3 files

A chosen orthogonal diagonalization.

lemma ex_sym_spectral source, line 450 
forall [R : realType] [n : nat] (A : 'M_n),
exists Pd : 'M_n * 'rV_n,
  (Pd.1 \is orthogonalmx) &&
  ((A \is symmetricmx) ==> (A == (Pd.1)^T *m diag_mx Pd.2 *m Pd.1))
Statement as written in the source
Lemma ex_sym_spectral n (A : 'M[R]_n) : exists Pd : 'M[R]_n * 'rV[R]_n,
  (Pd.1 \is orthogonalmx) &&
  ((A \is symmetricmx) ==> (A == Pd.1^T *m diag_mx Pd.2 *m Pd.1)).
Used by 4 declarations in 1 file
definition sym_spectralmx source, line 460
Type
forall [R : realType] [n : nat], 'M_n -> 'M_n
Definition
Definition sym_spectralmx n (A : 'M[R]_n) : 'M[R]_n :=
  (xchoose (ex_sym_spectral A)).1.
Used by 16 declarations in 6 files
definition sym_spectral_diag source, line 462
Type
forall [R : realType] [n : nat], 'M_n -> 'rV_n
Definition
Definition sym_spectral_diag n (A : 'M[R]_n) : 'rV[R]_n :=
  (xchoose (ex_sym_spectral A)).2.
Used by 21 declarations in 6 files
lemma sym_spectralmx_orthogonal source, line 465 
forall [R : realType] [n : nat] (A : 'M_n), sym_spectralmx A \is orthogonalmx
Statement as written in the source
Lemma sym_spectralmx_orthogonal n (A : 'M[R]_n) :
  sym_spectralmx A \is orthogonalmx.
Used by 14 declarations in 5 files
lemma sym_spectralE source, line 469 
forall [R : realType] [n : nat] [A : 'M_n],
A \is symmetricmx ->
A = (sym_spectralmx A)^T *m diag_mx (sym_spectral_diag A) *m sym_spectralmx A
Statement as written in the source
Lemma sym_spectralE n (A : 'M[R]_n) : A \is symmetricmx ->
  A = (sym_spectralmx A)^T *m diag_mx (sym_spectral_diag A) *m sym_spectralmx A.
Used by 11 declarations in 5 files
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.