GaussianAnalysisRocq library documentation
Main resultsGlossary
On this page
GaussianAnalysismatrixopnorm

The operator norm of real matrices

GaussianAnalysis.matrix.opnormlibrary/matrix/opnorm.v304 lines27 lemmas and theorems, 1 definitionsource
Imports 2 library modules and 11 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

Imported by 31
Required by 38 files of the paper proofs

The operator norm of A : 'M[R]_(m, n) is its norm as a linear map x |-> A *m x from 'cV[R]_n to 'cV[R]_m, both with the Euclidean norm frobenius. It is characterized by the inequality frobenius (A *m x) <= b * frobenius x (opnorm_leP) and by the bilinear inequality `|mxdot y (A *m x)| <= b * frobenius y * frobenius x (opnorm_bilinearP). For a symmetric matrix, it is the smallest b such that `|mxdot x (A *m x)| <= b * mxdot x x for every x (opnorm_symP), and the largest absolute value of an eigenvalue (opnorm_spectral). For a symmetric matrix and an even exponent p > 0, tr (A ^+ p) <= t ^+ p, or mxdot x (A ^+ p *m x) <= t ^+ p * mxdot x x for every x, gives opnorm A <= t (opnorm_le_trace_exp, opnorm_le_form_exp). The operator norm lies between the norm mx_norm of MathComp-Analysis and the Frobenius norm: mx_norm A <= opnorm A <= frobenius A (mx_norm_le_opnorm, opnorm_le_frobenius).

opnorm Athe operator norm of A, the supremum of frobenius (A *m x) over the columns x with frobenius x <= 1

Main results

ResultsStatementUsed by theories/
opnorm_lePopnorm_bilinearPopnormDopnorm_mulmxopnorm_trmx
The operator norm sup_{|x| <= 1} |A x| is the least b with |A x| <= b |x|, and the least b with |y^T A x| <= b |y| |x|. It is a submultiplicative norm, invariant under transposition and orthogonal multiplication, and lies between the entrywise norm mx_norm of MathComp-Analysis and the Frobenius norm (mx_norm_le_opnorm, opnorm_le_frobenius).Spectral/SymmetricDiagonalization, SquareFree/EdgeLower, SquareFree/WalkNBEvent, Head/TailSupport; opnorm_trmx inside the library only
opnorm_symPopnorm_spectral
For a symmetric matrix, opnorm A <= b if and only if |x^T A x| <= b x^T x for all x, and the operator norm is the largest absolute value of an eigenvalue.Feature/DiagonalTrace, SquareFree/EdgeUpper, SquareFree/EdgeLower, Spectral/OperatorTransport, Spectral/OrthogonalBounds, Head/TailSupport
opnorm_exp_le_trace_evenopnorm_le_trace_expopnorm_le_form_exp
For a symmetric matrix and an even exponent p > 0, opnorm A ^ p <= tr(A^p); so tr(A^p) <= t^p with t >= 0 gives opnorm A <= t, and so does x^T A^p x <= t^p x^T x for all x.Feature/DiagonalTrace, SquareFree/EdgeUpper, SquareFree/WalkNBEvent, SquareFree/EdgeLower

Declarations28 exported

lemma, theoremdefinitioninstancelocal
sectionopnorm
Variable R : realType.
Implicit Types m n p : nat.
definition opnorm source, line 43
Type
forall [R : realType] [m n : nat], 'M_(m, n) -> R
Definition
Definition opnorm m n (A : 'M[R]_(m, n)) : R :=
  sup [set frobenius (A *m x) | x in [set x : 'cV[R]_n | frobenius x <= 1]].
Used by 156 declarations in 28 files
lemma opnorm_has_sup source, line 46 
forall [R : realType] [m n : nat] (A : 'M_(m, n)),
has_sup [set frobenius (A *m x) | x in [set x | frobenius x <= 1]]
Statement as written in the source
Lemma opnorm_has_sup m n (A : 'M[R]_(m, n)) :
  has_sup [set frobenius (A *m x) | x in [set x : 'cV[R]_n | frobenius x <= 1]].
Used by 2 declarations in 1 file
lemma opnorm_ub source, line 56 
forall [R : realType] [m n : nat] (A : 'M_(m, n)) [x : 'cV_n],
frobenius x <= 1 -> frobenius (A *m x) <= opnorm A
Statement as written in the source
Lemma opnorm_ub m n (A : 'M[R]_(m, n)) (x : 'cV[R]_n) :
  frobenius x <= 1 -> frobenius (A *m x) <= opnorm A.
Used by 2 declarations in 1 file
lemma opnorm_le source, line 62 
forall [R : realType] [m n : nat] [A : 'M_(m, n)] [b : R],
(forall x : 'cV_n, frobenius x <= 1 -> frobenius (A *m x) <= b) -> opnorm A <= b
Statement as written in the source
Lemma opnorm_le m n (A : 'M[R]_(m, n)) (b : R) :
  (forall x : 'cV[R]_n, frobenius x <= 1 -> frobenius (A *m x) <= b) ->
  opnorm A <= b.
Used by 6 declarations in 4 files
lemma opnorm_ge0 source, line 70 
forall [R : realType] [m n : nat] (A : 'M_(m, n)), 0 <= opnorm A
Statement as written in the source
Lemma opnorm_ge0 m n (A : 'M[R]_(m, n)) : 0 <= opnorm A.
Used by 42 declarations in 14 files
lemma opnorm_le_frobenius source, line 76 
forall [R : realType] [m n : nat] (A : 'M_(m, n)), opnorm A <= frobenius A
Statement as written in the source
Lemma opnorm_le_frobenius m n (A : 'M[R]_(m, n)) : opnorm A <= frobenius A.
Used by 10 declarations in 10 files
lemma frobenius_mulmx_opnorm source, line 82 
forall [R : realType] [m n : nat] (A : 'M_(m, n)) (x : 'cV_n),
frobenius (A *m x) <= opnorm A * frobenius x
Statement as written in the source
Lemma frobenius_mulmx_opnorm m n (A : 'M[R]_(m, n)) (x : 'cV[R]_n) :
  frobenius (A *m x) <= opnorm A * frobenius x.
Used by 13 declarations in 7 files
lemma opnorm_leP main result source, line 94 
forall [R : realType] [m n : nat] (A : 'M_(m, n)) [b : R],
0 <= b -> (forall x : 'cV_n, frobenius (A *m x) <= b * frobenius x) <-> opnorm A <= b
Main result, as the README states it

The operator norm sup_{|x| <= 1} |A x| is the least b with |A x| <= b |x|, and the least b with |y^T A x| <= b |y| |x|. It is a submultiplicative norm, invariant under transposition and orthogonal multiplication, and lies between the entrywise norm mx_norm of MathComp-Analysis and the Frobenius norm (mx_norm_le_opnorm, opnorm_le_frobenius).

Used in theories/ by: Spectral/SymmetricDiagonalization, SquareFree/EdgeLower, SquareFree/WalkNBEvent, Head/TailSupport; opnorm_trmx inside the library only
Statement as written in the source
Lemma opnorm_leP m n (A : 'M[R]_(m, n)) (b : R) : 0 <= b ->
  (forall x : 'cV[R]_n, frobenius (A *m x) <= b * frobenius x) <->
  opnorm A <= b.
Used by 10 declarations in 5 files
lemma mxdot_col source, line 105 
forall [R : realType] [m n : nat] (A B : 'M_(m, n)),
mxdot A B = \sum_k mxdot (col k A) (col k B)
Statement as written in the source
Lemma mxdot_col m n (A B : 'M[R]_(m, n)) :
  mxdot A B = \sum_k mxdot (col k A) (col k B).
Used by 1 declaration in 1 file
lemma frobenius_mulmx_mx_opnorm source, line 112 
forall [R : realType] [m n p : nat] (A : 'M_(m, n)) (X : 'M_(n, p)),
frobenius (A *m X) <= opnorm A * frobenius X
Statement as written in the source
Lemma frobenius_mulmx_mx_opnorm m n p (A : 'M[R]_(m, n)) (X : 'M[R]_(n, p)) :
  frobenius (A *m X) <= opnorm A * frobenius X.
Used by 2 declarations in 2 files
lemma opnorm0 source, line 123 
forall (R : realType) (m n : nat), opnorm (0 : 'M_(m, n)) = 0
Statement as written in the source
Lemma opnorm0 m n : opnorm (0 : 'M[R]_(m, n)) = 0.
Used by 6 declarations in 4 files
lemma opnormZ source, line 129 
forall [R : realType] [m n : nat] (a : R) (A : 'M_(m, n)),
opnorm (a *: A) = `|a| * opnorm A
Statement as written in the source
Lemma opnormZ m n a (A : 'M[R]_(m, n)) : opnorm (a *: A) = `|a| * opnorm A.
Used by 8 declarations in 5 files
lemma opnormN source, line 142 
forall [R : realType] [m n : nat] (A : 'M_(m, n)), opnorm (- A) = opnorm A
Statement as written in the source
Lemma opnormN m n (A : 'M[R]_(m, n)) : opnorm (- A) = opnorm A.
Used by 7 declarations in 5 files
lemma opnormD main result source, line 145 
forall [R : realType] [m n : nat] (A B : 'M_(m, n)), opnorm (A + B) <= opnorm A + opnorm B
Main result

Stated in the README together with opnorm_leP.

Statement as written in the source
Lemma opnormD m n (A B : 'M[R]_(m, n)) : opnorm (A + B) <= opnorm A + opnorm B.
Used by 10 declarations in 7 files
lemma opnorm_mulmx main result source, line 152 
forall [R : realType] [m n p : nat] (A : 'M_(m, n)) (B : 'M_(n, p)),
opnorm (A *m B) <= opnorm A * opnorm B
Main result

Stated in the README together with opnorm_leP.

Statement as written in the source
Lemma opnorm_mulmx m n p (A : 'M[R]_(m, n)) (B : 'M[R]_(n, p)) :
  opnorm (A *m B) <= opnorm A * opnorm B.
Used by 1 declaration in 1 file
lemma mxdot_opnorm source, line 160 
forall [R : realType] [m n : nat] (A : 'M_(m, n)) (y : 'cV_m) (x : 'cV_n),
`|mxdot y (A *m x)| <= opnorm A * frobenius y * frobenius x
Statement as written in the source
Lemma mxdot_opnorm m n (A : 'M[R]_(m, n)) (y : 'cV[R]_m) (x : 'cV[R]_n) :
  `|mxdot y (A *m x)| <= opnorm A * frobenius y * frobenius x.
Used by 12 declarations in 8 files
lemma mxdot_delta_opnorm source, line 167 
forall [R : realType] [m n : nat] (A : 'M_(m, n)) (i : 'I_m) (j : 'I_n),
`|A i j| <= opnorm A * frobenius (delta_mx i 0 : 'cV_m) * frobenius (delta_mx j 0 : 'cV_n)
Statement as written in the source
Lemma mxdot_delta_opnorm m n (A : 'M[R]_(m, n)) i j :
  `|A i j| <= opnorm A * frobenius (delta_mx i 0 : 'cV[R]_m) *
    frobenius (delta_mx j 0 : 'cV[R]_n).
Used by 5 declarations in 5 files
lemma mx_norm_le_opnorm source, line 175 
forall [R : realType] [m n : nat] (A : 'M_(m, n)), mx_norm A <= opnorm A
Statement as written in the source
Lemma mx_norm_le_opnorm m n (A : 'M[R]_(m, n)) : mx_norm A <= opnorm A.
Used by 1 declaration in 1 file
lemma opnorm_bilinearP main result source, line 184 
forall [R : realType] [m n : nat] (A : 'M_(m, n)) [b : R],
0 <= b ->
(forall (y : 'cV_m) (x : 'cV_n), `|mxdot y (A *m x)| <= b * frobenius y * frobenius x) <->
opnorm A <= b
Main result

Stated in the README together with opnorm_leP.

Statement as written in the source
Lemma opnorm_bilinearP m n (A : 'M[R]_(m, n)) (b : R) : 0 <= b ->
  (forall (y : 'cV[R]_m) (x : 'cV[R]_n),
    `|mxdot y (A *m x)| <= b * frobenius y * frobenius x) <->
  opnorm A <= b.
Used by 2 declarations in 2 files
lemma opnorm_trmx main result source, line 198 
forall [R : realType] [m n : nat] (A : 'M_(m, n)), opnorm A^T = opnorm A
Main result

Stated in the README together with opnorm_leP.

Statement as written in the source
Lemma opnorm_trmx m n (A : 'M[R]_(m, n)) : opnorm A^T = opnorm A.
Used by 5 declarations in 4 files
lemma opnorm_orthogonalmxl source, line 206 
forall [R : realType] [m n : nat] [P : 'M_m] (A : 'M_(m, n)),
P \is orthogonalmx -> opnorm (P *m A) = opnorm A
Statement as written in the source
Lemma opnorm_orthogonalmxl m n (P : 'M[R]_m) (A : 'M[R]_(m, n)) :
  P \is orthogonalmx -> opnorm (P *m A) = opnorm A.
Used by 3 declarations in 3 files
lemma opnorm_orthogonalmxr source, line 214 
forall [R : realType] [m n : nat] (A : 'M_(m, n)) [Q : 'M_n],
Q \is orthogonalmx -> opnorm (A *m Q) = opnorm A
Statement as written in the source
Lemma opnorm_orthogonalmxr m n (A : 'M[R]_(m, n)) (Q : 'M[R]_n) :
  Q \is orthogonalmx -> opnorm (A *m Q) = opnorm A.
Used by 3 declarations in 3 files
lemma opnorm_symP main result source, line 223 
forall [R : realType] [n : nat] [A : 'M_n] [b : R],
A \is symmetricmx ->
0 <= b -> (forall x : 'cV_n, `|mxdot x (A *m x)| <= b * mxdot x x) <-> opnorm A <= b
Main result, as the README states it

For a symmetric matrix, opnorm A <= b if and only if |x^T A x| <= b x^T x for all x, and the operator norm is the largest absolute value of an eigenvalue.

Used in theories/ by: Feature/DiagonalTrace, SquareFree/EdgeUpper, SquareFree/EdgeLower, Spectral/OperatorTransport, Spectral/OrthogonalBounds, Head/TailSupport
Statement as written in the source
Lemma opnorm_symP n (A : 'M[R]_n) (b : R) : A \is symmetricmx -> 0 <= b ->
  (forall x : 'cV[R]_n, `|mxdot x (A *m x)| <= b * mxdot x x) <-> opnorm A <= b.
Used by 7 declarations in 6 files
lemma opnorm_spectral main result source, line 239 
forall [R : realType] [n : nat] [A P : 'M_n] [d : 'rV_n],
P \is orthogonalmx -> A = P^T *m diag_mx d *m P -> opnorm A = \big[Num.max/0]_i `|d 0 i|
Main result

Stated in the README together with opnorm_symP.

Statement as written in the source
Lemma opnorm_spectral n (A P : 'M[R]_n) (d : 'rV[R]_n) :
  P \is orthogonalmx -> A = P^T *m diag_mx d *m P ->
  opnorm A = \big[Num.max/0]_i `|d 0 i|.
Used by 3 declarations in 3 files
lemma opnorm_exp_le_trace source, line 257 
forall [R : realType] [n : nat] [A : 'M_n] (k : nat),
A \is symmetricmx -> opnorm A ^+ k.+1.*2 <= \tr (A ^+ k.+1.*2)
Statement as written in the source
Lemma opnorm_exp_le_trace n (A : 'M[R]_n) k : A \is symmetricmx ->
  opnorm A ^+ k.+1.*2 <= \tr (A ^+ k.+1.*2).
Used by 2 declarations in 2 files
lemma opnorm_exp_le_trace_even main result source, line 273 
forall [R : realType] [n : nat] [A : 'M_n] [p : nat],
A \is symmetricmx -> ~~ odd p -> (0 < p)%N -> opnorm A ^+ p <= \tr (A ^+ p)
Main result, as the README states it

For a symmetric matrix and an even exponent p > 0, opnorm A ^ p <= tr(A^p); so tr(A^p) <= t^p with t >= 0 gives opnorm A <= t, and so does x^T A^p x <= t^p x^T x for all x.

Used in theories/ by: Feature/DiagonalTrace, SquareFree/EdgeUpper, SquareFree/WalkNBEvent, SquareFree/EdgeLower
Statement as written in the source
Lemma opnorm_exp_le_trace_even n (A : 'M[R]_n) p : A \is symmetricmx ->
  ~~ odd p -> (0 < p)%N -> opnorm A ^+ p <= \tr (A ^+ p).
Used by 1 declaration in 1 file
lemma opnorm_le_trace_exp main result source, line 282 
forall [R : realType] [n : nat] [A : 'M_n] [p : nat] [t : R],
A \is symmetricmx ->
~~ odd p -> (0 < p)%N -> 0 <= t -> \tr (A ^+ p) <= t ^+ p -> opnorm A <= t
Main result

Stated in the README together with opnorm_exp_le_trace_even.

Statement as written in the source
Lemma opnorm_le_trace_exp n (A : 'M[R]_n) p (t : R) : A \is symmetricmx ->
  ~~ odd p -> (0 < p)%N -> 0 <= t -> \tr (A ^+ p) <= t ^+ p -> opnorm A <= t.
lemma opnorm_le_form_exp main result source, line 292 
forall [R : realType] [n : nat] [A : 'M_n] [p : nat] [t : R],
A \is symmetricmx ->
~~ odd p ->
(0 < p)%N ->
0 <= t -> (forall x : 'cV_n, mxdot x (A ^+ p *m x) <= t ^+ p * mxdot x x) -> opnorm A <= t

For a symmetric matrix and an even exponent p > 0, a bound t^p on the quadratic form of A^p bounds the operator norm by t.

Main result

Stated in the README together with opnorm_exp_le_trace_even.

Statement as written in the source
Lemma opnorm_le_form_exp n (A : 'M[R]_n) p (t : R) : A \is symmetricmx ->
  ~~ odd p -> (0 < p)%N -> 0 <= t ->
  (forall x : 'cV[R]_n, mxdot x (A ^+ p *m x) <= t ^+ p * mxdot x x) ->
  opnorm A <= t.
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.