Linear ODE with negative-real-part eigenvalues is asymptotically stable

Problem statement

Notes: If every eigenvalue of A has negative real part, every solution of x' = Ax decays to zero in norm.

Source: Classical linear stability theory; Hirsch-Smale-Devaney.

Informal solution: Pass to the complexification; bring A to (Schur or Jordan) upper-triangular form; the matrix exponential satisfies ||exp(tA)|| <= C(1+t^{n-1}) exp(alpha t) for any alpha greater than the maximum real part of the spectrum, hence decays to 0. For any t_1 > 0, x(t) = exp((t - t_1) A) x(t_1) for t >= t_1 by uniqueness of the linear IVP, so ||x(t)|| -> 0 as t -> infty.

theorem declaration uses `sorry`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) := byn:ℕA:Matrix (Fin n) (Fin n) ℝhA:∀ (μ : ℂ), Module.End.HasEigenvalue (Matrix.toLin' (A.map ⇑(algebraMap ℝ ℂ))) μ → μ.re < 0x:ℝ → Fin n → ℝhx:∀ (t : ℝ), 0 < t → HasDerivAt x (A *ᵥ x t) t⊢ Filter.Tendsto (fun t => ‖x t‖) Filter.atTop (nhds 0)
  sorryAll goals completed! 🐙