On this page

The largest eigenvalue of a real square matrix

GaussianAnalysis.matrix.lambda_maxlibrary/matrix/lambda_max.v220 lines16 lemmas and theorems, 1 definitionsource

Imports 3 library modules and 9 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

Imported by 2

lambda_max A is the supremum of the quadratic form mxdot x (A *m x) over the unit vectors x of 'cV[R]_n, in the conventions of opnorm (opnorm.v) and rayleigh_max (real_spectral.v): column vectors, the Frobenius inner product mxdot. For a symmetric matrix it is the largest eigenvalue. For n = 0 there is no unit vector and lambda_max A = 0, the supremum of the empty set (lambda_max_dim0).

The definition is alone in the section lambda_max, which is frozen with the statement of target T3 of phase 12 (AGENTS.md, section Phase 12; the sharp upper edge of the GOE): the source checker of scripts/ compares its code and the Require commands of this file with the acceptance commit fc76edf. The lemmas below it may grow. The file is a Rocq formalization of the largest eigenvalue lambda_max(W) of the credited argument of the proof of the proposition 'Good disorder' of 'Cutoff throughout the high-temperature Sherrington-Kirkpatrick phase' (family 227 of the OpenAI math collection, revision 1581d4cbd, appendices/entropy.tex). It follows no Lean module: the Lean modules of the collection write lambda_max(W) as the supremum of a Gaussian process over the unit ball and have no separate definition of the largest eigenvalue.

Proved:

lambda_max_ub, lambda_max_form: x^T A x <= lambda_max A for every unit x, and x^T A x <= lambda_max A x^T x for every x.
lambda_max_le: for n > 0, lambda_max A <= b as soon as x^T A x <= b for every unit x; lambda_max_attained: for n > 0, the supremum is attained at a unit vector (rayleigh_max).
lambda_max_eigenvector, eigenvalue_le_lambda_max: for n > 0 and A symmetric, lambda_max A is an eigenvalue of A; for every A, every eigenvalue of A with a unit eigenvector is at most lambda_max A.
lambda_max_opnorm, lambda_maxD: lambda_max A <= opnorm A, and lambda_max (A + B) <= lambda_max A + lambda_max B.
lambda_max_lipschitz, lambda_max_lipschitz_frobenius: `|lambda_max A - lambda_max B| <= opnorm (A - B) <= frobenius (A - B).
opnorm_lambda_max: for a symmetric A, opnorm A = Num.max (lambda_max A) (lambda_max (- A)).

lambda_max A the supremum of mxdot x (A *m x) over the columns x with mxdot x x = 1; the largest eigenvalue of a symmetric A

Main results

Results	Statement
lambda_maxlambda_max_ublambda_max_formlambda_max_lelambda_max_attained	`lambda_max A`, the supremum of `x^T A x` over the unit columns `x` of a square matrix (0 when `n = 0`). It bounds `x^T A x` for unit `x`, and `x^T A x <= lambda_max A x^T x` for all `x`; for `n > 0` it is the least such bound and is attained at a unit vector. The definition is alone in its section, frozen with the statement of target T3 of phase 12 (`applications/GoeEdgeStatement.v`, accepted at `fc76edf`).
lambda_max_eigenvectoreigenvalue_le_lambda_max	For `n > 0` and `A` symmetric, `lambda_max A` is an eigenvalue of `A` with a unit eigenvector. For every square `A`, every eigenvalue of `A` with a unit eigenvector is at most `lambda_max A`.
lambda_max_opnormlambda_maxDlambda_max_lipschitzlambda_max_lipschitz_frobeniusopnorm_lambda_max	`lambda_max A <= opnorm A`, `lambda_max (A + B) <= lambda_max A + lambda_max B`, and `\|lambda_max A - lambda_max B\| <= opnorm (A - B) <= frobenius (A - B)`, for all square matrices. For `A` symmetric, `opnorm A = max (lambda_max A, lambda_max (- A))`.

Declarations17 exported

sectionlambda_max

Variable R : realType.

definition lambda_max main result source, line 64

Type

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

Definition

Definition lambda_max n (A : 'M[R]_n) : R :=
  sup [set mxdot x (A *m x) | x in [set x : 'cV[R]_n | mxdot x x = 1]].

Main result, as the README states it

lambda_max A, the supremum of x^T A x over the unit columns x of a square matrix (0 when n = 0). It bounds x^T A x for unit x, and x^T A x <= lambda_max A x^T x for all x; for n > 0 it is the least such bound and is attained at a unit vector. The definition is alone in its section, frozen with the statement of target T3 of phase 12 (applications/GoeEdgeStatement.v, accepted at fc76edf).

Used by 25 declarations in 3 files

this file: lambda_max_dim0, lambda_max_ub, lambda_max_le, lambda_max_form, lambda_max_attained, lambda_max_eigenvector, eigenvalue_le_lambda_max, lambda_max_opnorm, lambda_maxD, lambda_max_lipschitz, lambda_max_lipschitz_frobenius, opnorm_lambda_max
GaussianAnalysis.random_matrix.goe_edge: lambda_max_net_le, goe_lambda_max_lipschitz, goe_lambda_maxN_lipschitz, measurable_goe_lambda_max, measurable_goe_lambda_maxN, integrable_goe_lambda_max, integrable_goe_lambda_maxN, goe_lambda_max_mean, goe_lambda_maxN_mean, goe_lambda_max_tail, goe_lambda_maxN_tail, goe_opnorm_edge_tail
GaussianApplications.GoeEdgeStatement: goe_edge_statement

sectionlambda_max_lemmas

Variable R : realType.
Implicit Types n : nat.

lemma mxdot_unit_dim source, line 73

forall [R : realType] [n : nat] [x : 'cV_n], mxdot x x = 1 -> (0 < n)%N

Statement as written in the source

Lemma mxdot_unit_dim n (x : 'cV[R]_n) : mxdot x x = 1 -> (0 < n)%N.

Used by 2 declarations in 1 file

this file: lambda_max_dim0, lambda_max_ub

lemma lambda_max_dim0 source, line 78

forall [R : realType] (A : 'M_0), lambda_max A = 0

Statement as written in the source

Lemma lambda_max_dim0 (A : 'M[R]_0) : lambda_max A = 0.

Used by 3 declarations in 1 file

this file: lambda_max_opnorm, lambda_maxD, opnorm_lambda_max

lemma lambda_max_set_neq0 source, line 85

forall [R : realType] [n : nat] (A : 'M_n),
(0 < n)%N -> [set mxdot x (A *m x) | x in [set x | mxdot x x = 1]] !=set0

Statement as written in the source

Lemma lambda_max_set_neq0 n (A : 'M[R]_n) : (0 < n)%N ->
  [set mxdot x (A *m x) | x in [set x : 'cV[R]_n | mxdot x x = 1]] !=set0.

Used by 2 declarations in 1 file

this file: lambda_max_has_sup, lambda_max_le

lemma lambda_max_ubound source, line 93

forall [R : realType] [n : nat] [A : 'M_n],
ubound [set mxdot x (A *m x) | x in [set x | mxdot x x = 1]] (opnorm A)

Statement as written in the source

Lemma lambda_max_ubound n (A : 'M[R]_n) :
  ubound [set mxdot x (A *m x) | x in [set x : 'cV[R]_n | mxdot x x = 1]]
    (opnorm A).

Used by 2 declarations in 1 file

this file: lambda_max_has_sup, lambda_max_opnorm

lemma lambda_max_has_sup source, line 102

forall [R : realType] [n : nat] (A : 'M_n),
(0 < n)%N -> has_sup [set mxdot x (A *m x) | x in [set x | mxdot x x = 1]]

Statement as written in the source

Lemma lambda_max_has_sup n (A : 'M[R]_n) : (0 < n)%N ->
  has_sup [set mxdot x (A *m x) | x in [set x : 'cV[R]_n | mxdot x x = 1]].

Used by 1 declaration in 1 file

this file: lambda_max_ub

lemma lambda_max_ub main result source, line 109

forall [R : realType] [n : nat] (A : 'M_n) [x : 'cV_n],
mxdot x x = 1 -> mxdot x (A *m x) <= lambda_max A

Main result

Stated in the README together with lambda_max.

Statement as written in the source

Lemma lambda_max_ub n (A : 'M[R]_n) (x : 'cV[R]_n) :
  mxdot x x = 1 -> mxdot x (A *m x) <= lambda_max A.

Used by 5 declarations in 1 file

this file: lambda_max_form, lambda_max_attained, eigenvalue_le_lambda_max, lambda_maxD, opnorm_lambda_max

lemma lambda_max_le main result source, line 116

forall [R : realType] [n : nat] [A : 'M_n] [b : R],
(0 < n)%N ->
(forall x : 'cV_n, mxdot x x = 1 -> mxdot x (A *m x) <= b) -> lambda_max A <= b

Main result

Stated in the README together with lambda_max.

Statement as written in the source

Lemma lambda_max_le n (A : 'M[R]_n) (b : R) : (0 < n)%N ->
  (forall x : 'cV[R]_n, mxdot x x = 1 -> mxdot x (A *m x) <= b) ->
  lambda_max A <= b.

Used by 3 declarations in 1 file

this file: lambda_max_attained, lambda_max_opnorm, lambda_maxD

lemma lambda_max_form main result source, line 124

forall [R : realType] [n : nat] (A : 'M_n) (x : 'cV_n),
mxdot x (A *m x) <= lambda_max A * mxdot x x

Main result

Stated in the README together with lambda_max.

Statement as written in the source

Lemma lambda_max_form n (A : 'M[R]_n) (x : 'cV[R]_n) :
  mxdot x (A *m x) <= lambda_max A * mxdot x x.

Used by 2 declarations in 1 file

this file: lambda_max_eigenvector, opnorm_lambda_max

lemma lambda_max_attained main result source, line 137

forall [R : realType] [n : nat] (A : 'M_n),
(0 < n)%N -> exists2 v : 'cV_n, mxdot v v = 1 & mxdot v (A *m v) = lambda_max A

Main result

Stated in the README together with lambda_max.

Statement as written in the source

Lemma lambda_max_attained n (A : 'M[R]_n) : (0 < n)%N ->
  exists2 v : 'cV[R]_n, mxdot v v = 1 & mxdot v (A *m v) = lambda_max A.

Used by 2 declarations in 2 files

this file: lambda_max_eigenvector
GaussianAnalysis.random_matrix.goe_edge: lambda_max_net_le

lemma lambda_max_eigenvector main result source, line 145

forall [R : realType] [n : nat] [A : 'M_n],
(0 < n)%N ->
A \is symmetricmx -> exists2 v : 'cV_n, mxdot v v = 1 & A *m v = lambda_max A *: v

Main result, as the README states it

For n > 0 and A symmetric, lambda_max A is an eigenvalue of A with a unit eigenvector. For every square A, every eigenvalue of A with a unit eigenvector is at most lambda_max A.

Statement as written in the source

Lemma lambda_max_eigenvector n (A : 'M[R]_n) : (0 < n)%N ->
  A \is symmetricmx ->
  exists2 v : 'cV[R]_n, mxdot v v = 1 & A *m v = lambda_max A *: v.

lemma eigenvalue_le_lambda_max main result source, line 163

forall [R : realType] [n : nat] [A : 'M_n] [v : 'cV_n] [mu : R],
mxdot v v = 1 -> A *m v = mu *: v -> mu <= lambda_max A

Main result

Stated in the README together with lambda_max_eigenvector.

Statement as written in the source

Lemma eigenvalue_le_lambda_max n (A : 'M[R]_n) (v : 'cV[R]_n) (mu : R) :
  mxdot v v = 1 -> A *m v = mu *: v -> mu <= lambda_max A.

lemma lambda_max_opnorm main result source, line 169

forall [R : realType] [n : nat] (A : 'M_n), lambda_max A <= opnorm A

Main result, as the README states it

lambda_max A <= opnorm A, lambda_max (A + B) <= lambda_max A + lambda_max B, and |lambda_max A - lambda_max B| <= opnorm (A - B) <= frobenius (A - B), for all square matrices. For A symmetric, opnorm A = max (lambda_max A, lambda_max (- A)).

Statement as written in the source

Lemma lambda_max_opnorm n (A : 'M[R]_n) : lambda_max A <= opnorm A.

Used by 2 declarations in 1 file

this file: lambda_max_lipschitz, opnorm_lambda_max

lemma lambda_maxD main result source, line 175

forall [R : realType] [n : nat] (A B : 'M_n),
lambda_max (A + B) <= lambda_max A + lambda_max B

Main result

Stated in the README together with lambda_max_opnorm.

Statement as written in the source

Lemma lambda_maxD n (A B : 'M[R]_n) :
  lambda_max (A + B) <= lambda_max A + lambda_max B.

Used by 1 declaration in 1 file

this file: lambda_max_lipschitz

lemma lambda_max_lipschitz main result source, line 183

forall [R : realType] [n : nat] (A B : 'M_n),
`|lambda_max A - lambda_max B| <= opnorm (A - B)

Main result

Stated in the README together with lambda_max_opnorm.

Statement as written in the source

Lemma lambda_max_lipschitz n (A B : 'M[R]_n) :
  `|lambda_max A - lambda_max B| <= opnorm (A - B).

Used by 2 declarations in 2 files

this file: lambda_max_lipschitz_frobenius
GaussianAnalysis.random_matrix.goe_edge: goe_lambda_max_lipschitz

lemma lambda_max_lipschitz_frobenius main result source, line 194

forall [R : realType] [n : nat] (A B : 'M_n),
`|lambda_max A - lambda_max B| <= frobenius (A - B)

Main result

Stated in the README together with lambda_max_opnorm.

Statement as written in the source

Lemma lambda_max_lipschitz_frobenius n (A B : 'M[R]_n) :
  `|lambda_max A - lambda_max B| <= frobenius (A - B).

lemma opnorm_lambda_max main result source, line 198

forall [R : realType] [n : nat] [A : 'M_n],
A \is symmetricmx -> opnorm A = Num.max (lambda_max A) (lambda_max (- A))

Main result

Stated in the README together with lambda_max_opnorm.

Statement as written in the source

Lemma opnorm_lambda_max n (A : 'M[R]_n) : A \is symmetricmx ->
  opnorm A = Num.max (lambda_max A) (lambda_max (- A)).

Used by 1 declaration in 1 file

GaussianAnalysis.random_matrix.goe_edge: goe_opnorm_edge_tail

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.