In the most general context, the Picard-Lindelöf theorem (aka Cauchy-Lipschitz in French) asserts the existence of a maximal solution for $\dot{x}(t) = f(t,x(t))$, i.e. of a solution $x(t)$ defined on a interval $I$ such that there exist no other solution whose restriction to $I$ coincide with $x$. The usual proofs of this (when $f$ is such that there is no local unicity) use Zorn's lemma, or some other weaker form of choice. But is this result actually not provable in ZF?
$\begingroup$
$\endgroup$
2
-
2$\begingroup$ I though the ODE theorem for when $f$ is such that there is no local unicity, was the $\hspace{.5 in}$ en.wikipedia.org/wiki/Peano_existence_theorem (in English). $\endgroup$– user5810Commented Nov 12, 2012 at 19:34
-
1$\begingroup$ The Cauchy-Lipschitz theorem in french or in any other language is dealing with the case where $f$ is locally Lipschitz continuous with respect to $x$, i.e. satisfies an estimate of type $$ \vert f(t,x_1)-f(t,x_2)\vert\le \alpha(t) \vert x_1-x_2\vert, $$ with $\alpha \in L^1_{loc}$. In that case, local uniqueness occurs for the ODE. $\endgroup$– BazinCommented Nov 12, 2012 at 21:20
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
3
At least for scalar equations $\dot x(t)=f(t,x(t))$, that is with a nonlinearity $f\in C^0(\Omega,\mathbb{R})$, defined on an open set $\Omega\subset \mathbb{R}^2$, the Zorn's lemma is not necessary: the order structure of $\mathbb{R}$ allows to select a preferred solution (actually, two)
Any IVP admits an upper and a lower solution, whose domains are maximal intervals. For $(t_0,x_0)\in\Omega$, define, for $t\in\mathbb{R}$ $$x ^ * (t):=\sup\big\{x(t)\, : x\in C^1(\mathrm{co}(t_0,t),\, \mathbb{R}),\, \mathrm{graph}(x)\subset\Omega, x(t_0)=x_0, \dot x(s)=f(s,x(s)) \big\}\, ,$$ (where of course $\sup\emptyset=-\infty$). Define $\mathrm{dom}(x ^ *)$ to be the connected component of $t_0$ in the set $\{ t: x ^ *(t) \in\mathbb{R} \}$. Then, $x ^ *$ is a solution of the ODE with IVC $x(t_0)=x_0$, maximally defined on the interval $\mathrm{dom}(x ^ *)$.
answered Nov 12, 2012 at 21:46
-
$\begingroup$ As to the case of systems, that is $\Omega\subset\mathbb{R}\times\mathbb{R}^n$ and $f\in C^0(\Omega,\mathbb{R}^n)$, it seems to me that the same construction can be used, using the lexicographic order on $\mathbb{R}^n$. $\endgroup$ Commented Jan 23, 2013 at 14:35
-
$\begingroup$ A similar proof can be found in the paper of Wolfgang Walter American Math Monthly vol 78 1971 pages 170-173 . $\endgroup$ Commented Jan 23, 2013 at 19:19
-
1$\begingroup$ Actually, one should go and see the original proof of the theorem, by Giuseppe Peano. No surprise if we found it's the best proof. $\endgroup$ Commented Jan 23, 2013 at 19:33