I'm trying to prove that, under certain conditions, a damped harmonic oscillator that starts on one side of the equilibrium remains on that side of the equilibrium. More precisely, consider the following system
$$x(t)' = v(t)$$ $$v(t)' = -kx(t)-cv(t)$$
for constants $k$ and $c$ such that $c^2 - 4k \geq 0$ (the system is critically or overdamped). Assume that the initial position $x_0$ and initial velocity $v_0$ satisfy $x_0 \geq 0$ and $-v_0 \leq x_0\frac{c}{2\sqrt{k}}$. Now prove that for all time, $x \geq 0$.
I believe that this can be done by examining the solution to this system. However, I'm trying to prove this property using barrier certificates, a concept similar to Lyapunov functions. In particular, I'm looking for a function $B(x,v)$ such that
- $B(x,v) > 0$ for all $x < 0$
- $\frac{dB(x,v)}{dt} \leq 0$
The existence of such a function guarantees that if the system starts in a state where $B(x,v)$ is non-positive, then $x$ will never be less than 0. This function is called a barrier certificate.