3.5. The exponential contraction flow in 1-d🔗

We consider the flow of the vector field f : ℝ → ℝ given by f(x) = r x for some fixed r : ℝ.

def

smulFlow (r : ℝ) : Flow ℝ ℝ
smulFlow (r : ℝ) : Flow ℝ ℝ

The flow of the vector field x ↦ r • x.

Even without knowing the explicit solution of the ODE, it is easy to see that the function V(x) = x ^ 2 is Lyapunov function if r ≤ 0.

theorem

isLyapunov_sq_smulFlow {r : ℝ} (hr : 0 ≤ r) :
  IsLyapunov (fun x ↦ x ^ 2) (smulFlow (-r)).toFun
isLyapunov_sq_smulFlow {r : ℝ}
  (hr : 0 ≤ r) :
  IsLyapunov (fun x ↦ x ^ 2)
    (smulFlow (-r)).toFun

The function x ↦ x ^ 2 is a Lyapunov function for the system d/dt x = (-r) • x.

From this it follows that the origin is globally asymptotic stable:

theorem

isStableOn_smulFlow {r : ℝ} (hr : 0 ≤ r) :
  (𝓝 0).IsStableOn (smulFlow (-r)).toFun (Set.Ici 0)
isStableOn_smulFlow {r : ℝ} (hr : 0 ≤ r) :
  (𝓝 0).IsStableOn (smulFlow (-r)).toFun
    (Set.Ici 0)

The origin is stable under the forward flow of d/dt x = r x

theorem

tendsto_smulFlow {r : ℝ} (hr : 0 < r) (x : ℝ) :
  Filter.Tendsto (fun x_1 ↦ (smulFlow (-r)).toFun x_1 x) Filter.atTop
    (𝓝 0)
tendsto_smulFlow {r : ℝ} (hr : 0 < r)
  (x : ℝ) :
  Filter.Tendsto
    (fun x_1 ↦
      (smulFlow (-r)).toFun x_1 x)
    Filter.atTop (𝓝 0)

The origin is globally asymptotic stable under the forward flow of d/dt x = r x