Proof of A Priori Bounded Initial Value Problems with Locally Lipschitz Right-Hand Side Have Exactly One Solution on the Whole Interval

We prove (i) and (ii); (iii) and (iv) are treated at the end. By Basic Facts about Intervals of the Real Line (v) and Basic Facts about Intervals of the Real Line (ii), for every $c\in\mathbb{R}$ with $a<c\le b$, $[a,c]$ is an interval containing the two distinct points $a$ and $c$, and $[a,c]\subseteq[a,b]$. $(\mathbb{R}^{n},d_{E})$ is a metric space by $\mathbb{R}^n$ with the Euclidean Distance Is a Complete Metric Space with Coordinatewise Convergence (i), with $d_{E}(u,v)=\lVert u-v\rVert$ by The Euclidean Distance on $\mathbb{R}^n$ (i), and $d$ denotes the product metric on $\mathbb{R}\times\mathbb{R}^{n}$. Computations with real numbers below (sums, products, halving, minima, maxima and absolute values of differences) are carried out in the type of The Real Numbers as a Type (i), with differences, quotients and absolute values read there by Differences, Quotients and Absolute Values of Real Numbers, Read in the Type Real (i), Differences, Quotients and Absolute Values of Real Numbers, Read in the Type Real (ii) and Differences, Quotients and Absolute Values of Real Numbers, Read in the Type Real (iii). Let $F$, $\xi$ and $\rho$ be as in (i).

Step 1: the truncated right-hand side. Let $R=\rho+1$. Since $\rho\ge\lVert\xi\rVert\ge0$ by Properties of the Euclidean Norm on $\mathbb{R}^n$: Square, Distance, Vanishing, Coordinate Bounds, Homogeneity, Triangle Inequalities and Expansion of a Square (i), $R>0$; choose $L_{R}\in\mathbb{R}$ with $L_{R}\ge0$ as in the Lipschitz hypothesis of (i) for this $R$, and let $\pi_{R}:\mathbb{R}^{n}\to\mathbb{R}^{n}$ be the map of Radial Retraction onto a Closed Ball in ℝⁿ and in the Real Matrices (i). Let $P:[a,b]\times\mathbb{R}^{n}\to\mathbb{R}\times\mathbb{R}^{n}$ be the map $(t,z)\mapsto(t,\pi_{R}(z))$ (which exists by Maps and Relations Given by Formulas (ii), with $\mathbb{R}\times\mathbb{R}^{n}$, $[a,b]$ and $\mathbb{R}^{n}$ for its $b$, $c$ and $d$); its values lie in $[a,b]\times\mathbb{R}^{n}$.

$P$ is continuous on $[a,b]\times\mathbb{R}^{n}$. Let $(t_{0},z_{0})\in[a,b]\times\mathbb{R}^{n}$ and let $\varepsilon>0$ be real; let $\delta=\varepsilon/2$. Let $(t,z)\in[a,b]\times\mathbb{R}^{n}$ with $d\bigl((t_{0},z_{0}),(t,z)\bigr)<\delta$. By The Product Metric is a Metric (iii), $|t_{0}-t|<\delta$ and $\lVert z_{0}-z\rVert=d_{E}(z_{0},z)<\delta$. By Radial Retraction onto a Closed Ball in ℝⁿ and in the Real Matrices (iii), $d_{E}\bigl(\pi_{R}(z_{0}),\pi_{R}(z)\bigr)\le2\lVert z_{0}-z\rVert<\varepsilon$, and $|t_{0}-t|<\varepsilon$; by Metric Space (iv) and The Product Metric is a Metric (iii), $d\bigl(P(t,z),P(t_{0},z_{0})\bigr)<\varepsilon$. So $P$ is continuous at $(t_{0},z_{0})$ relative to $[a,b]\times\mathbb{R}^{n}$, and continuous on $[a,b]\times\mathbb{R}^{n}$ by Continuous Map Between Metric Spaces (ii).

Let $G=F\circ P:[a,b]\times\mathbb{R}^{n}\to\mathbb{R}^{n}$, so that $G(t,z)=F(t,\pi_{R}(z))$ (a map by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction (ii), $P$ being a map into $[a,b]\times\mathbb{R}^{n}$ by Functions, Values of a Function, and Functions from One Class to Another (iii), as its values lie there). By Continuity of Identity Maps, Compositions and Reciprocals (ii), with $(\mathbb{R}\times\mathbb{R}^{n},d)$ in place of $(X,d_{X})$ and $(Y,d_{Y})$, $(\mathbb{R}^{n},d_{E})$ in place of $(Z,d_{Z})$, $[a,b]\times\mathbb{R}^{n}$ in place of $A$ and $B$, and $P$ and $F$ in place of $f$ and $g$, $G$ is continuous on $[a,b]\times\mathbb{R}^{n}$. For $t\in[a,b]$ and $z_{1},z_{2}\in\mathbb{R}^{n}$ we have $\lVert\pi_{R}(z_{1})\rVert\le R$ and $\lVert\pi_{R}(z_{2})\rVert\le R$ by Radial Retraction onto a Closed Ball in ℝⁿ and in the Real Matrices (ii), so the choice of $L_{R}$ and Radial Retraction onto a Closed Ball in ℝⁿ and in the Real Matrices (iii) give

$$\lVert G(t,z_{1})-G(t,z_{2})\rVert\le L_{R}\,\lVert\pi_{R}(z_{1})-\pi_{R}(z_{2})\rVert\le2L_{R}\,\lVert z_{1}-z_{2}\rVert ,$$

with $2L_{R}\ge0$. By The Picard–Lindelöf Theorem on a Closed Interval: Existence, Uniqueness and Continuous Dependence for Globally Lipschitz Systems (i), with $G$ and $2L_{R}$ in place of $F$ and $L$, the initial value problem with right-hand side $G$ and initial value $\xi$ has exactly one solution; let $x:[a,b]\to\mathbb{R}^{n}$ be this solution. By Solution of an Initial Value Problem on $[a,c]$ (i), $x$ is differentiable, $x'(t)=G(t,x(t))$ for every $t\in[a,b]$, and $x(a)=\xi$; by Rules for Derivatives of Vector- and Matrix-Valued Maps (i), with $[a,b]$ in place of $I$, $x$ is continuous at every $t\in[a,b]$ relative to $[a,b]$.

Step 2: where $x$ stays in the ball, it solves the original problem. Let $c\in\mathbb{R}$ with $a<c\le b$ be such that $\lVert x(t)\rVert\le R$ for every $t\in[a,c]$. We show that the restriction $y=x|_{[a,c]}:[a,c]\to\mathbb{R}^{n}$ (a map by Domains and Restrictions of Maps (ii), with $y(t)=x(t)$ for $t\in[a,c]$ by Domains and Restrictions of Maps (iii)) is a solution on $[a,c]$ of the initial value problem with right-hand side $F$ and initial value $\xi$; consequently, by the a priori hypothesis of (i), $\lVert x(t)\rVert=\lVert y(t)\rVert\le\rho$ for every $t\in[a,c]$. Let $t\in[a,c]$ and $k\in[n]$. The component map $y_{k}$ of Derivative of a Vector-Valued or Matrix-Valued Map on an Interval (i) is the restriction $x_{k}|_{[a,c]}$ of the component map $x_{k}$ (the two maps $[a,c]\to\mathbb{R}$ have the same values by Domains and Restrictions of Maps (iii), so they are equal by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (iv)); since $x_{k}$ is differentiable at $t$ relative to $[a,b]$ by Derivative of a Vector-Valued or Matrix-Valued Map on an Interval (i), Restriction Stability of Continuity and of the Derivative (ii), with $[a,b]$ and $[a,c]$ in place of $I$ and $J$ and $x_{k}$ in place of $f$, shows that $y_{k}$ is differentiable at $t$ relative to $[a,c]$ with $y_{k}'(t)=x_{k}'(t)$. Hence, by Derivative of a Vector-Valued or Matrix-Valued Map on an Interval (i) and Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations (iii), $y$ is differentiable at $t$ with $y'(t)=x'(t)$. As $\lVert x(t)\rVert\le R$, Radial Retraction onto a Closed Ball in ℝⁿ and in the Real Matrices (ii) gives $\pi_{R}(x(t))=x(t)$, so

$$y'(t)=x'(t)=G\bigl(t,x(t)\bigr)=F\bigl(t,\pi_{R}(x(t))\bigr)=F\bigl(t,y(t)\bigr).$$

Thus $y$ is differentiable (Derivative of a Vector-Valued or Matrix-Valued Map on an Interval (iii)), and $y(a)=x(a)=\xi$; by Solution of an Initial Value Problem on $[a,c]$ (i), $y$ is a solution on $[a,c]$ as claimed.

Step 3: $x$ stays in the ball. Let $S$ be the set of $c\in[a,b]$ with $a<c$ and $\lVert x(t)\rVert\le R$ for every $t\in[a,c]$ (a set by Sets and Maps: Ordinary Notation (iii): the condition on $c$ is predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (i), with $a$, $R$, $x$, the order $\le$ and the strict order $<$ of $\mathbb{R}$ and the map $u\mapsto\lVert u\rVert$ of The Summation Map on Real-Valued Maps over a Finite Set, and the Dot Product, Euclidean Norm and Euclidean Distance as Maps (iii) as parameters).

$S$ is nonempty. By continuity of $x$ at $a$ (Continuous Map Between Metric Spaces (i), with $\varepsilon=1$), choose a real $\delta_{0}>0$ such that every $t\in[a,b]$ with $|a-t|<\delta_{0}$ satisfies $\lVert x(t)-x(a)\rVert<1$. Let $c_{0}$ be the smaller of $a+\delta_{0}/2$ and $b$; then $a<c_{0}\le b$, and every $t\in[a,c_{0}]$ satisfies $|a-t|\le\delta_{0}/2<\delta_{0}$, hence, by Properties of the Euclidean Norm on $\mathbb{R}^n$: Square, Distance, Vanishing, Coordinate Bounds, Homogeneity, Triangle Inequalities and Expansion of a Square (vi),

$$\lVert x(t)\rVert\le\lVert x(a)\rVert+\lVert x(t)-x(a)\rVert<\lVert\xi\rVert+1\le\rho+1=R .$$

So $c_{0}\in S$.

The supremum. $S$ is a subset of $\mathbb{R}$, nonempty, and bounded above by $b$ (Bounds, Least and Greatest Elements, Suprema and Infima for a Partial Order (i)), so it has a supremum $c^{*}=\sup S$ by The Real Numbers Form an Ordered Field in Which Every Nonempty Set Bounded Above Has a Supremum (ii). By Bounds, Least and Greatest Elements, Suprema and Infima for a Partial Order (iv), $c^{*}$ is an upper bound of $S$ and $c^{*}\le b$; as $c_{0}\in S$, $a<c_{0}\le c^{*}\le b$.

$\lVert x(t)\rVert\le\rho$ for every $t\in[a,c^{*})$. Let $a\le t<c^{*}$. By Arbitrary Positive Slack, and Approximation of Suprema and Infima, in the Real Numbers (iv) there is $c\in S$ with $t<c$; then $t\in[a,c]$, and Step 2, applied to $c$, gives $\lVert x(t)\rVert\le\rho$.

$\lVert x(c^{*})\rVert\le\rho$. Let $\varepsilon>0$ be real. By continuity of $x$ at $c^{*}$ (Continuous Map Between Metric Spaces (i)), choose a real $\delta>0$ such that every $t\in[a,b]$ with $|c^{*}-t|<\delta$ satisfies $\lVert x(t)-x(c^{*})\rVert<\varepsilon$. Let $t$ be the larger of $a$ and $c^{*}-\delta/2$; then $a\le t<c^{*}$, as $a<c^{*}$, and $|c^{*}-t|\le\delta/2<\delta$. By the previous paragraph and Properties of the Euclidean Norm on $\mathbb{R}^n$: Square, Distance, Vanishing, Coordinate Bounds, Homogeneity, Triangle Inequalities and Expansion of a Square (vi) and Properties of the Euclidean Norm on $\mathbb{R}^n$: Square, Distance, Vanishing, Coordinate Bounds, Homogeneity, Triangle Inequalities and Expansion of a Square (v),

$$\lVert x(c^{*})\rVert\le\lVert x(t)\rVert+\lVert x(c^{*})-x(t)\rVert<\rho+\varepsilon .$$

As $\varepsilon>0$ was arbitrary, $\lVert x(c^{*})\rVert\le\rho$ by Arbitrary Positive Slack, and Approximation of Suprema and Infima, in the Real Numbers (i). Hence $\lVert x(t)\rVert\le\rho$ for every $t\in[a,c^{*}]$.

$c^{*}=b$. Suppose $c^{*}<b$. By continuity of $x$ at $c^{*}$ with $\varepsilon=1$, choose a real $\delta_{1}>0$ such that every $t\in[a,b]$ with $|c^{*}-t|<\delta_{1}$ satisfies $\lVert x(t)-x(c^{*})\rVert<1$, and let $c_{1}$ be the smaller of $c^{*}+\delta_{1}/2$ and $b$, so that $c^{*}<c_{1}\le b$. Let $t\in[a,c_{1}]$. If $t\le c^{*}$, then $\lVert x(t)\rVert\le\rho<R$. If $c^{*}<t$, then $|c^{*}-t|\le\delta_{1}/2<\delta_{1}$, and by Properties of the Euclidean Norm on $\mathbb{R}^n$: Square, Distance, Vanishing, Coordinate Bounds, Homogeneity, Triangle Inequalities and Expansion of a Square (vi)

$$\lVert x(t)\rVert\le\lVert x(c^{*})\rVert+\lVert x(t)-x(c^{*})\rVert<\rho+1=R .$$

So $c_{1}\in S$, and $c_{1}\le c^{*}$ as $c^{*}$ is an upper bound of $S$, contradicting $c^{*}<c_{1}$. Hence $c^{*}=b$, and $\lVert x(t)\rVert\le\rho$ for every $t\in[a,b]$.

Step 4: existence and the bound. By Step 3, $\lVert x(t)\rVert\le\rho\le R$ for every $t\in[a,b]$, so Step 2 applies with $c=b$: $x=x|_{[a,b]}$ (Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (iii)) is a solution of the initial value problem with right-hand side $F$ and initial value $\xi$, and $\lVert x(t)\rVert\le\rho$ for every $t\in[a,b]$.

Step 5: uniqueness. Let $y$ be a solution of the initial value problem with right-hand side $F$ and initial value $\xi$. By the a priori hypothesis of (i) with $c=b$, $\lVert y(t)\rVert\le\rho\le R$ for every $t\in[a,b]$, so $\pi_{R}(y(t))=y(t)$ by Radial Retraction onto a Closed Ball in ℝⁿ and in the Real Matrices (ii). By Solution of an Initial Value Problem on $[a,c]$ (i), $y$ is differentiable, $y(a)=\xi$, and for every $t\in[a,b]$

$$y'(t)=F\bigl(t,y(t)\bigr)=F\bigl(t,\pi_{R}(y(t))\bigr)=G\bigl(t,y(t)\bigr);$$

so $y$ is a solution of the initial value problem with right-hand side $G$ and initial value $\xi$, by Solution of an Initial Value Problem on $[a,c]$ (i), and $y=x$ by the uniqueness in The Picard–Lindelöf Theorem on a Closed Interval: Existence, Uniqueness and Continuous Dependence for Globally Lipschitz Systems (i). With Step 4 this proves (i); and as the solution of (i) is $x$, Step 4 proves (ii).

Proof of (iii) and (iv). The argument above applies word for word, with $\mathcal{M}_{p\times q}(\mathbb{R})$, $d_{p\times q}$, the operator norm, $\Xi$, the map $\Pi_{R}$ of Radial Retraction onto a Closed Ball in ℝⁿ and in the Real Matrices (i), the entry maps and the indices $i\in[p]$, $j\in[q]$, The Initial Value Problem for a First-Order System of Ordinary Differential Equations (ii) and Solution of an Initial Value Problem on $[a,c]$ (ii) in place of $\mathbb{R}^{n}$, $d_{E}$, the Euclidean norm, $\xi$, $\pi_{R}$, the component maps and the index $k\in[n]$, The Initial Value Problem for a First-Order System of Ordinary Differential Equations (i) and Solution of an Initial Value Problem on $[a,c]$ (i); using that $(\mathcal{M}_{p\times q}(\mathbb{R}),d_{p\times q})$ is a metric space by The Real Matrices with the Operator-Norm Distance Form a Complete Metric Space with Entrywise Convergence (i), with $d_{p\times q}(A,B)=\lVert A-B\rVert$ by The Distance between Real Matrices (i); the operator norm as a map $\mathcal{M}_{p\times q}(\mathbb{R})\to\mathbb{R}$ by The Operator Norm of a Real Matrix (i) in place 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 (iii); Rules for the Operator Norm: Bound, Least Constant, Definiteness, Homogeneity, Triangle Inequality and Products (i), Rules for the Operator Norm: Bound, Least Constant, Definiteness, Homogeneity, Triangle Inequality and Products (vi) and Rules for the Operator Norm: Bound, Least Constant, Definiteness, Homogeneity, Triangle Inequality and Products (v) in place of Properties of the Euclidean Norm on $\mathbb{R}^n$: Square, Distance, Vanishing, Coordinate Bounds, Homogeneity, Triangle Inequalities and Expansion of a Square (i), Properties of the Euclidean Norm on $\mathbb{R}^n$: Square, Distance, Vanishing, Coordinate Bounds, Homogeneity, Triangle Inequalities and Expansion of a Square (vi) and Properties of the Euclidean Norm on $\mathbb{R}^n$: Square, Distance, Vanishing, Coordinate Bounds, Homogeneity, Triangle Inequalities and Expansion of a Square (v); Derivative of a Vector-Valued or Matrix-Valued Map on an Interval (ii) and Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations (iii) in place of Derivative of a Vector-Valued or Matrix-Valued Map on an Interval (i) and Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations (iii); the matrix halves of Radial Retraction onto a Closed Ball in ℝⁿ and in the Real Matrices (ii), Radial Retraction onto a Closed Ball in ℝⁿ and in the Real Matrices (iii) and Rules for Derivatives of Vector- and Matrix-Valued Maps (i); and The Picard–Lindelöf Theorem on a Closed Interval: Existence, Uniqueness and Continuous Dependence for Globally Lipschitz Systems (iii) in place of The Picard–Lindelöf Theorem on a Closed Interval: Existence, Uniqueness and Continuous Dependence for Globally Lipschitz Systems (i).