Lyapunov's indirect method

TheoremExponential decay of a Hurwitz semigroup#✓fully proved

If A is Hurwitz, there are M, α > 0 with ‖exp(t A) v‖ ≤ M e^{-α t} ‖v‖ for all t ≥ 0 and all vectors v.

theorem IsHurwitz.exists_norm_exp_smul_mulVec_le {A : Matrix ι ι ℝ} (hA : A.IsHurwitz) :
    ∃ M α : ℝ, 0 < M ∧ 0 < α ∧ ∀ t : ℝ, 0 ≤ t → ∀ v : ι → ℝ,
      ‖NormedSpace.exp (t • A) *ᵥ v‖ ≤ M * exp (-(α * t)) * ‖v‖

Uses 1 · Used by 1

Statement usesHurwitz matrix

Used byLyapunov's indirect method (linearized stability), conditional decay form

TheoremLyapunov's indirect method (linearized stability), conditional decay form#✓fully proved

Let f (x⋆) = 0 and let f be differentiable at x⋆ with Jacobian matrix A. If A is Hurwitz, then for some δ, C, α > 0, every solution of x' = f(x) on [0, ∞) with ‖x(0) - x⋆‖ < δ satisfies ‖x(t) - x⋆‖ ≤ C e^{-α t} ‖x(0) - x⋆‖ for all t ≥ 0. This is conditional on the solution being defined on all of [0, ∞); it does not assert solution existence, so it is not by itself local exponential stability (Khalil 2002, Theorem 4.7, which assumes f is C¹ and concludes asymptotic stability).

theorem globalSolution_decay_of_hasFDerivAt {f : (ι → ℝ) → ι → ℝ}
    {xstar : ι → ℝ} {A : Matrix ι ι ℝ} (hf : f xstar = 0)
    (hfA : HasFDerivAt f (LinearMap.toContinuousLinearMap (Matrix.toLin' A)) xstar)
    (hA : A.IsHurwitz) :
    ∃ δ C α : ℝ, 0 < δ ∧ 0 < C ∧ 0 < α ∧ ∀ x : ℝ → ι → ℝ,
      (∀ t, 0 ≤ t → HasDerivAt x (f (x t)) t) → ‖x 0 - xstar‖ < δ →
        ∀ t, 0 ≤ t → ‖x t - xstar‖ ≤ C * exp (-(α * t)) * ‖x 0 - xstar‖

Uses 2 · Used by 1

Statement usesHurwitz matrix

Proof usesExponential decay of a Hurwitz semigroup

Used byThreshold theorem, stability half, conditional decay form

TheoremAsymptotic stability of linear ODEs with eigenvalues in the open left half-plane#●ready to prove

Let \(n \ge 0\) and let \(A\) be a real \(n \times n\) matrix such that every complex eigenvalue \(\mu\) of \(A\) (an eigenvalue of \(A\) viewed as a complex matrix acting on \(\mathbb{C}^n\)) satisfies \(\operatorname{Re} \mu < 0\). Let \(x : \mathbb{R} \to \mathbb{R}^n\) be a function that, at every \(t > 0\), is differentiable with derivative \(x'(t) = A\,x(t)\). Then \(\|x(t)\| \to 0\) as \(t \to \infty\), where \(\|\cdot\|\) is the sup norm on \(\mathbb{R}^n\).

public theorem_wanted linear_ode_asymptotic_stability
    (n : ℕ) (A : Matrix (Fin n) (Fin n) ℝ)
    (hA : ∀ μ : ℂ,
        Module.End.HasEigenvalue
          (Matrix.toLin' (A.map (algebraMap ℝ ℂ))) μ → μ.re < 0)
    (x : ℝ → (Fin n → ℝ))
    (hx : ∀ t : ℝ, 0 < t → HasDerivAt x (A.mulVec (x t)) t) :
    Filter.Tendsto (fun t : ℝ => ‖x t‖) Filter.atTop (nhds 0)

Sources

• Classical linear stability theory; Hirsch-Smale-Devaney. Problem linear_ode_asymptotic_stability of the lean-eval benchmark.

TheoremLyapunov's indirect method, instability#●ready to prove

Lyapunov's indirect method, instability (Khalil 2002, Theorem 4.7). If f is C¹, f x⋆ = 0, and the Jacobian matrix A of f at x⋆ has an eigenvalue with positive real part, then x⋆ is unstable: for some ε > 0, every neighbourhood of x⋆ contains an initial point x₀ from which a solution segment of x' = f(x) on some finite interval [0, T] reaches distance ≥ ε from x⋆. Quantifying over finite segments (rather than only over solutions on all of [0, ∞)) keeps the statement non-vacuous when solutions blow up in finite time.

theorem_wanted exists_unstable_of_hasFDerivAt {ι : Type*} [Fintype ι] [DecidableEq ι]
    {f : (ι → ℝ) → ι → ℝ} {xstar : ι → ℝ} {A : Matrix ι ι ℝ} (hf : f xstar = 0)
    (hfC1 : ContDiff ℝ 1 f)
    (hfA : HasFDerivAt f (LinearMap.toContinuousLinearMap (Matrix.toLin' A)) xstar)
    (hA : ∃ μ ∈ spectrum ℂ (A.map (algebraMap ℝ ℂ)), 0 < μ.re) :
    ∃ ε > 0, ∀ δ > 0, ∃ x₀ : ι → ℝ, ‖x₀ - xstar‖ < δ ∧ ∃ T : ℝ, 0 ≤ T ∧
      ∃ x : ℝ → ι → ℝ, x 0 = x₀ ∧ (∀ t ∈ Set.Icc 0 T, HasDerivAt x (f (x t)) t) ∧
        ε ≤ ‖x T - xstar‖

2 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.