# Uniqueness of $y'=cos(y)$ solutions

Consider the equation $$\begin{cases} \displaystyle y'(x)=\cos\left(y(x)\right)\\ y(0)=0 \end{cases}$$ I've found explicitely $$y$$ and I know this equation has a unique solution. However is there a way to prove unicity of such an $$y$$ without using Cauchy-Lipschitz Theorem ? I've tried to suppose two solutions $$y_1$$ and $$y_2$$ to show $$y_1-y_2=0$$. I only found $$(y_1-y_2)'=-2\sin\left(\frac{y_1+y_2}{2}\right)\sin\left(\frac{y_1-y_2}{2}\right)$$ But it did not help me. Can anyone got an idea to show it this way ?

• If you set $z:=y_1-y_2$ and integrate what you found, using that $z(0)=0$, you should be able to conclude via Gronwall's inequality (integral form). – Giuseppe Negro Jan 24 '19 at 19:38
• @GiuseppeNegro I wonder how you would use it ? Because $\cos\left(y\right)$ does satisfy $\leq y$ ? – Atmos Jan 25 '19 at 17:32

In order to prove the unicity in this particular case let $$U$$ be an open interval around $$0\in{\mathbb R}$$, where $$|y(x)|<{\pi\over2}$$, and consider the auxiliary function $$u(x):=\log{1+\sin\bigl(y(x)\bigr)\over1-\sin\bigl(y(x)\bigr)}\qquad(x\in U)\ .\tag{1}$$ One computes $$u'(x)=\left({1\over1+\sin\bigl(y(x)\bigr)}-{-1\over1-\sin\bigl(y(x)\bigr)}\right)\cos\bigl(y(x)\bigr)y'(x)\equiv2\qquad(x\in U)\ .$$ I think you will accept that this together with $$u(0)=0$$ implies $$u(x)=2x$$ for all $$x\in U$$. From $$(1)$$ we then get $${1+\sin\bigl(y(x)\bigr)\over1-\sin\bigl(y(x)\bigr)}=e^{2x}\qquad(x\in U)\ ,$$ and this leads to $$y(x)=\arcsin\bigl(\tanh x\bigr)\qquad(x\in U)\ .\tag{2}$$ As $$|\tanh x|<1$$ for all $$x\in {\mathbb R}$$ we see that the |RHS| of $$(2)$$ is $$<{\pi\over2}$$ for all $$x\in{\mathbb R}$$, so that we may choose $$U={\mathbb R}$$.
• I found that $u'(x)=-sin(y(x))$ – Atmos Jan 24 '19 at 20:51