Proof of The Earlier and the New Versions of the Definitions of Symmetric and Positive Semidefinite Matrices, the Operator Norm, Matrix Distance, Eigenvalues and Square Roots Agree

Routine facts about equal class abstractions are used without comment (Toolkit for AL3).

The two versions. Each new version treated here has the text of its earlier version, with the same anchors, except for its references: it adopts Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity in place of an earlier version of the routine-facts setting, cites Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations and Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations in place of Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations and Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations, and cites the new versions of the definitions of the dot product, the Euclidean norm, the matrix-vector product, the matrix product and the transpose, and of the other definitions treated here, in place of their earlier versions. The setting Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity extends Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, a later version of that setting, and adds readings of the same numbers as typed terms together with routine facts about them; so $\mathbb{N}$, $\mathbb{R}$ with its operations and its order, suprema of subsets of $\mathbb{R}$, and the segments $[n]$ mean the same in both versions. By The Earlier and the New Versions of the Definitions of Euclidean Space, Real Matrices and Normed Spaces Agree (i) and The Earlier and the New Versions of the Definitions of Euclidean Space, Real Matrices and Normed Spaces Agree (ii), the two versions have the same sets $\mathbb{R}^{n}$ and $\mathcal{M}_{m\times n}(\mathbb{R})$, with the same components and entries, the same sums, scalar multiples, negatives and differences, the same origin and the same zero matrix. By The Earlier and the New Versions of the Definitions of the Dot Product, the Euclidean Norm and Distance, and the Matrix Operations Agree (i), The Earlier and the New Versions of the Definitions of the Dot Product, the Euclidean Norm and Distance, and the Matrix Operations Agree (ii), The Earlier and the New Versions of the Definitions of the Dot Product, the Euclidean Norm and Distance, and the Matrix Operations Agree (iv), The Earlier and the New Versions of the Definitions of the Dot Product, the Euclidean Norm and Distance, and the Matrix Operations Agree (vi) and The Earlier and the New Versions of the Definitions of the Dot Product, the Euclidean Norm and Distance, and the Matrix Operations Agree (vii), they have the same dot product $x\cdot y$, Euclidean norm $\lVert x\rVert$, matrix-vector product $Ax$, matrix product $AB$ and transpose $A^{\top}$. It remains to check, clause by clause, that what each definition builds from these agrees.

Symmetric matrices. For (i), both versions call $A\in\mathcal{M}_{n}(\mathbb{R})$ symmetric when $A^{\top}=A$ (Symmetric Real Matrices and the Set $\mathcal{S}(n)$ (i), Symmetric Real Matrices and the Set $\mathcal{S}(n)$ (i)). The set $\mathcal{M}_{n}(\mathbb{R})$ and the transpose are the same in both versions, so this is one condition on $A$. Both versions define $\mathcal{S}(n)$ as the set of the $A\in\mathcal{M}_{n}(\mathbb{R})$ with $A^{\top}=A$ (Symmetric Real Matrices and the Set $\mathcal{S}(n)$ (ii), Symmetric Real Matrices and the Set $\mathcal{S}(n)$ (ii)); the two sets therefore have the same elements, and are equal.

Semidefiniteness. For (ii), let $A\in\mathcal{S}(n)$, the same set in both versions by (i). Both versions call $A$ positive semidefinite when

$$x\cdot(Ax)\ge0\qquad(x\in\mathbb{R}^{n}),$$

and positive definite when $x\cdot(Ax)>0$ for every $x\in\mathbb{R}^{n}$ with $x\neq0$ (Positive Semidefinite and Positive Definite Real Matrices (i), Positive Semidefinite and Positive Definite Real Matrices (i), Positive Semidefinite and Positive Definite Real Matrices (ii), Positive Semidefinite and Positive Definite Real Matrices (ii)). For each $x$ the real number $x\cdot(Ax)$ is the same in both versions, and so is the origin $0$; so each of the two conditions is the same in both.

The semidefinite ordering. For (iii), let $X,Y\in\mathcal{S}(n)$. Both versions define $X\preceq Y$ by

$$z\cdot(Xz)\le z\cdot(Yz)\qquad(z\in\mathbb{R}^{n})$$

(The Positive Semidefinite Ordering on Symmetric Matrices (i), The Positive Semidefinite Ordering on Symmetric Matrices (i)), and both sides are the same real numbers in both versions.

Operator norm. For (iv), both versions take the unit ball $U_{n}=\{x\in\mathbb{R}^{n}:\lVert x\rVert\le1\}$ and the sets $N_{B}=\{\lVert Bx\rVert:x\in U_{n}\}$ as in The Set of Lengths ‖Ax‖ over the Unit Ball Has a Supremum, and the Supremum Map Exists, the same lemma in both, and define $\lVert A\rVert$ as the value at $A$ of the map $B\mapsto\sup N_{B}$ of The Set of Lengths ‖Ax‖ over the Unit Ball Has a Supremum, and the Supremum Map Exists (iv) (The Operator Norm of a Real Matrix (i), The Operator Norm of a Real Matrix (i)). Since the Euclidean norm and the matrix-vector product are the same in both versions, the descriptions of $U_{n}$ and $N_{B}$ name the same sets in both; so the map, and its value $\lVert A\rVert$ at $A$, are the same.

Distance. For (v), both versions define $d_{m\times n}$ as the unique map $d$ of The Operator-Norm Distance between Real Matrices Is a Map (i), the same lemma in both, with

$$d_{m\times n}(A,B)=\lVert A-B\rVert$$

(The Distance between Real Matrices (i), The Distance between Real Matrices (i)). The difference $A-B$ is the same in both versions, and so is the operator norm by (iv); so the two versions name the same map.

Eigenvalues and eigenvectors. For (vi), both versions call $x\in\mathbb{R}^{n}$ an eigenvector of $A$ with eigenvalue $\lambda$ when $x\neq0$ and $Ax=\lambda x$ (Real Eigenvalues and Eigenvectors of a Real Square Matrix (i), Real Eigenvalues and Eigenvectors of a Real Square Matrix (i)). The origin, the matrix-vector product and the scalar multiple are the same in both versions, so this is one condition on $x$ and $\lambda$. Both versions call $\lambda$ an eigenvalue of $A$ when $A$ has an eigenvector with eigenvalue $\lambda$ (Real Eigenvalues and Eigenvectors of a Real Square Matrix (ii), Real Eigenvalues and Eigenvectors of a Real Square Matrix (ii)), and as the eigenvectors agree, so do the eigenvalues.

Square root. For (vii), let $A\in\mathcal{S}(n)$ be positive semidefinite, which means the same in both versions by (i) and (ii). Both versions define $A^{1/2}$ as the unique $B\in\mathcal{S}(n)$ that is positive semidefinite and satisfies $BB=A$, which exists and is unique by Every Positive Semidefinite Matrix Has Exactly One Positive Semidefinite Square Root (i), the same lemma in both (The Positive Semidefinite Square Root of a Positive Semidefinite Matrix (i), The Positive Semidefinite Square Root of a Positive Semidefinite Matrix (i)). The set $\mathcal{S}(n)$, positive semidefiniteness and the product $BB$ are the same in both versions by (i), (ii) and the agreement of the matrix products, so the two conditions on $B$ coincide, and the matrix they determine is the same.