Proof of The Exponential Series of a Real Square Matrix: Convergence, a Norm Bound and the Exponential Map

Computations with real numbers use The Real Numbers as a Type. Let $K=\lVert M\rVert$; then $K\ge0$ by Rules for the Operator Norm: Bound, Least Constant, Definiteness, Homogeneity, Triangle Inequality and Products (i). Let $(b_{k})_{k\in\mathbb{N}}$ be the sequence of The Exponential Series Converges Absolutely, and Its Sum Is a Map on ℝ (i) for $u=K$, so $b_{k}=K^{k-1}/(k-1)!$; then $b_{k}\ge0$ for every $k\in\mathbb{N}$, by Powers in a Commutative Ring, a Field and an Ordered Field: Exponent Laws, Factorisation, Geometric Sums, Monotonicity and Bernoulli's Inequality (vi) and Natural Numbers and Factorials Read in the Reals: the Order Carries Over, One Is Least, and Factorials Are Positive, Recursive and Nondecreasing (iii). By The Exponential Series Converges Absolutely, and Its Sum Is a Map on ℝ (ii), $\sum_{k=1}^{\infty}b_{k}$ converges, and its sum is $\exp(K)$ by The Real Exponential Function (i) and The Real Exponential Function (ii). $(\mathcal{M}_{n}(\mathbb{R}),d_{n})$ is a metric space by The Real Matrices with the Operator-Norm Distance Form a Complete Metric Space with Entrywise Convergence (i).

Proof of (i). The matrix product is a binary operation on $\mathcal{M}_{n}(\mathbb{R})$ with neutral element $I_{n}$, and $M^{m}$ is the power for it, as in Powers of a Square Matrix; so, by Maps Given by Iterated Operations: Partial Iterates, Images of Natural Numbers, Powers and Operations over a Finite Set (iii), there is a map $P:\mathbb{N}_{0}\to\mathcal{M}_{n}(\mathbb{R})$ with $P(m)=M^{m}$ for every $m\in\mathbb{N}_{0}$, and by The Factorial as a Map on the Natural Numbers with Zero (i) there is a map $\mathbb{N}_{0}\to\mathbb{N}_{0}$, $m\mapsto m!$. For $k\in\mathbb{N}$, $1\le k$ by Natural Numbers Are the Successors in Omega: One Is Least and Not a Successor of a Natural Number, the Successor Is Injective, and N Is Closed under Addition and Multiplication (ii), so $k-1\in\mathbb{N}_{0}$ is the difference, $(k-1)!>0$ in $\mathbb{R}$ by Natural Numbers and Factorials Read in the Reals: the Order Carries Over, One Is Least, and Factorials Are Positive, Recursive and Nondecreasing (iii), and $\frac{1}{(k-1)!}P(k-1)\in\mathcal{M}_{n}(\mathbb{R})$ by Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations (iv). So the map $T:\mathbb{N}\to\mathcal{M}_{n}(\mathbb{R})$, $k\mapsto\frac{1}{(k-1)!}P(k-1)=\frac{1}{(k-1)!}M^{k-1}$, given by this expression in $P$, the factorial and the difference, exists (Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (v)), and so, for $N\in\mathbb{N}$, does the map $[N]\to\mathcal{M}_{n}(\mathbb{R})$ given by the same expression on $[N]\subseteq\mathbb{N}$ (Intervals of Natural Numbers (ii)); the latter is the restriction $T|_{[N]}$, as both have the same values, and it is the only map $[N]\to\mathcal{M}_{n}(\mathbb{R})$ with these values, by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (iv). Hence $S_{N}(M)=\sum_{k=1}^{N}T_{k}$, the sum of $T|_{[N]}$ (Iterated Operations: Finite Sums and Finite Products (i) and Iterated Operations: Finite Sums and Finite Products (ii)).

The addition of $\mathcal{M}_{n}(\mathbb{R})$ is a binary operation on $\mathcal{M}_{n}(\mathbb{R})$ by Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations (iv). By Maps Given by Iterated Operations: Partial Iterates, Images of Natural Numbers, Powers and Operations over a Finite Set (i), with $T$ for $a$, there is exactly one map $\mathbb{N}\to\mathcal{M}_{n}(\mathbb{R})$ whose value at every $N\in\mathbb{N}$ is $\sum_{k=1}^{N}T_{k}=S_{N}(M)$, that is, by Sequences (i), exactly one sequence in $\mathcal{M}_{n}(\mathbb{R})$ with $N$-th term $S_{N}(M)$.

Let $N\in\mathbb{N}$. For every $X\in\mathcal{M}_{n}(\mathbb{R})$, what was shown for $M$ applies to $X$: the summand map $[N]\to\mathcal{M}_{n}(\mathbb{R})$, $k\mapsto\frac{1}{(k-1)!}X^{k-1}$, exists, and $S_{N}(X)$, its finite sum, lies in $\mathcal{M}_{n}(\mathbb{R})$. So $S_{N}(X)$ is an expression in $X$ built from defined set symbols (the finite sum, the summand map, powers, factorials and the difference), and the map $\mathcal{M}_{n}(\mathbb{R})\to\mathcal{M}_{n}(\mathbb{R})$, $X\mapsto S_{N}(X)$, exists (Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (v)); it is the only map with these values by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (iv). This proves (i).

Proof of (ii). Let $i,j\in[n]$, and let $(a_{k})_{k\in\mathbb{N}}$ be the sequence with $a_{k}=(M^{k-1})_{ij}/(k-1)!$ (a sequence by Sequences of Real Numbers Built from Given Ones: Partial Sums, Index Shifts, Predecessor Reindexing, Absolute Values and Termwise Operations (iii), with the map $q:\mathbb{N}_{0}\to\mathbb{R}$, $m\mapsto(M^{m})_{ij}/m!$, given by an expression in the map $m\mapsto M^{m}$ of Maps Given by Iterated Operations: Partial Iterates, Images of Natural Numbers, Powers and Operations over a Finite Set (iii) and the factorial map of The Factorial as a Map on the Natural Numbers with Zero (i) (Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (v))). It is the only sequence in $\mathbb{R}$ with these terms, by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (iv), a sequence in $\mathbb{R}$ being a map $\mathbb{N}\to\mathbb{R}$ (Sequences (i)). For $k\in\mathbb{N}$, The Operator Norm of Entries, Transposes, Multiples of the Identity, Orthogonal Factors and Diagonal Matrices (ii) and Powers of a Square Matrix (vi) give $|(M^{k-1})_{ij}|\le\lVert M^{k-1}\rVert\le K^{k-1}$, and dividing by $(k-1)!>0$ gives $|a_{k}|\le b_{k}$. By Series of Real Numbers with Nonnegative Terms, Comparison, Absolute Convergence and the Geometric Series (iv), $\sum_{k=1}^{\infty}a_{k}$ converges absolutely, and by Series of Real Numbers with Nonnegative Terms, Comparison, Absolute Convergence and the Geometric Series (iii) it converges. This proves (ii).

Proof of (iii). Let $(T_{k})_{k\in\mathbb{N}}$ be the sequence $T$ of the proof of (i), with $T_{k}=\frac{1}{(k-1)!}M^{k-1}$, so that $S_{N}(M)=\sum_{k=1}^{N}T_{k}$ for $N\in\mathbb{N}$. As $1+0=1$ by Arithmetic of Addition on Omega: Recursion Rules, Associativity, Commutativity, Cancellation and Compatibility with the Order (i), $1-1=0$ by The Difference of Two Natural Numbers with Zero (i); and for $N\in\mathbb{N}$, $N+1\in\mathbb{N}$ by Natural Numbers Are the Successors in Omega: One Is Least and Not a Successor of a Natural Number, the Successor Is Injective, and N Is Closed under Addition and Multiplication (ii) and Natural Numbers Are the Successors in Omega: One Is Least and Not a Successor of a Natural Number, the Successor Is Injective, and N Is Closed under Addition and Multiplication (vi), so $1\le N+1$ by Natural Numbers Are the Successors in Omega: One Is Least and Not a Successor of a Natural Number, the Successor Is Injective, and N Is Closed under Addition and Multiplication (ii), and $1+N=N+1$ by Arithmetic of Addition on Omega: Recursion Rules, Associativity, Commutativity, Cancellation and Compatibility with the Order (iv), so $(N+1)-1=N$. Hence, by Iterated Operations: Recursion, Splitting, Reordering, Termwise Combination and Homomorphisms (i), $S_{1}(M)=T_{1}=\frac{1}{0!}M^{0}=1\,I_{n}=I_{n}$, using $0!=1$ by The Factorial as a Map on the Natural Numbers with Zero (ii) and Powers of a Square Matrix (i), and $1\,I_{n}=I_{n}$ by Rules for Pointwise Operations on Real-Valued Maps: a Commutative Ring, Scalar Multiples and Evaluation (iii), with $[n]\times[n]$ for its $I$ (matrices being maps $[n]\times[n]\to\mathbb{R}$ with the pointwise operations, Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations (i) and Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations (iv)), and

$$S_{N+1}(M)=S_{N}(M)+T_{N+1}=S_{N}(M)+\frac{1}{N!}M^{N}\qquad(N\in\mathbb{N}).$$

This proves (iii).

Proof of (iv). Let $i,j\in[n]$ and let $(a_{k})$ be as in the proof of (ii), with partial sums $s_{N}=\sum_{k=1}^{N}a_{k}$. The map $\mathcal{M}_{n}(\mathbb{R})\to\mathbb{R}$, $X\mapsto X_{ij}$, satisfies $(X+Y)_{ij}=X_{ij}+Y_{ij}$ and $(cX)_{ij}=c\,X_{ij}$ by Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations (iv); so $(T_{k})_{ij}=a_{k}$, and by Iterated Operations: Recursion, Splitting, Reordering, Termwise Combination and Homomorphisms (ii)

$$\bigl(S_{N}(M)\bigr)_{ij}=\sum_{k=1}^{N}(T_{k})_{ij}=\sum_{k=1}^{N}a_{k}=s_{N}\qquad(N\in\mathbb{N}).$$

By (ii) and Series of Real Numbers: Partial Sums, Convergence, the Sum and Absolute Convergence (ii), $(s_{N})$ converges to the sum $\sigma_{ij}=\sum_{k=1}^{\infty}a_{k}$, as in Convergent Sequences of Real Numbers (i), that is, in $(\mathbb{R},d_{\mathbb{R}})$, by Predicative Formulas for Convergence and Limits, and Maps Defined by Limits (iv). The map $[n]\times[n]\to\mathbb{R}$, $(i,j)\mapsto\sigma_{ij}$ (a map given by limits, Predicative Formulas for Convergence and Limits, and Maps Defined by Limits (v)), is a matrix $E\in\mathcal{M}_{n}(\mathbb{R})$ with $E_{ij}=\sigma_{ij}$ by Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations (i) and Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations (ii), and it is the only matrix with these entries by Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations (iii). Since the entry sequences $\bigl((S_{N}(M))_{ij}\bigr)_{N\in\mathbb{N}}=(s_{N})$ converge to $E_{ij}$ in $(\mathbb{R},d_{\mathbb{R}})$ for all $i,j\in[n]$, the sequence $(S_{N}(M))$ converges to $E$ in $(\mathcal{M}_{n}(\mathbb{R}),d_{n})$ by The Real Matrices with the Operator-Norm Distance Form a Complete Metric Space with Entrywise Convergence (v). This proves (iv).

Proof of (v). Let $t_{N}=\sum_{k=1}^{N}b_{k}$ for $N\in\mathbb{N}$, so $t_{1}=b_{1}$ and $t_{N+1}=t_{N}+b_{N+1}$ by Sequences of Real Numbers Built from Given Ones: Partial Sums, Index Shifts, Predecessor Reindexing, Absolute Values and Termwise Operations (i), with $b_{1}=K^{0}/0!=1$, as $K^{0}=1$ by Powers with Exponents in the Natural Numbers with Zero (ii) and $0!=1$ by The Factorial as a Map on the Natural Numbers with Zero (ii), and $b_{N+1}=K^{N}/N!$ as $(N+1)-1=N$ (shown in the proof of (iii)). We show $\lVert S_{N}(M)\rVert\le t_{N}$ for every $N\in\mathbb{N}$, by induction on $N$ (Arithmetic and Order of the Natural Numbers (xiii)). For $N=1$, $\lVert S_{1}(M)\rVert=\lVert I_{n}\rVert=\lVert1\,I_{n}\rVert=1=t_{1}$ by The Operator Norm of Entries, Transposes, Multiples of the Identity, Orthogonal Factors and Diagonal Matrices (vi) with $t=1$. If $\lVert S_{N}(M)\rVert\le t_{N}$, then by (iii), Rules for the Operator Norm: Bound, Least Constant, Definiteness, Homogeneity, Triangle Inequality and Products (vi), Rules for the Operator Norm: Bound, Least Constant, Definiteness, Homogeneity, Triangle Inequality and Products (v) and Powers of a Square Matrix (vi),

$$\lVert S_{N+1}(M)\rVert\le\lVert S_{N}(M)\rVert+\frac{1}{N!}\lVert M^{N}\rVert\le t_{N}+\frac{K^{N}}{N!}=t_{N+1}.$$

By Series of Real Numbers with Nonnegative Terms, Comparison, Absolute Convergence and the Geometric Series (i), $t_{N}\le\sum_{k=1}^{\infty}b_{k}=\exp(K)$, so $\lVert S_{N}(M)\rVert\le\exp(K)$ for every $N\in\mathbb{N}$.

Let $\varepsilon>0$ be real. As $(S_{N}(M))$ converges to $E$ in $(\mathcal{M}_{n}(\mathbb{R}),d_{n})$ by (iv), Convergent Sequence in a Metric Space (i) gives $N\in\mathbb{N}$ with $d_{n}(S_{N}(M),E)<\varepsilon$. By The Real Matrices with the Operator-Norm Distance Form a Complete Metric Space with Entrywise Convergence (iii), $\lVert E\rVert-\lVert S_{N}(M)\rVert\le d_{n}(S_{N}(M),E)$, so $\lVert E\rVert<\exp(K)+\varepsilon$. As $\varepsilon$ was arbitrary, $\lVert E\rVert\le\exp(K)=\exp(\lVert M\rVert)$ by Arbitrary Positive Slack, and Approximation of Suprema and Infima, in the Real Numbers (i). This proves (v).

Proof of (vi). By (iv), for every $X\in\mathcal{M}_{n}(\mathbb{R})$ the sequence $(S_{N}(X))_{N\in\mathbb{N}}$ (the sequence of (i) with $X$ for $M$) is convergent in $(\mathcal{M}_{n}(\mathbb{R}),d_{n})$, and its limit is the matrix $E$ of (iv) for $X$, by Uniqueness of Limits in a Metric Space (i). By Predicative Formulas for Convergence and Limits, and Maps Defined by Limits (v), with $\mathcal{M}_{n}(\mathbb{R})$ for its $a$ and $(\mathcal{M}_{n}(\mathbb{R}),d_{n})$ for $(X,d)$, there is exactly one map $f:\mathcal{M}_{n}(\mathbb{R})\to\mathcal{M}_{n}(\mathbb{R})$ with $f(X)=\lim_{N\to\infty}S_{N}(X)$ for every $X$, that is, with $f(X)$ the matrix $E$ for $X$. This proves (vi).