Stability

Stream: new members

[Parivash]

Hi,
I have a question. I have a system of ODEs like this one $\frac{dx1}{dt} = 16*x2 - x1^2 - x1*x2 - 1.5*x1$ & $\frac{dx2}{dt}= x1^2 - 8*x2$ in which $\frac{dx1}{dt}$, $\frac{dx2}{dt}$ , x1 and x2 are all real numbers and represent concentration of two products by the pass of time. This system has two stable points which means perturbation of system around these two points is negligible. Can we use Lean to prove stability of the system around that equilibrium (stable) points.
Actually, in another theorem prover we need to provide Lyapunov function to prove it, but don't know whether we can prove it by Lean!

[Kevin Buzzard]

Can you write lean code expressing your question?

[Yaël Dillies]

Questions of the form "Can we prove <advanced statement> in Lean?" usually get the answer "Yes, but we can't even state <advanced statement> as of today".

[Parivash]

Right, hold on! let me formalized the conditions which must be passed to prove stability