Proof of The Set of Lengths ‖Ax‖ over the Unit Ball Has a Supremum, and the Supremum Map Exists

Each result cited is universally quantified over the data in its own statement.

We work in Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices. $\mathbb{R}$ is an ordered field by The Real Numbers Form an Ordered Field in Which Every Nonempty Set Bounded Above Has a Supremum §ordered-field, so the results on ordered fields cited below apply to it. For $B\in\mathcal{M}_{m\times n}(\mathbb{R})$ and $x\in\mathbb{R}^{n}$, the matrix-vector product $Bx\in\mathbb{R}^{m}$ is the value of the map of The Matrix Product, Matrix-Vector Product, Transpose, Trace, Identity Matrix and Standard Basis Vectors Exist and Are Unique §matrix-vector, by Matrix-Vector Product §product.

The sets $U_{n}$ and $N_{B}$. $U_{n}=\{x\in\mathbb{R}^{n}:\lVert x\rVert\le1\}$ is a set-builder subset of $\mathbb{R}^{n}$, its condition being the membership of the pair $(\lVert x\rVert,1)$ in the order $\le$, with $\lVert x\rVert$ the value at $x$ of the map of The Summation Map on Real-Valued Maps over a Finite Set, and the Dot Product, Euclidean Norm and Euclidean Distance as Maps §norm; so, for every set $x$, $x\in U_{n}$ if and only if $x\in\mathbb{R}^{n}$ and $\lVert x\rVert\le1$. The set $U_{n}$ does not depend on $B$: it enters the formulas below as a parameter, a set variable to which the set $U_{n}$ is assigned, as do $\mathbb{R}^{n}$, $\mathbb{R}$, $\mathcal{M}_{m\times n}(\mathbb{R})$ and the maps of The Matrix Product, Matrix-Vector Product, Transpose, Trace, Identity Matrix and Standard Basis Vectors Exist and Are Unique §matrix-vector and The Summation Map on Real-Valued Maps over a Finite Set, and the Dot Product, Euclidean Norm and Euclidean Distance as Maps §norm.

Let $\gamma$ be the guard $B\in\mathcal{M}_{m\times n}(\mathbb{R})$ for the variable $B$, and let $x$ be a set variable other than $B$. Under the guard $\gamma\wedge x\in U_{n}$, for the variables $B$ and $x$, the variables $B$ and $x$ are terms of type $\mathcal{M}_{m\times n}(\mathbb{R})$ and of type $\mathbb{R}^{n}$, as $U_{n}\subseteq\mathbb{R}^{n}$ (Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them §variable), so $(B,x)$ is a term of type $\mathcal{M}_{m\times n}(\mathbb{R})\times\mathbb{R}^{n}$ (Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them §pair); applying to it the map of The Matrix Product, Matrix-Vector Product, Transpose, Trace, Identity Matrix and Standard Basis Vectors Exist and Are Unique §matrix-vector, and then the map of The Summation Map on Real-Valued Maps over a Finite Set, and the Dot Product, Euclidean Norm and Euclidean Distance as Maps §norm on $\mathbb{R}^{m}$, gives the terms $Bx$ of type $\mathbb{R}^{m}$ and $\lVert Bx\rVert$ of type $\mathbb{R}$ (Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them §value). By Images of Typed Terms: the Set of Values $\{t:u\in D\}$ Is a Set, Finite when $D$ Is Finite, and a Typed Term §typed, with $B$ for its $x_{1}$, $\gamma$ for its $\gamma$, $x$ for its $u$, $U_{n}$ for its $D$, $\lVert Bx\rVert$ for its $t$, $\mathbb{R}$ for its $B$ and the power set $\mathcal{P}(\mathbb{R})$ for its $C$, $N_{B}=\{\lVert Bx\rVert:x\in U_{n}\}$ is a term of type $\mathcal{P}(\mathbb{R})$ under $\gamma$: for every $B\in\mathcal{M}_{m\times n}(\mathbb{R})$ it is a set and a subset of $\mathbb{R}$ (Images of Typed Terms: the Set of Values $\{t:u\in D\}$ Is a Set, Finite when $D$ Is Finite, and a Typed Term §set), and the condition $\gamma\wedge z=N_{B}$ on $B$ and a set variable $z$ is expressed by a predicative formula. By Images of Typed Terms: the Set of Values $\{t:u\in D\}$ Is a Set, Finite when $D$ Is Finite, and a Typed Term §members, for every set $s$: $s\in N_{B}$ if and only if $s=\lVert Bx\rVert$ for some $x\in U_{n}$. With $A$ for $B$, these descriptions of the elements of $U_{n}$ and of $N_{A}$ are the clause membership.

Clause bounded. By the above, $N_{A}$ is a subset of $\mathbb{R}$. Let $0$ denote the origin of $\mathbb{R}^{n}$ and of $\mathbb{R}^{m}$. By Properties of the Euclidean Norm on $\mathbb{R}^n$: Square, Distance, Vanishing, Coordinate Bounds, Homogeneity, Triangle Inequalities and Expansion of a Square §vanishing, $\lVert0\rVert=0$, and $0\le1$; so $0\in U_{n}$. By Algebraic Rules for Matrix Products, Matrix-Vector Products and Transposes §matrix-vector, $A0=0$, so $\lVert A0\rVert=0$ by the same norm clause, vanishing, in $\mathbb{R}^{m}$. Hence $0\in N_{A}$, and $N_{A}$ is nonempty.

Let $A_{ij}$ be the entries of $A$, and let $\Phi_{A}=\sum_{i=1}^{m}\sum_{j=1}^{n}A_{ij}^{2}$, a sum of real numbers. For $i\in[m]$ and $j\in[n]$, $A_{ij}^{2}=A_{ij}\cdot A_{ij}\ge0$ by Rules of Arithmetic and Order in an Ordered Field §squares. Hence Finite Sums in a Commutative Ring and in an Ordered Field: Distributivity, Differences, Telescoping, Constant Terms, Comparison and the Triangle Inequality §nonnegative, applied for each $i\in[m]$ to the map $j\mapsto A_{ij}^{2}$ from $[n]$ to $\mathbb{R}$, and then to the map $i\mapsto\sum_{j=1}^{n}A_{ij}^{2}$ from $[m]$ to $\mathbb{R}$, gives $\sum_{j=1}^{n}A_{ij}^{2}\ge0$ for every $i\in[m]$, and $\Phi_{A}\ge0$. These are maps: with $q:\mathbb{R}\to\mathbb{R}$ the map $y\mapsto y^{2}$ of Absolute Value and Squaring as Maps on the Reals, and Entrywise Absolute Values and Squares of a Real Matrix §square, the composite $q\circ A\in\mathcal{M}_{m\times n}(\mathbb{R})$ has entries $(q\circ A)_{ij}=A_{ij}^{2}$ by Absolute Value and Squaring as Maps on the Reals, and Entrywise Absolute Values and Squares of a Real Matrix §entrywise; and Maps Given by Iterated Operations: Partial Iterates, Images of Natural Numbers, Powers and Operations over a Finite Set §finite-operation, with the addition of $\mathbb{R}$, which has the neutral element $0$, for its $\ast$, $[m]$ and $[n]$ for its $A$ and $B$ ($[n]$ being finite by Finite Sets: the Pigeonhole Principle, Uniqueness of the Length, Subsets, Unions, Products, Images, Bounded Sets of Natural Numbers, Extreme Elements, Sets of Maps, Finite Unions and Finite Choice §naturals) and $q\circ A$ for its $f$, gives the maps $j\mapsto A_{ij}^{2}$ from $[n]$ to $\mathbb{R}$, for $i\in[m]$, and the map $i\mapsto\sum_{j=1}^{n}A_{ij}^{2}$ from $[m]$ to $\mathbb{R}$. By Existence and Uniqueness of Nonnegative k-th Roots of Nonnegative Real Numbers §root with $k=2$, there is $r\in\mathbb{R}$ with $r\ge0$ and $r^{2}=\Phi_{A}$.

Let $s\in N_{A}$, and let $x\in U_{n}$ with $s=\lVert Ax\rVert$. By Properties of the Euclidean Norm on $\mathbb{R}^n$: Square, Distance, Vanishing, Coordinate Bounds, Homogeneity, Triangle Inequalities and Expansion of a Square §square, $0\le\lVert x\rVert$ and $0\le\lVert Ax\rVert$. As $0\le\lVert x\rVert\le1$ and $0\le1$, Powers in a Commutative Ring, a Field and an Ordered Field: Exponent Laws, Factorisation, Geometric Sums, Monotonicity and Bernoulli's Inequality §monotone-iff, with $2$ for its $n$, gives $\lVert x\rVert^{2}\le1^{2}=1$; and Inequalities in an Ordered Field: Mixed Transitivity, Strict Sums, Signs, Products, Natural Numbers, Halving, Reciprocals, Absolute Values and Squares §nonnegative-scaling, applied to $\lVert x\rVert^{2}\le1$ with $\Phi_{A}$ for its $z$, gives $\Phi_{A}\lVert x\rVert^{2}\le\Phi_{A}$. By Algebraic Rules for Matrix Products, Matrix-Vector Products and Transposes §bound,

$$\lVert Ax\rVert^{2}\le\Phi_{A}\lVert x\rVert^{2}\le\Phi_{A}=r^{2}.$$

As $\lVert Ax\rVert\ge0$ and $r\ge0$, Powers in a Commutative Ring, a Field and an Ordered Field: Exponent Laws, Factorisation, Geometric Sums, Monotonicity and Bernoulli's Inequality §monotone-iff, with $2$ for its $n$, gives $\lVert Ax\rVert\le r$, that is, $s\le r$. So $r\in\mathbb{R}$ is an upper bound of $N_{A}$ in the sense of Bounds, Least and Greatest Elements, Suprema and Infima for a Partial Order §bounds, and $N_{A}$ is bounded above by Bounds, Least and Greatest Elements, Suprema and Infima for a Partial Order §bounded.

Clause supremum. By the clause bounded, $N_{A}$ is a nonempty subset of $\mathbb{R}$ that is bounded above. By The Real Numbers Form an Ordered Field in Which Every Nonempty Set Bounded Above Has a Supremum §supremum, $N_{A}$ has a supremum.

Clause map. Since $A$ was arbitrary, the clauses bounded and supremum hold for every $B\in\mathcal{M}_{m\times n}(\mathbb{R})$ in place of $A$: for every such $B$, $N_{B}$ is a subset of $\mathbb{R}$ that has a supremum for the partial order $\le$ of $\mathbb{R}$. By Images of Typed Terms: the Set of Values $\{t:u\in D\}$ Is a Set, Finite when $D$ Is Finite, and a Typed Term §symbol, with the data used above for $N_{B}$, $N_{B}$ is a defined set symbol with argument $B$, used properly where $\gamma$ holds, that is, at every $B\in\mathcal{M}_{m\times n}(\mathbb{R})$; $B$ is the only one of the variables there, so none is fixed, and the values $N_{B}$ lie in the set $\mathcal{P}(\mathbb{R})$. So it may stand as the expression $t(u)$ of the clause applied next, with $B$ as its $u$ and $\mathcal{M}_{m\times n}(\mathbb{R})$ as its $a$. By Predicative Formulas for Suprema and Infima, and Maps Defined by Suprema and Infima §maps, with $\mathcal{M}_{m\times n}(\mathbb{R})$ for its $a$, $\mathbb{R}$ with $\le$ for its $p$ with $\preceq$, $B$ for its $u$ and $N_{B}$ for its $t(u)$, there is exactly one map $\nu:\mathcal{M}_{m\times n}(\mathbb{R})\to\mathbb{R}$ with $\nu(B)=\sup N_{B}$ for every $B\in\mathcal{M}_{m\times n}(\mathbb{R})$.