Given a system of ODEs, $$x'=y$$ $$y'=x-x^3-y$$ $$x(0)=x_0$$ $$y(0)=y_0,$$ also given a set $S=\{(x,y):V(x,y)\le k, x>0\}$, $V(x,y)=-\frac{x^2}{2}+\frac{x^4}{4}+\frac{y^2}{2}$, where $-\frac{1}{4}<k<0$, it is needed to be shown that $S$ is compact and positively invariant, and that if $(x_0, y_0)\in S$ then $\lim\limits_{t\to\infty} (x(t), y(t))=(1,0).$
My attempt:
(i) Compactness: Consider $-\frac{1}{4}\le \frac{(x^2-1)^2+2y^2-1}{4}\le k$. Also, $S$ is closed. Therefore, $S$ is a compact set.
(ii) Positive invariance: I think we should use LaSalle's Invariance Principle in this case. Let $E:=\{(x,y)\in S: \dot{V}=0\}=\{(x,0)\}$. Also, consider $V(x, 0) = -\frac{x^2}{2}+\frac{x^4}{4}=-\frac{1}{4} < k$, which implies that $x=1$, $V^{-1}(-\frac{1}{4})=\{(x,0)\in S: V(x,y)=-\frac{1}{4}\}$. Hence, $\omega((x_0, y_0))\subseteq E\cup V^{-1}(-\frac{1}{4})=\{(1,0)\}$.
(iii) It follows from (ii) that $\forall \vec{x_0} \in \Omega$, $\psi_t(\vec{x_0})\to (1,0)$ as $t\to\infty$.
Please let me know if this is correct. I'm concerned about the choice of $-\frac{1}{4}$ - it seems rather arbitrary to me. Also, for the positive invariance, I'm not completely sure that I provided enough details to show it.
Let $f(x,y):=\begin{bmatrix} y \\ x-x^3-y \end{bmatrix}$
A corollary to the Poincaré-Bendixson Theorem states:
One can check that the divergence of $f$, namely $\nabla\cdot f(x,y)=−1<0$ does not change sign on $S$, thus the system has no periodic solutions, hence it must have an equilibrium point. Now, since $\dot{V}=-y^2\le 0$, $y=0$. We can substitute $y=0$ into the system and get that $x-x^3=0$. Since $x>0$, $x=1$. In addition, it can be checked that $(1,0)$ is a center point of the system, thus it is stable, and thus a trajectory $\psi_t(\vec{x_0})$ must converge to $(1,0)$.