## Formalized Name Picard-Lindelöf Theorem for Controlled Ordinary Differential Equations ## Formalized Statement Let $n,m \in \mathbb{N}$, let $I \subseteq \mathbb{R}$ be an interval, let $X \subseteq \mathbb{R}^n$ and $U \subseteq \mathbb{R}^m$ be open sets, and let $f: X \times U \to \mathbb{R}^n$ be continuous. Assume that $f$ is locally Lipschitz in the state variable uniformly for controls in compact subsets of $U$: for every compact set $K_X \subset X$ and every compact set $K_U \subset U$, there exists a constant $L = L(K_X,K_U) \geq 0$ such that \begin{align*} |f(x,u)-f(y,u)| \leq L|x-y| \end{align*} for all $x,y \in K_X$ and all $u \in K_U$. Let $u: I \to U$ be Lebesgue measurable with respect to the restriction of $\mathcal{L}^1$ to $I$, and assume that for every compact interval $K \subseteq I$, compact as a subset of $\mathbb{R}$, there exists a compact set $C_K \subset U$ such that $u(t) \in C_K$ for $\mathcal{L}^1$-a.e. $t \in K$. If $t_0 \in I$ and $x_0 \in X$, then there exist an interval $J \subseteq I$ containing $t_0$ as a relative interval in $I$ and a locally absolutely continuous map $x: J \to X$ such that \begin{align*} x(t_0)=x_0 \end{align*} and \begin{align*} \dot{x}(t)=f(x(t),u(t)) \end{align*} for $\mathcal{L}^1$-a.e. $t \in J$. Moreover, this solution is unique on overlaps: if $L \subseteq I$ is an interval containing $t_0$ and $y: L \to X$ is another locally absolutely continuous solution with $y(t_0)=x_0$, then \begin{align*} x(t)=y(t) \end{align*} for all $t \in J \cap L$. Finally, there is a unique maximal solution $x_{\max}: J_{\max} \to X$, where $J_{\max} \subseteq I$ is an interval containing $t_0$, such that every locally absolutely continuous solution $y: L \to X$ with initial condition $y(t_0)=x_0$ satisfies $L \subseteq J_{\max}$ and $y=x_{\max}|_L$. ## Proof [proofplan] We prove local existence by converting the controlled differential equation into an integral equation and applying the Picard contraction argument on a small relative time interval around $t_0$. The compact essential range hypothesis for the measurable control gives both a finite bound for $f$ and a uniform Lipschitz constant in the state variable on the relevant compact state-control rectangle. The fixed point is locally absolutely continuous and satisfies the ODE almost everywhere by the fundamental theorem for absolutely continuous functions. Uniqueness follows from the same local Lipschitz estimate and Gronwall's inequality on compact subintervals. The maximal solution is then obtained by taking the union of all compatible local solutions, with compatibility guaranteed by overlap uniqueness. [/proofplan] [step:Choose compact state and control sets on a small relative time interval] Because $X \subseteq \mathbb{R}^n$ is open and $x_0 \in X$, choose $r>0$ such that the closed Euclidean ball \begin{align*} K_X := \overline{B}(x_0,r) \end{align*} is contained in $X$. Since $I$ is an interval and $t_0 \in I$, choose $a>0$ such that \begin{align*} K_I := I \cap [t_0-a,t_0+a] \end{align*} is a compact interval as a subset of $\mathbb{R}$ and contains $t_0$. This is possible by taking $a$ small enough that the intersection is a closed bounded interval in $\mathbb{R}$, allowing the one-sided cases when $t_0$ is an endpoint of $I$. By the compact essential range hypothesis applied to $K_I$, there exists a compact set $K_U \subset U$ such that $u(t) \in K_U$ for $\mathcal{L}^1$-a.e. $t \in K_I$. Let $N \subset K_I$ be a Borel null set such that $u(t) \in K_U$ for every $t \in K_I \setminus N$. Since $f$ is continuous and $K_X \times K_U$ is compact, define \begin{align*} M := \max_{(z,v)\in K_X \times K_U} |f(z,v)|. \end{align*} Then $M<\infty$. By the uniform local Lipschitz hypothesis, there exists $L \geq 0$ such that \begin{align*} |f(z,v)-f(w,v)| \leq L|z-w| \end{align*} for all $z,w \in K_X$ and all $v \in K_U$. Choose $\delta \in (0,a]$ such that \begin{align*} \delta M \leq r \end{align*} and \begin{align*} \delta L < 1, \end{align*} where the second inequality is automatic after decreasing $\delta$ if $L>0$, and imposes no restriction if $L=0$. Define the relative compact interval \begin{align*} J_0 := I \cap [t_0-\delta,t_0+\delta]. \end{align*} This definition includes the one-sided cases where $t_0$ is an endpoint of $I$. [/step] [step:Build a contraction on curves staying in the compact state ball] Let $\mathcal{C}$ be the set of continuous maps $\gamma: J_0 \to K_X$, equipped with the metric \begin{align*} d_{\mathcal{C}}(\gamma,\eta) := \sup_{t \in J_0} |\gamma(t)-\eta(t)|. \end{align*} Since $K_X$ is closed in the complete metric space $\mathbb{R}^n$, the space $\mathcal{C}$ is complete with this metric. It is nonempty because the constant map $J_0 \to K_X$ given by $t \mapsto x_0$ belongs to $\mathcal{C}$. For every $\gamma \in \mathcal{C}$, define the measurable map \begin{align*} G_\gamma: J_0 \to \mathbb{R}^n, \qquad s \mapsto f(\gamma(s),u(s)). \end{align*} On $J_0 \setminus N$ we have $\gamma(s) \in K_X$ and $u(s) \in K_U$, hence $|G_\gamma(s)| \leq M$. Thus $G_\gamma \in L^1(J_0;\mathbb{R}^n)$. The indefinite integral of an $L^1$ map on a compact interval is absolutely continuous, hence continuous. Therefore the map $t \mapsto x_0+\int_{t_0}^{t}G_\gamma(s)\,d\mathcal{L}^1(s)$ belongs to $C(J_0;\mathbb{R}^n)$. We use the oriented integral notation \begin{align*} \int_{t_0}^{t} G_\gamma(s)\,d\mathcal{L}^1(s) \end{align*} to mean the integral over $[t_0,t]$ when $t \geq t_0$, and the negative of the integral over $[t,t_0]$ when $t \leq t_0$. Define the Picard operator \begin{align*} \Phi:\mathcal{C}\to C(J_0;\mathbb{R}^n), \qquad (\Phi\gamma)(t) := x_0+\int_{t_0}^{t} f(\gamma(s),u(s))\,d\mathcal{L}^1(s). \end{align*} For every $t \in J_0$, \begin{align*} |(\Phi\gamma)(t)-x_0| \leq \int_{\min\{t,t_0\}}^{\max\{t,t_0\}} |f(\gamma(s),u(s))|\,d\mathcal{L}^1(s) \leq M|t-t_0| \leq M\delta \leq r. \end{align*} Hence $\Phi\gamma$ takes values in $K_X$, so $\Phi$ maps $\mathcal{C}$ into itself. If $\gamma,\eta \in \mathcal{C}$ and $t \in J_0$, then, using the Lipschitz estimate outside the null set $N$, \begin{align*} |(\Phi\gamma)(t)-(\Phi\eta)(t)| \leq \int_{\min\{t,t_0\}}^{\max\{t,t_0\}} |f(\gamma(s),u(s))-f(\eta(s),u(s))|\,d\mathcal{L}^1(s). \end{align*} Therefore \begin{align*} |(\Phi\gamma)(t)-(\Phi\eta)(t)| \leq L\int_{\min\{t,t_0\}}^{\max\{t,t_0\}} |\gamma(s)-\eta(s)|\,d\mathcal{L}^1(s) \leq L\delta d_{\mathcal{C}}(\gamma,\eta). \end{align*} Taking the supremum over $t \in J_0$ gives \begin{align*} d_{\mathcal{C}}(\Phi\gamma,\Phi\eta) \leq L\delta d_{\mathcal{C}}(\gamma,\eta). \end{align*} Since $L\delta<1$, $\Phi$ is a contraction. We use the Banach fixed-point theorem in the following precise form: every contraction self-map of a nonempty complete metric space has a unique fixed point. The hypotheses are satisfied because $\mathcal{C}$ is nonempty and complete and because $\Phi:\mathcal{C}\to\mathcal{C}$ has contraction constant $L\delta<1$. Hence there exists a unique $x \in \mathcal{C}$ such that $\Phi x=x$. [guided] The goal is to solve the ODE by solving its integral form. For a candidate curve $\gamma: J_0 \to K_X$, the right-hand side \begin{align*} s \mapsto f(\gamma(s),u(s)) \end{align*} is measurable because $\gamma$ is continuous, $u$ is measurable, and $f$ is continuous. On the full-measure set $J_0 \setminus N$, the curve value lies in $K_X$ and the control value lies in $K_U$, so the compactness bound gives \begin{align*} |f(\gamma(s),u(s))| \leq M. \end{align*} Thus the map is integrable on $J_0$ with respect to $\mathcal{L}^1$. We define the Picard operator \begin{align*} \Phi:\mathcal{C}\to C(J_0;\mathbb{R}^n), \qquad (\Phi\gamma)(t) := x_0+\int_{t_0}^{t} f(\gamma(s),u(s))\,d\mathcal{L}^1(s). \end{align*} The oriented integral is only a compact way to treat both sides of $t_0$ at once: for $t \geq t_0$ it is the usual integral over $[t_0,t]$, while for $t \leq t_0$ it is minus the integral over $[t,t_0]$. Because $s \mapsto f(\gamma(s),u(s))$ belongs to $L^1(J_0;\mathbb{R}^n)$, the indefinite integral defining $\Phi\gamma$ is absolutely continuous on $J_0$ and therefore continuous. Thus $\Phi\gamma$ is at least an element of $C(J_0;\mathbb{R}^n)$. We first check that $\Phi$ preserves the closed ball constraint. For every $t \in J_0$, \begin{align*} |(\Phi\gamma)(t)-x_0| \leq \int_{\min\{t,t_0\}}^{\max\{t,t_0\}} |f(\gamma(s),u(s))|\,d\mathcal{L}^1(s). \end{align*} The integrand is bounded by $M$ outside the null set $N$, so \begin{align*} |(\Phi\gamma)(t)-x_0| \leq M|t-t_0| \leq M\delta \leq r. \end{align*} Hence $(\Phi\gamma)(t) \in \overline{B}(x_0,r)=K_X$ for every $t \in J_0$, so $\Phi\gamma \in \mathcal{C}$. We next check the contraction estimate. If $\gamma,\eta \in \mathcal{C}$, then for $\mathcal{L}^1$-a.e. $s \in J_0$ the points $\gamma(s)$ and $\eta(s)$ lie in $K_X$, while $u(s)$ lies in $K_U$. The uniform Lipschitz condition therefore gives \begin{align*} |f(\gamma(s),u(s))-f(\eta(s),u(s))| \leq L|\gamma(s)-\eta(s)|. \end{align*} Integrating this estimate between $t_0$ and $t$ gives \begin{align*} |(\Phi\gamma)(t)-(\Phi\eta)(t)| \leq L\int_{\min\{t,t_0\}}^{\max\{t,t_0\}} |\gamma(s)-\eta(s)|\,d\mathcal{L}^1(s). \end{align*} Since $|\gamma(s)-\eta(s)| \leq d_{\mathcal{C}}(\gamma,\eta)$ for all $s \in J_0$, we obtain \begin{align*} |(\Phi\gamma)(t)-(\Phi\eta)(t)| \leq L\delta d_{\mathcal{C}}(\gamma,\eta). \end{align*} Taking the supremum over $t \in J_0$ yields \begin{align*} d_{\mathcal{C}}(\Phi\gamma,\Phi\eta) \leq L\delta d_{\mathcal{C}}(\gamma,\eta). \end{align*} The constant $L\delta$ is strictly less than $1$ by construction. We now apply the Banach fixed-point theorem: a contraction self-map of a nonempty complete metric space has exactly one fixed point. The metric space $\mathcal{C}$ is nonempty because it contains the constant curve $t \mapsto x_0$. It is complete because a uniformly convergent sequence of continuous maps $J_0 \to K_X$ has a continuous limit $J_0 \to K_X$, using that $K_X$ is closed in $\mathbb{R}^n$. The map $\Phi$ is a self-map with contraction constant $L\delta<1$. Therefore the theorem applies and gives a unique fixed point $x \in \mathcal{C}$ satisfying $\Phi x=x$. [/guided] [/step] [step:Convert the fixed point into a locally absolutely continuous solution] The fixed point identity says that for every $t \in J_0$, \begin{align*} x(t)=x_0+\int_{t_0}^{t} f(x(s),u(s))\,d\mathcal{L}^1(s). \end{align*} The map \begin{align*} G_x:J_0\to\mathbb{R}^n, \qquad s\mapsto f(x(s),u(s)) \end{align*} belongs to $L^1(J_0;\mathbb{R}^n)$, because $|G_x(s)|\leq M$ for $\mathcal{L}^1$-a.e. $s \in J_0$. We use the fundamental theorem for absolutely continuous functions in Lebesgue integral form: if $G \in L^1(J_0;\mathbb{R}^n)$ and $F(t)=c+\int_{t_0}^{t}G(s)\,d\mathcal{L}^1(s)$, then $F$ is absolutely continuous and $\dot F(t)=G(t)$ for $\mathcal{L}^1$-a.e. $t$. Applying this result to $G_x$ and $c=x_0$, the map $x:J_0\to X$ is absolutely continuous and satisfies \begin{align*} \dot{x}(t)=G_x(t)=f(x(t),u(t)) \end{align*} for $\mathcal{L}^1$-a.e. $t \in J_0$. Also, evaluating the integral identity at $t=t_0$ gives $x(t_0)=x_0$. Thus $x:J_0\to X$ is a local solution. [/step] [step:Prove uniqueness on every common interval by a local Gronwall estimate] Let $J \subseteq I$ and $L_0 \subseteq I$ be intervals containing $t_0$, and let \begin{align*} x:J\to X, \qquad y:L_0\to X \end{align*} be locally absolutely continuous solutions with $x(t_0)=y(t_0)=x_0$. We prove that $x=y$ on $J\cap L_0$. Fix $t \in J\cap L_0$ with $t \geq t_0$; the case $t \leq t_0$ is identical after reversing the interval orientation. Define the compact interval \begin{align*} K_t := [t_0,t] \subseteq J\cap L_0. \end{align*} The images $x(K_t)$ and $y(K_t)$ are compact subsets of $X$. Hence \begin{align*} K_{X,t} := x(K_t)\cup y(K_t) \end{align*} is compact in $X$. By the compact essential range hypothesis, there is a compact set $K_{U,t} \subset U$ such that $u(s) \in K_{U,t}$ for $\mathcal{L}^1$-a.e. $s \in K_t$. By the uniform local Lipschitz hypothesis, choose $L_t \geq 0$ such that \begin{align*} |f(z,v)-f(w,v)| \leq L_t |z-w| \end{align*} for all $z,w \in K_{X,t}$ and all $v \in K_{U,t}$. Since $x$ and $y$ are locally absolutely continuous on their domains, their restrictions to the compact interval $K_t$ are absolutely continuous. The fundamental theorem for absolutely continuous functions therefore gives the integral identities for both curves on $K_t$. Subtracting those identities, for every $\tau \in K_t$ we have \begin{align*} x(\tau)-y(\tau)=\int_{t_0}^{\tau} \bigl(f(x(s),u(s))-f(y(s),u(s))\bigr)\,d\mathcal{L}^1(s). \end{align*} Therefore \begin{align*} |x(\tau)-y(\tau)| \leq L_t\int_{t_0}^{\tau} |x(s)-y(s)|\,d\mathcal{L}^1(s). \end{align*} We use Gronwall's inequality in the zero-initial-term form: if a nonnegative continuous function $\psi:[t_0,t]\to[0,\infty)$ satisfies $\psi(\tau)\leq A\int_{t_0}^{\tau}\psi(s)\,d\mathcal{L}^1(s)$ for every $\tau\in[t_0,t]$ and some $A\geq0$, then $\psi\equiv0$. Applying this result to the nonnegative continuous function \begin{align*} \psi:K_t\to[0,\infty), \qquad \psi(\tau):=|x(\tau)-y(\tau)|, \end{align*} with $A=L_t$, gives $\psi(\tau)=0$ for every $\tau \in K_t$. In particular, $x(t)=y(t)$. Since $t \in J\cap L_0$ was arbitrary on the right of $t_0$, and the same argument applies on the left of $t_0$, the solutions agree on all of $J\cap L_0$. [guided] The only possible source of nonuniqueness is that two curves might separate after starting from the same point. We rule this out on each compact time interval by obtaining an integral inequality for their distance. Fix $t \in J\cap L_0$ with $t \geq t_0$ and set \begin{align*} K_t := [t_0,t]. \end{align*} Because $x$ and $y$ are continuous, the sets $x(K_t)$ and $y(K_t)$ are compact subsets of $X$. Their union \begin{align*} K_{X,t} := x(K_t)\cup y(K_t) \end{align*} is therefore compact. The control may not have a compact pointwise range on $K_t$, but the hypothesis gives exactly what is needed: there is a compact set $K_{U,t} \subset U$ such that $u(s) \in K_{U,t}$ for $\mathcal{L}^1$-a.e. $s \in K_t$. Now the uniform local Lipschitz assumption applies on $K_{X,t} \times K_{U,t}$. Thus there exists $L_t \geq 0$ such that \begin{align*} |f(z,v)-f(w,v)| \leq L_t|z-w| \end{align*} for all $z,w \in K_{X,t}$ and all $v \in K_{U,t}$. Since both curves are locally absolutely continuous solutions, their restrictions to the compact interval $K_t$ are absolutely continuous. The fundamental theorem for absolutely continuous functions applies to the derivatives $s\mapsto f(x(s),u(s))$ and $s\mapsto f(y(s),u(s))$, which are integrable on $K_t$ because the curves have compact images and the control has compact essential range there. Hence their integral equations on $K_t$ are \begin{align*} x(\tau)=x_0+\int_{t_0}^{\tau} f(x(s),u(s))\,d\mathcal{L}^1(s) \end{align*} and \begin{align*} y(\tau)=x_0+\int_{t_0}^{\tau} f(y(s),u(s))\,d\mathcal{L}^1(s). \end{align*} Subtracting these two identities gives \begin{align*} x(\tau)-y(\tau)=\int_{t_0}^{\tau} \bigl(f(x(s),u(s))-f(y(s),u(s))\bigr)\,d\mathcal{L}^1(s). \end{align*} Taking Euclidean norms and applying the Lipschitz estimate for $\mathcal{L}^1$-a.e. $s \in K_t$ yields \begin{align*} |x(\tau)-y(\tau)| \leq L_t\int_{t_0}^{\tau} |x(s)-y(s)|\,d\mathcal{L}^1(s). \end{align*} Define \begin{align*} \psi:K_t\to[0,\infty), \qquad \psi(\tau):=|x(\tau)-y(\tau)|. \end{align*} The function $\psi$ is continuous and satisfies \begin{align*} \psi(\tau) \leq L_t\int_{t_0}^{\tau} \psi(s)\,d\mathcal{L}^1(s). \end{align*} The zero-initial-term form of Gronwall's inequality says that a nonnegative continuous function satisfying $\psi(\tau)\leq A\int_{t_0}^{\tau}\psi(s)\,d\mathcal{L}^1(s)$ for all $\tau$ must vanish identically. Its hypotheses hold here with $A=L_t$: $\psi$ is nonnegative and continuous, and the displayed integral inequality holds for every $\tau\in K_t$. Therefore $\psi(\tau)=0$ for every $\tau \in K_t$. Hence $x(\tau)=y(\tau)$ throughout $[t_0,t]$, and in particular $x(t)=y(t)$. If $t \leq t_0$, the same proof is applied on the compact interval $[t,t_0]$, integrating from $t$ up to $t_0$ after subtracting the two integral equations. Thus the two solutions agree on both sides of $t_0$, hence on all of $J\cap L_0$. [/guided] [/step] [step:Construct the maximal solution by taking the union of compatible solutions] Let $\mathcal{S}$ be the collection of all pairs $(J_\alpha,x_\alpha)$ such that $J_\alpha \subseteq I$ is an interval containing $t_0$ and \begin{align*} x_\alpha:J_\alpha\to X \end{align*} is a locally absolutely continuous solution with $x_\alpha(t_0)=x_0$. The previous local existence step shows that $\mathcal{S}$ is nonempty. Define \begin{align*} J_{\max}:=\bigcup_{(J_\alpha,x_\alpha)\in\mathcal{S}} J_\alpha. \end{align*} Since every $J_\alpha$ is an interval containing $t_0$, the union $J_{\max}$ is also an interval containing $t_0$ and contained in $I$. For $t \in J_{\max}$, choose any $(J_\alpha,x_\alpha)\in\mathcal{S}$ with $t \in J_\alpha$, and define \begin{align*} x_{\max}(t):=x_\alpha(t). \end{align*} This definition is independent of the choice of $\alpha$: if $t \in J_\alpha\cap J_\beta$, then the overlap uniqueness already proved gives $x_\alpha(t)=x_\beta(t)$. It remains to check that $x_{\max}$ is itself a locally absolutely continuous solution. Let $K \subseteq J_{\max}$ be a compact interval, and write its endpoints as $p\leq q$. Since $p,q\in J_{\max}$, choose solutions $(J_p,x_p)$ and $(J_q,x_q)$ in $\mathcal{S}$ such that $p\in J_p$ and $q\in J_q$. Both intervals $J_p$ and $J_q$ contain $t_0$. We first verify that $K\subseteq J_p\cup J_q$. If $q\leq t_0$, then $p,q\in J_p$ because $q\in[p,t_0]$ and $J_p$ is an interval containing $p$ and $t_0$, so $K=[p,q]\subseteq J_p$. If $t_0\leq p$, then $p,q\in J_q$ because $p\in[t_0,q]$ and $J_q$ is an interval containing $t_0$ and $q$, so $K\subseteq J_q$. If $p\leq t_0\leq q$, then $[p,t_0]\subseteq J_p$ and $[t_0,q]\subseteq J_q$, hence $K\subseteq J_p\cup J_q$. In all cases $J_p\cup J_q$ is an interval, because $J_p\cap J_q$ contains $t_0$. Define \begin{align*} z:J_p\cup J_q\to X \end{align*} by $z(t)=x_p(t)$ for $t\in J_p$ and $z(t)=x_q(t)$ for $t\in J_q$. This is well-defined because overlap uniqueness gives $x_p=x_q$ on $J_p\cap J_q$. To prove that $z$ is locally absolutely continuous, let $H\subseteq J_p\cup J_q$ be a compact interval. Since $J_p$ and $J_q$ are intervals with nonempty intersection and $H\subseteq J_p\cup J_q$, the compact interval $H$ is covered by one or two compact subintervals $H_p\subseteq H\cap J_p$ and $H_q\subseteq H\cap J_q$, with any nonempty overlap again an interval. On the overlap the two definitions agree by overlap uniqueness. Since $x_p$ and $x_q$ are locally absolutely continuous, their restrictions to $H_p$ and $H_q$ are absolutely continuous. The finite pasting criterion for absolutely continuous functions therefore gives that $z|_H$ is absolutely continuous. Thus $z$ is locally absolutely continuous. The differential equation also passes to the pasted map. On $H\cap J_p$, the equality $\dot z(t)=f(z(t),u(t))$ holds for $\mathcal{L}^1$-a.e. $t$ because $z=x_p$ there. On $H\cap J_q$, the same equality holds for $\mathcal{L}^1$-a.e. $t$ because $z=x_q$ there. The exceptional set is the union of two $\mathcal{L}^1$-null sets, hence is null. Therefore $z$ is a locally absolutely continuous solution on $J_p\cup J_q$. Since $K\subseteq J_p\cup J_q$ and $x_{\max}|_K=z|_K$, the restriction $x_{\max}|_K$ is absolutely continuous and satisfies \begin{align*} \dot{x}_{\max}(t)=f(x_{\max}(t),u(t)) \end{align*} for $\mathcal{L}^1$-a.e. $t \in K$. Since $K$ was arbitrary, $x_{\max}:J_{\max}\to X$ is locally absolutely continuous and solves the controlled ODE. [guided] The union definition of $x_{\max}$ is pointwise, so the remaining issue is not well-definedness but regularity: a function defined by taking many local solutions must still be locally absolutely continuous on every compact subinterval. Fix a compact interval $K\subseteq J_{\max}$ and write $K=[p,q]$ with $p\leq q$. Because $p$ and $q$ lie in the union $J_{\max}$, there are solutions $(J_p,x_p)$ and $(J_q,x_q)$ in $\mathcal{S}$ such that $p\in J_p$ and $q\in J_q$. Both $J_p$ and $J_q$ contain the initial time $t_0$. Why do these two endpoint solutions cover all of $K$? This uses the interval property. If $q\leq t_0$, then the interval $J_p$ contains both $p$ and $t_0$, so it contains every point between them, including all of $[p,q]$. If $t_0\leq p$, then $J_q$ contains both $t_0$ and $q$, so it contains all of $[p,q]$. If $p\leq t_0\leq q$, then $J_p$ contains $[p,t_0]$ and $J_q$ contains $[t_0,q]$. Hence in every case \begin{align*} K\subseteq J_p\cup J_q. \end{align*} Moreover $J_p\cup J_q$ is an interval because $J_p\cap J_q$ contains $t_0$. Define the pasted map \begin{align*} z:J_p\cup J_q\to X \end{align*} by setting $z(t)=x_p(t)$ on $J_p$ and $z(t)=x_q(t)$ on $J_q$. This definition is consistent: on $J_p\cap J_q$, both $x_p$ and $x_q$ are solutions with the same initial condition, so the overlap uniqueness already proved gives $x_p(t)=x_q(t)$ for every $t\in J_p\cap J_q$. Now we check the two properties required of a solution. First, $z$ is locally absolutely continuous. Let $H\subseteq J_p\cup J_q$ be a compact interval. Since $J_p$ and $J_q$ are intervals with common point $t_0$ and $H\subseteq J_p\cup J_q$, the interval $H$ is covered by one or two compact subintervals $H_p\subseteq H\cap J_p$ and $H_q\subseteq H\cap J_q$. If both pieces are present, their overlap is either empty, a common endpoint, or an interval; wherever both formulas are defined, they agree by overlap uniqueness. Since $x_p$ and $x_q$ are locally absolutely continuous, their restrictions to $H_p$ and $H_q$ are absolutely continuous. The finite pasting criterion for absolutely continuous functions then gives that $z|_H$ is absolutely continuous. Since $H$ was arbitrary, $z$ is locally absolutely continuous. Second, $z$ satisfies the differential equation almost everywhere. On the part of $H$ lying in $J_p$, we have $z=x_p$, so \begin{align*} \dot z(t)=f(z(t),u(t)) \end{align*} for $\mathcal{L}^1$-a.e. $t\in H\cap J_p$. On the part of $H$ lying in $J_q$, we have $z=x_q$, so the same equality holds for $\mathcal{L}^1$-a.e. $t\in H\cap J_q$. The union of the two exceptional null sets is still a null set, so the equation holds for $\mathcal{L}^1$-a.e. $t\in H$. Thus $z$ is a solution on $J_p\cup J_q$. Finally, $x_{\max}$ agrees with $z$ on $K$: for each $t\in K$, the value $x_{\max}(t)$ is defined using some local solution through $t$, and overlap uniqueness identifies that value with the value of the pasted solution $z(t)$ on the interval $J_p\cup J_q$ containing $K$. Therefore $x_{\max}|_K$ is absolutely continuous and satisfies \begin{align*} \dot{x}_{\max}(t)=f(x_{\max}(t),u(t)) \end{align*} for $\mathcal{L}^1$-a.e. $t\in K$. Since every compact interval $K\subseteq J_{\max}$ has this property, $x_{\max}$ is locally absolutely continuous and solves the controlled ODE on $J_{\max}$. [/guided] Finally, if $y:L\to X$ is any other solution with $y(t_0)=x_0$, then $(L,y)\in\mathcal{S}$, so $L\subseteq J_{\max}$ by definition of the union. The overlap uniqueness result gives \begin{align*} y(t)=x_{\max}(t) \end{align*} for every $t \in L$. Thus every solution is the restriction of $x_{\max}$. [/step] [step:Verify uniqueness of the maximal solution] Suppose \begin{align*} \tilde{x}_{\max}:\tilde{J}_{\max}\to X \end{align*} is another maximal solution with the same initial condition. Since $x_{\max}:J_{\max}\to X$ is a solution, maximality of $\tilde{x}_{\max}$ gives $J_{\max}\subseteq \tilde{J}_{\max}$ and \begin{align*} x_{\max}=\tilde{x}_{\max}|_{J_{\max}}. \end{align*} Conversely, since $\tilde{x}_{\max}$ is a solution, maximality of $x_{\max}$ gives $\tilde{J}_{\max}\subseteq J_{\max}$ and \begin{align*} \tilde{x}_{\max}=x_{\max}|_{\tilde{J}_{\max}}. \end{align*} Therefore $J_{\max}=\tilde{J}_{\max}$ and $x_{\max}=\tilde{x}_{\max}$ on this common interval. This proves the existence and uniqueness of the maximal solution and completes the proof. [/step]