GaussianAnalysisRocq library documentation
Main resultsGlossary
On this page
GaussianAnalysismatrixeuclidean

The Euclidean structure of real matrices

GaussianAnalysis.matrix.euclideanlibrary/matrix/euclidean.v363 lines60 lemmas and theorems, 3 definitionssource
Imports 0 library modules and 8 external

External: HB.structures, mathcomp.classical.all_ssreflect_compat, mathcomp.finite_group.fingroup, mathcomp.finite_group.perm, mathcomp.algebra.algebraic_hierarchy.ssralg, mathcomp.algebra.numeric_hierarchy.ssrnum, mathcomp.algebra.matrix, mathcomp.algebra.ring_tactic

Imported by 67
Required by 57 files of the paper proofs

The Frobenius inner product and norm of rectangular matrices, and orthogonal matrices. On row and column vectors, the Frobenius inner product and norm are the Euclidean inner product and norm.

mxdot A Bthe Frobenius inner product of A, B : 'M[R]_(m, n), \sum_i \sum_j A i j * B i j
frobenius Athe Frobenius norm Num.sqrt (mxdot A A) of A; the Euclidean norm when A is a row or a column vector
M \is orthogonalmxthe square matrix M is orthogonal: M *m M^T = 1

Main results

ResultsStatementUsed by theories/
mxdotfrobeniusmxdot_cauchy_schwarzfrobeniusDfrobenius_mulmx
mxdot A B, the sum of the A_(i, j) B_(i, j), is the Frobenius inner product of real matrices and frobenius A its norm. Cauchy-Schwarz holds, and the norm satisfies the triangle inequality and is submultiplicative. On row and column vectors they are the Euclidean inner product and norm.Spectral/SymmetricDiagonalization, Spectral/OperatorNet, Feature/DiagonalTrace, SquareFree/EdgeLower, SquareFree/WalkNBEvent, Gaussian/Tail/UnitLinear, Gaussian/Lipschitz/Concentration, Gaussian/Lipschitz/Variance, Gaussian/Orthogonal/WeightedSquareTail, Gordon/EscapeExpectation, Gordon/Processes; in the library, the nine files of comparison/ that handle vectors. mxdot_cauchy_schwarz and frobeniusD are used inside the library only
orthogonalmxmxdot_orthogonalmxlfrobenius_orthogonalmxr
The orthogonal matrices (M M^T = 1). Multiplying by an orthogonal matrix, on either side, preserves the Frobenius inner product and norm.Spectral/SymmetricDiagonalization, Spectral/OrthogonalBounds

Declarations64 exported

lemma, theoremdefinitioninstancelocal
sectionmxdot
Variable R : comNzRingType.
Implicit Types m n p : nat.
definition mxdot main result source, line 32
Type
forall [R : comNzRingType] [m n : nat], 'M_(m, n) -> 'M_(m, n) -> R
Definition
Definition mxdot m n (A B : 'M[R]_(m, n)) : R := \sum_i \sum_j A i j * B i j.
Main result, as the README states it

mxdot A B, the sum of the A_(i, j) B_(i, j), is the Frobenius inner product of real matrices and frobenius A its norm. Cauchy-Schwarz holds, and the norm satisfies the triangle inequality and is submultiplicative. On row and column vectors they are the Euclidean inner product and norm.

Used in theories/ by: Spectral/SymmetricDiagonalization, Spectral/OperatorNet, Feature/DiagonalTrace, SquareFree/EdgeLower, SquareFree/WalkNBEvent, Gaussian/Tail/UnitLinear, Gaussian/Lipschitz/Concentration, Gaussian/Lipschitz/Variance, Gaussian/Orthogonal/WeightedSquareTail, Gordon/EscapeExpectation, Gordon/Processes; in the library, the nine files of comparison/ that handle vectors. mxdot_cauchy_schwarz and frobeniusD are used inside the library only
Used by 596 declarations in 60 files
lemma mxdotC source, line 34 
forall [R : comNzRingType] [m n : nat] (A B : 'M_(m, n)), mxdot A B = mxdot B A
Statement as written in the source
Lemma mxdotC m n (A B : 'M[R]_(m, n)) : mxdot A B = mxdot B A.
Used by 74 declarations in 34 files
lemma mxdotDl source, line 37 
forall [R : comNzRingType] [m n : nat] (A B C : 'M_(m, n)),
mxdot (A + B) C = mxdot A C + mxdot B C
Statement as written in the source
Lemma mxdotDl m n (A B C : 'M[R]_(m, n)) :
  mxdot (A + B) C = mxdot A C + mxdot B C.
Used by 29 declarations in 18 files
lemma mxdotDr source, line 44 
forall [R : comNzRingType] [m n : nat] (A B C : 'M_(m, n)),
mxdot A (B + C) = mxdot A B + mxdot A C
Statement as written in the source
Lemma mxdotDr m n (A B C : 'M[R]_(m, n)) :
  mxdot A (B + C) = mxdot A B + mxdot A C.
Used by 36 declarations in 22 files
lemma mxdotZl source, line 48 
forall [R : comNzRingType] [m n : nat] (a : R) (A B : 'M_(m, n)),
mxdot (a *: A) B = a * mxdot A B
Statement as written in the source
Lemma mxdotZl m n a (A B : 'M[R]_(m, n)) : mxdot (a *: A) B = a * mxdot A B.
Used by 56 declarations in 28 files
lemma mxdotZr source, line 54 
forall [R : comNzRingType] [m n : nat] (a : R) (A B : 'M_(m, n)),
mxdot A (a *: B) = a * mxdot A B
Statement as written in the source
Lemma mxdotZr m n a (A B : 'M[R]_(m, n)) : mxdot A (a *: B) = a * mxdot A B.
Used by 73 declarations in 34 files
lemma mxdotNl source, line 57 
forall [R : comNzRingType] [m n : nat] (A B : 'M_(m, n)), mxdot (- A) B = - mxdot A B
Statement as written in the source
Lemma mxdotNl m n (A B : 'M[R]_(m, n)) : mxdot (- A) B = - mxdot A B.
Used by 18 declarations in 12 files
lemma mxdotNr source, line 60 
forall [R : comNzRingType] [m n : nat] (A B : 'M_(m, n)), mxdot A (- B) = - mxdot A B
Statement as written in the source
Lemma mxdotNr m n (A B : 'M[R]_(m, n)) : mxdot A (- B) = - mxdot A B.
Used by 16 declarations in 15 files
lemma mxdotBl source, line 63 
forall [R : comNzRingType] [m n : nat] (A B C : 'M_(m, n)),
mxdot (A - B) C = mxdot A C - mxdot B C
Statement as written in the source
Lemma mxdotBl m n (A B C : 'M[R]_(m, n)) :
  mxdot (A - B) C = mxdot A C - mxdot B C.
Used by 29 declarations in 19 files
lemma mxdotBr source, line 67 
forall [R : comNzRingType] [m n : nat] (A B C : 'M_(m, n)),
mxdot A (B - C) = mxdot A B - mxdot A C
Statement as written in the source
Lemma mxdotBr m n (A B C : 'M[R]_(m, n)) :
  mxdot A (B - C) = mxdot A B - mxdot A C.
Used by 35 declarations in 22 files
lemma mxdot0l source, line 71 
forall [R : comNzRingType] [m n : nat] (A : 'M_(m, n)), mxdot 0 A = 0
Statement as written in the source
Lemma mxdot0l m n (A : 'M[R]_(m, n)) : mxdot 0 A = 0.
Used by 38 declarations in 22 files
lemma mxdot0r source, line 74 
forall [R : comNzRingType] [m n : nat] (A : 'M_(m, n)), mxdot A 0 = 0
Statement as written in the source
Lemma mxdot0r m n (A : 'M[R]_(m, n)) : mxdot A 0 = 0.
Used by 18 declarations in 14 files
lemma mxdot_suml source, line 77 
forall [R : comNzRingType] [m n : nat] [I : Type] (r : seq I) (P : pred I)
  (F : I -> 'M_(m, n)) (B : 'M_(m, n)),
mxdot (\sum_(k <- r | P k) F k) B = \sum_(k <- r | P k) mxdot (F k) B
Statement as written in the source
Lemma mxdot_suml m n I (r : seq I) (P : pred I) (F : I -> 'M[R]_(m, n)) B :
  mxdot (\sum_(k <- r | P k) F k) B = \sum_(k <- r | P k) mxdot (F k) B.
Used by 17 declarations in 10 files
lemma mxdot_sumr source, line 81 
forall [R : comNzRingType] [m n : nat] [I : Type] (r : seq I) (P : pred I)
  (F : I -> 'M_(m, n)) (A : 'M_(m, n)),
mxdot A (\sum_(k <- r | P k) F k) = \sum_(k <- r | P k) mxdot A (F k)
Statement as written in the source
Lemma mxdot_sumr m n I (r : seq I) (P : pred I) (F : I -> 'M[R]_(m, n)) A :
  mxdot A (\sum_(k <- r | P k) F k) = \sum_(k <- r | P k) mxdot A (F k).
Used by 13 declarations in 7 files
lemma mxdot_trmx source, line 85 
forall [R : comNzRingType] [m n : nat] (A B : 'M_(m, n)), mxdot A^T B^T = mxdot A B
Statement as written in the source
Lemma mxdot_trmx m n (A B : 'M[R]_(m, n)) : mxdot A^T B^T = mxdot A B.
Used by 26 declarations in 19 files
lemma mxdot_trace source, line 91 
forall [R : comNzRingType] [m n : nat] (A B : 'M_(m, n)), mxdot A B = \tr (A *m B^T)
Statement as written in the source
Lemma mxdot_trace m n (A B : 'M[R]_(m, n)) : mxdot A B = \tr (A *m B^T).
Used by 29 declarations in 19 files
lemma mxdot_mulmxl source, line 97 
forall [R : comNzRingType] [m n p : nat] (A : 'M_(m, n)) (B : 'M_(n, p)) (C : 'M_(m, p)),
mxdot (A *m B) C = mxdot B (A^T *m C)
Statement as written in the source
Lemma mxdot_mulmxl m n p (A : 'M[R]_(m, n)) (B : 'M[R]_(n, p)) C :
  mxdot (A *m B) C = mxdot B (A^T *m C).
Used by 20 declarations in 10 files
lemma mxdot_mulmxr source, line 103 
forall [R : comNzRingType] [m n p : nat] (A : 'M_(m, n)) (B : 'M_(n, p)) (C : 'M_(m, p)),
mxdot (A *m B) C = mxdot A (C *m B^T)
Statement as written in the source
Lemma mxdot_mulmxr m n p (A : 'M[R]_(m, n)) (B : 'M[R]_(n, p)) C :
  mxdot (A *m B) C = mxdot A (C *m B^T).
Used by 17 declarations in 10 files
lemma mxdot_rowE source, line 107 
forall [R : comNzRingType] [n : nat] (u v : 'rV_n), mxdot u v = (u *m v^T) 0 0
Statement as written in the source
Lemma mxdot_rowE n (u v : 'rV[R]_n) : mxdot u v = (u *m v^T) 0 0.
Used by 15 declarations in 13 files
lemma mxdot_colE source, line 110 
forall [R : comNzRingType] [n : nat] (x y : 'cV_n), mxdot x y = (x^T *m y) 0 0
Statement as written in the source
Lemma mxdot_colE n (x y : 'cV[R]_n) : mxdot x y = (x^T *m y) 0 0.
Used by 13 declarations in 8 files
lemma mxdot_outer source, line 113 
forall [R : comNzRingType] [m n : nat] (A : 'M_(m, n)) (x : 'cV_m) (y : 'cV_n),
mxdot A (x *m y^T) = (x^T *m A *m y) 0 0
Statement as written in the source
Lemma mxdot_outer m n (A : 'M[R]_(m, n)) (x : 'cV[R]_m) (y : 'cV[R]_n) :
  mxdot A (x *m y^T) = (x^T *m A *m y) 0 0.
Used by 7 declarations in 6 files
lemma mxdot_outer2 source, line 120 
forall [R : comNzRingType] [m n : nat] (a c : 'cV_m) (b e : 'cV_n),
mxdot (a *m b^T) (c *m e^T) = mxdot a c * mxdot b e
Statement as written in the source
Lemma mxdot_outer2 m n (a c : 'cV[R]_m) (b e : 'cV[R]_n) :
  mxdot (a *m b^T) (c *m e^T) = mxdot a c * mxdot b e.
Used by 5 declarations in 5 files
lemma mxdot_diag source, line 127 
forall [R : comNzRingType] [n : nat] (a b : 'rV_n),
mxdot (diag_mx a) (diag_mx b) = \sum_i a 0 i * b 0 i
Statement as written in the source
Lemma mxdot_diag n (a b : 'rV[R]_n) :
  mxdot (diag_mx a) (diag_mx b) = \sum_i a 0 i * b 0 i.
Used by 6 declarations in 4 files
lemma mxdot_delta source, line 135 
forall [R : comNzRingType] [m n : nat] (A : 'M_(m, n))
  (i : 'I_m)
  (j : 'I_n),
mxdot A (delta_mx i j) = A i j
Statement as written in the source
Lemma mxdot_delta m n (A : 'M[R]_(m, n)) i j : mxdot A (delta_mx i j) = A i j.
Used by 31 declarations in 17 files
sectionmxdot_real
Variable R : realDomainType.
Implicit Types m n : nat.
lemma mxdot_ge0 source, line 150 
forall [R : realDomainType] [m n : nat] (A : 'M_(m, n)), 0 <= mxdot A A
Statement as written in the source
Lemma mxdot_ge0 m n (A : 'M[R]_(m, n)) : 0 <= mxdot A A.
Used by 80 declarations in 30 files
lemma mxdot_eq0 source, line 155 
forall [R : realDomainType] [m n : nat] (A : 'M_(m, n)), (mxdot A A == 0) = (A == 0)
Statement as written in the source
Lemma mxdot_eq0 m n (A : 'M[R]_(m, n)) : (mxdot A A == 0) = (A == 0).
Used by 10 declarations in 7 files
lemma mxdot_gt0 source, line 166 
forall [R : realDomainType] [m n : nat] (A : 'M_(m, n)), (0 < mxdot A A) = (A != 0)
Statement as written in the source
Lemma mxdot_gt0 m n (A : 'M[R]_(m, n)) : (0 < mxdot A A) = (A != 0).
Used by 10 declarations in 8 files
lemma mxdot_cauchy_schwarz main result source, line 169 
forall [R : realDomainType] [m n : nat] (A B : 'M_(m, n)),
mxdot A B ^+ 2 <= mxdot A A * mxdot B B
Main result

Stated in the README together with mxdot.

Statement as written in the source
Lemma mxdot_cauchy_schwarz m n (A B : 'M[R]_(m, n)) :
  mxdot A B ^+ 2 <= mxdot A A * mxdot B B.
Used by 14 declarations in 5 files
lemma sum_cauchy_schwarz source, line 182 
forall [R : realDomainType] [n : nat] (a b : 'I_n -> R),
(\sum_i a i * b i) ^+ 2 <= (\sum_i a i * a i) * \sum_i b i * b i
Statement as written in the source
Lemma sum_cauchy_schwarz n (a b : 'I_n -> R) :
  (\sum_i a i * b i) ^+ 2 <= (\sum_i a i * a i) * (\sum_i b i * b i).
Used by 9 declarations in 8 files
lemma mxdot_entry source, line 191 
forall [R : realDomainType] [m n : nat] (A : 'M_(m, n)) (i : 'I_m) (j : 'I_n),
A i j ^+ 2 <= mxdot A A
Statement as written in the source
Lemma mxdot_entry m n (A : 'M[R]_(m, n)) i j : A i j ^+ 2 <= mxdot A A.
Used by 10 declarations in 7 files
sectionfrobenius
Variable R : rcfType.
Implicit Types m n p : nat.
definition frobenius main result source, line 204
Type
forall [R : rcfType] [m n : nat], 'M_(m, n) -> R
Definition
Definition frobenius m n (A : 'M[R]_(m, n)) : R := Num.sqrt (mxdot A A).
Main result

Stated in the README together with mxdot.

Used by 369 declarations in 49 files
lemma frobenius_ge0 source, line 206 
forall [R : rcfType] [m n : nat] (A : 'M_(m, n)), 0 <= frobenius A
Statement as written in the source
Lemma frobenius_ge0 m n (A : 'M[R]_(m, n)) : 0 <= frobenius A.
Used by 130 declarations in 34 files
lemma frobenius_sqr source, line 209 
forall [R : rcfType] [m n : nat] (A : 'M_(m, n)), frobenius A ^+ 2 = mxdot A A
Statement as written in the source
Lemma frobenius_sqr m n (A : 'M[R]_(m, n)) : frobenius A ^+ 2 = mxdot A A.
Used by 87 declarations in 35 files
lemma frobenius_eq0 source, line 212 
forall [R : rcfType] [m n : nat] (A : 'M_(m, n)), (frobenius A == 0) = (A == 0)
Statement as written in the source
Lemma frobenius_eq0 m n (A : 'M[R]_(m, n)) : (frobenius A == 0) = (A == 0).
Used by 7 declarations in 4 files
lemma frobenius_gt0 source, line 215 
forall [R : rcfType] [m n : nat] (A : 'M_(m, n)), (0 < frobenius A) = (A != 0)
Statement as written in the source
Lemma frobenius_gt0 m n (A : 'M[R]_(m, n)) : (0 < frobenius A) = (A != 0).
Used by 18 declarations in 12 files
lemma frobenius0 source, line 218 
forall (R : rcfType) (m n : nat), frobenius (0 : 'M_(m, n)) = 0
Statement as written in the source
Lemma frobenius0 m n : frobenius (0 : 'M[R]_(m, n)) = 0.
Used by 31 declarations in 16 files
lemma frobeniusZ source, line 221 
forall [R : rcfType] [m n : nat] (a : R) (A : 'M_(m, n)),
frobenius (a *: A) = `|a| * frobenius A
Statement as written in the source
Lemma frobeniusZ m n a (A : 'M[R]_(m, n)) :
  frobenius (a *: A) = `|a| * frobenius A.
Used by 26 declarations in 16 files
lemma frobeniusN source, line 227 
forall [R : rcfType] [m n : nat] (A : 'M_(m, n)), frobenius (- A) = frobenius A
Statement as written in the source
Lemma frobeniusN m n (A : 'M[R]_(m, n)) : frobenius (- A) = frobenius A.
Used by 28 declarations in 11 files
lemma frobenius_trmx source, line 230 
forall [R : rcfType] [m n : nat] (A : 'M_(m, n)), frobenius A^T = frobenius A
Statement as written in the source
Lemma frobenius_trmx m n (A : 'M[R]_(m, n)) : frobenius A^T = frobenius A.
Used by 34 declarations in 10 files
lemma frobenius_rowE source, line 233 
forall [R : rcfType] [n : nat] (u : 'rV_n),
frobenius u = Num.ExtraDef.sqrtr ((u *m u^T) 0 0)
Statement as written in the source
Lemma frobenius_rowE n (u : 'rV[R]_n) : frobenius u = Num.sqrt ((u *m u^T) 0 0).
lemma frobenius_colE source, line 236 
forall [R : rcfType] [n : nat] (x : 'cV_n),
frobenius x = Num.ExtraDef.sqrtr ((x^T *m x) 0 0)
Statement as written in the source
Lemma frobenius_colE n (x : 'cV[R]_n) : frobenius x = Num.sqrt ((x^T *m x) 0 0).
lemma mxdot_le source, line 239 
forall [R : rcfType] [m n : nat] (A B : 'M_(m, n)),
`|mxdot A B| <= frobenius A * frobenius B
Statement as written in the source
Lemma mxdot_le m n (A B : 'M[R]_(m, n)) :
  `|mxdot A B| <= frobenius A * frobenius B.
Used by 21 declarations in 12 files
lemma ler_mxdot source, line 246 
forall [R : rcfType] [m n : nat] (A B : 'M_(m, n)), mxdot A B <= frobenius A * frobenius B
Statement as written in the source
Lemma ler_mxdot m n (A B : 'M[R]_(m, n)) :
  mxdot A B <= frobenius A * frobenius B.
Used by 26 declarations in 14 files
lemma frobeniusD main result source, line 250 
forall [R : rcfType] [m n : nat] (A B : 'M_(m, n)),
frobenius (A + B) <= frobenius A + frobenius B
Main result

Stated in the README together with mxdot.

Statement as written in the source
Lemma frobeniusD m n (A B : 'M[R]_(m, n)) :
  frobenius (A + B) <= frobenius A + frobenius B.
Used by 21 declarations in 13 files
lemma frobeniusB source, line 258 
forall [R : rcfType] [m n : nat] (A B : 'M_(m, n)),
frobenius (A - B) <= frobenius A + frobenius B
Statement as written in the source
Lemma frobeniusB m n (A B : 'M[R]_(m, n)) :
  frobenius (A - B) <= frobenius A + frobenius B.
Used by 2 declarations in 2 files
lemma ler_frobeniusB source, line 262 
forall [R : rcfType] [m n : nat] (A B : 'M_(m, n)),
`|frobenius A - frobenius B| <= frobenius (A - B)
Statement as written in the source
Lemma ler_frobeniusB m n (A B : 'M[R]_(m, n)) :
  `|frobenius A - frobenius B| <= frobenius (A - B).
Used by 12 declarations in 4 files
lemma frobenius_entry source, line 272 
forall [R : rcfType] [m n : nat] (A : 'M_(m, n)) (i : 'I_m) (j : 'I_n),
`|A i j| <= frobenius A
Statement as written in the source
Lemma frobenius_entry m n (A : 'M[R]_(m, n)) i j : `|A i j| <= frobenius A.
Used by 13 declarations in 6 files
lemma frobenius_mulmx main result source, line 275 
forall [R : rcfType] [m n p : nat] (A : 'M_(m, n)) (B : 'M_(n, p)),
frobenius (A *m B) <= frobenius A * frobenius B
Main result

Stated in the README together with mxdot.

Statement as written in the source
Lemma frobenius_mulmx m n p (A : 'M[R]_(m, n)) (B : 'M[R]_(n, p)) :
  frobenius (A *m B) <= frobenius A * frobenius B.
Used by 16 declarations in 8 files
sectionorthogonal
Variable R : comUnitRingType.
Implicit Types m n : nat.
definition orthogonalmx main result source, line 293
Type
forall {R : comUnitRingType} {n : nat}, qualifier 0 'M_n
Definition
Definition orthogonalmx {n} := [qualify M : 'M[R]_n | M *m M^T == 1%:M].
Main result, as the README states it

The orthogonal matrices (M M^T = 1). Multiplying by an orthogonal matrix, on either side, preserves the Frobenius inner product and norm.

Used in theories/ by: Spectral/SymmetricDiagonalization, Spectral/OrthogonalBounds
Used by 59 declarations in 14 files
fact orthogonalmx_key source, line 294 
forall (R : comUnitRingType) (n : nat), pred_key orthogonalmx
Statement as written in the source
Fact orthogonalmx_key n : pred_key (@orthogonalmx n).
Used by 1 declaration in 1 file
canonical orthogonalmx_keyed source, line 295 
Canonical orthogonalmx_keyed n := KeyedQualifier (orthogonalmx_key n).
lemma orthogonalmxP source, line 297 
forall [R : comUnitRingType] [n : nat] (M : 'M_n),
reflect (M *m M^T = 1%:M) (M \is orthogonalmx)
Statement as written in the source
Lemma orthogonalmxP n (M : 'M[R]_n) :
  reflect (M *m M^T = 1%:M) (M \is orthogonalmx).
Used by 34 declarations in 15 files
lemma orthogonalmxT source, line 301 
forall [R : comUnitRingType] [n : nat] [M : 'M_n], M \is orthogonalmx -> M^T *m M = 1%:M
Statement as written in the source
Lemma orthogonalmxT n (M : 'M[R]_n) : M \is orthogonalmx -> M^T *m M = 1%:M.
Used by 12 declarations in 9 files
lemma trmx_orthogonal source, line 304 
forall [R : comUnitRingType] [n : nat] (M : 'M_n),
(M^T \is orthogonalmx) = (M \is orthogonalmx)
Statement as written in the source
Lemma trmx_orthogonal n (M : 'M[R]_n) :
  (M^T \is orthogonalmx) = (M \is orthogonalmx).
Used by 19 declarations in 11 files
lemma orthogonalmx1 source, line 308 
forall (R : comUnitRingType) (n : nat), (1%:M : 'M_n) \is orthogonalmx
Statement as written in the source
Lemma orthogonalmx1 n : (1%:M : 'M[R]_n) \is orthogonalmx.
Used by 2 declarations in 1 file
lemma mul_orthogonalmx source, line 311 
forall [R : comUnitRingType] [n : nat] [A B : 'M_n],
A \is orthogonalmx -> B \is orthogonalmx -> A *m B \is orthogonalmx
Statement as written in the source
Lemma mul_orthogonalmx n (A B : 'M[R]_n) :
  A \is orthogonalmx -> B \is orthogonalmx -> A *m B \is orthogonalmx.
Used by 4 declarations in 3 files
lemma orthogonalmx_unit source, line 318 
forall [R : comUnitRingType] [n : nat] [M : 'M_n], M \is orthogonalmx -> M \in unitmx
Statement as written in the source
Lemma orthogonalmx_unit n (M : 'M[R]_n) : M \is orthogonalmx -> M \in unitmx.
Used by 3 declarations in 2 files
lemma invmx_orthogonal source, line 321 
forall [R : comUnitRingType] [n : nat] [M : 'M_n], M \is orthogonalmx -> invmx M = M^T
Statement as written in the source
Lemma invmx_orthogonal n (M : 'M[R]_n) : M \is orthogonalmx -> invmx M = M^T.
lemma orthogonal_block_mx source, line 327 
forall [R : comUnitRingType] [m n : nat] [P : 'M_m] [Q : 'M_n],
P \is orthogonalmx -> Q \is orthogonalmx -> block_mx P 0 0 Q \is orthogonalmx
Statement as written in the source
Lemma orthogonal_block_mx m n (P : 'M[R]_m) (Q : 'M[R]_n) :
  P \is orthogonalmx -> Q \is orthogonalmx -> block_mx P 0 0 Q \is orthogonalmx.
Used by 1 declaration in 1 file
lemma perm_mx_orthogonal source, line 335 
forall (R : comUnitRingType) [n : nat] (s : {perm 'I_n}), perm_mx s \is orthogonalmx
Statement as written in the source
Lemma perm_mx_orthogonal n (s : 'S_n) : perm_mx s \is orthogonalmx.
Used by 1 declaration in 1 file
lemma mxdot_orthogonalmxl main result source, line 338 
forall [R : comUnitRingType] [m n : nat] [P : 'M_m] (A B : 'M_(m, n)),
P \is orthogonalmx -> mxdot (P *m A) (P *m B) = mxdot A B
Main result

Stated in the README together with orthogonalmx.

Statement as written in the source
Lemma mxdot_orthogonalmxl m n (P : 'M[R]_m) (A B : 'M[R]_(m, n)) :
  P \is orthogonalmx -> mxdot (P *m A) (P *m B) = mxdot A B.
Used by 14 declarations in 10 files
lemma mxdot_orthogonalmxr source, line 342 
forall [R : comUnitRingType] [m n : nat] [P : 'M_n] (A B : 'M_(m, n)),
P \is orthogonalmx -> mxdot (A *m P) (B *m P) = mxdot A B
Statement as written in the source
Lemma mxdot_orthogonalmxr m n (P : 'M[R]_n) (A B : 'M[R]_(m, n)) :
  P \is orthogonalmx -> mxdot (A *m P) (B *m P) = mxdot A B.
Used by 11 declarations in 9 files
Arguments orthogonalmx {R n}.
sectionorthogonal_frobenius
Variable R : rcfType.
Implicit Types m n : nat.
lemma frobenius_orthogonalmxl source, line 355 
forall [R : rcfType] [m n : nat] [P : 'M_m] (A : 'M_(m, n)),
P \is orthogonalmx -> frobenius (P *m A) = frobenius A
Statement as written in the source
Lemma frobenius_orthogonalmxl m n (P : 'M[R]_m) (A : 'M[R]_(m, n)) :
  P \is orthogonalmx -> frobenius (P *m A) = frobenius A.
Used by 2 declarations in 1 file
lemma frobenius_orthogonalmxr main result source, line 359 
forall [R : rcfType] [m n : nat] [P : 'M_n] (A : 'M_(m, n)),
P \is orthogonalmx -> frobenius (A *m P) = frobenius A
Main result

Stated in the README together with orthogonalmx.

Statement as written in the source
Lemma frobenius_orthogonalmxr m n (P : 'M[R]_n) (A : 'M[R]_(m, n)) :
  P \is orthogonalmx -> frobenius (A *m P) = frobenius A.
Used by 1 declaration in 1 file
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.