Linear systems and fundamental matrices

TheoremGlobal existence and uniqueness for homogeneous linear ODEs#✓fully proved

Let \(E\) be a real Banach space, write \(L(E)\) for the space of continuous linear maps \(E \to E\) with the operator norm, let \(B : \mathbb{R} \to L(E)\) be continuous, and let \(t_0 \in \mathbb{R}\) and \(x_0 \in E\). Then there is exactly one function \(x : \mathbb{R} \to E\) with \(x(t_0) = x_0\) such that \(x\) is differentiable at every \(t \in \mathbb{R}\) with \(x'(t) = B(t)\,x(t)\).

theorem _root_.ODE.existsUnique_hasDerivAt_eq_continuousLinearMap
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
    (B : ℝ → E →L[ℝ] E) (t₀ : ℝ) (x₀ : E) (hB : Continuous B) :
    ∃! x : ℝ → E, x t₀ = x₀ ∧ ∀ t, HasDerivAt x (B t (x t)) t

Uses 1 · Used by 1

Proof usesGlobal existence and uniqueness for globally Lipschitz ODEs

Used byFundamental matrix of a linear system

TheoremJacobi's formula when the derivative is a left multiple of the matrix#✓fully proved

Let \(n \in \mathbb{N}\), let \(A\) be a real \(n \times n\) matrix, let \(\Phi : \mathbb{R} \to \mathbb{R}^{n \times n}\), and let \(t \in \mathbb{R}\). If \(\Phi\) is differentiable at \(t\) with \(\Phi'(t) = A \Phi(t)\), then \(s \mapsto \det \Phi(s)\) is differentiable at \(t\) with derivative \(\operatorname{tr}(A) \det \Phi(t)\).

theorem _root_.HasDerivAt.det_of_mul {n : ℕ}
    {Φ : ℝ → Matrix (Fin n) (Fin n) ℝ} {A : Matrix (Fin n) (Fin n) ℝ} {t : ℝ}
    (hΦ : HasDerivAt Φ (A * Φ t) t) :
    HasDerivAt (fun s ↦ (Φ s).det) (A.trace * (Φ t).det) t

Used by 2

Used byFundamental matrix of a linear system · Liouville's formula for the principal matrix solution

TheoremFundamental matrix of a linear system#✓fully proved

Let \(n \in \mathbb{N}\), let \(A : \mathbb{R} \to \mathbb{R}^{n \times n}\) be continuous, let \(t_0 \in \mathbb{R}\), and write \(I\) for the \(n \times n\) identity matrix. Then there is a function \(\Phi : \mathbb{R} \to \mathbb{R}^{n \times n}\) with \(\Phi(t_0) = I\), \(\Phi'(t) = A(t) \Phi(t)\) and \(\det \Phi(t) \ne 0\) for every \(t \in \mathbb{R}\), such that for every \(x_0 \in \mathbb{R}^n\) the function \(x(t) = \Phi(t) x_0\) satisfies \(x(t_0) = x_0\) and \(x'(t) = A(t) x(t)\) for every \(t \in \mathbb{R}\), and every \(y : \mathbb{R} \to \mathbb{R}^n\) with \(y(t_0) = x_0\) and \(y'(t) = A(t) y(t)\) for every \(t \in \mathbb{R}\) equals \(x\).

Proof: Global solutions are patched from clamped-time systems using Teschl, Theorem 3.9, then assembled into the principal matrix solution of (3.83) and Theorem 3.10. Liouville's formula gives invertibility as in (3.88)-(3.89).

theorem fundamental_matrix_linear_system
    {n : ℕ} (A : ℝ → Matrix (Fin n) (Fin n) ℝ) (t₀ : ℝ)
    (hA : Continuous A) :
    ∃ Φ : ℝ → Matrix (Fin n) (Fin n) ℝ, Φ t₀ = 1 ∧
      (∀ t, HasDerivAt Φ (A t * Φ t) t) ∧
      (∀ t, IsUnit (Φ t).det) ∧
      ∀ x₀ : Fin n → ℝ, ∃ x : ℝ → (Fin n → ℝ),
        x t₀ = x₀ ∧ (∀ t, HasDerivAt x ((A t).mulVec (x t)) t) ∧
        (∀ t, x t = (Φ t).mulVec x₀) ∧
        ∀ y : ℝ → (Fin n → ℝ), y t₀ = x₀ →
          (∀ t, HasDerivAt y ((A t).mulVec (y t)) t) → y = x

Sources

• G. Teschl, Ordinary Differential Equations and Dynamical Systems, Section 3.4; stable ref https://en.wikipedia.org/wiki/Fundamental_matrix_(linear_differential_equation).

Uses 2

Proof usesJacobi's formula when the derivative is a left multiple of the matrix · Global existence and uniqueness for homogeneous linear ODEs

TheoremLiouville's formula for the principal matrix solution#✓fully proved

Let \(n \in \mathbb{N}\), let \(A : \mathbb{R} \to \mathbb{R}^{n \times n}\) be continuous, let \(t_0 \in \mathbb{R}\), write \(I\) for the \(n \times n\) identity matrix, and let \(\Phi : \mathbb{R} \to \mathbb{R}^{n \times n}\) satisfy \(\Phi(t_0) = I\) and \(\Phi'(t) = A(t) \Phi(t)\) for every \(t \in \mathbb{R}\). Then for every \(t \in \mathbb{R}\), \(\det \Phi(t) = \det \Phi(t_0) \exp\left(\int_{t_0}^{t} \operatorname{tr} A(s)\, ds\right)\).

Proof: Jacobi's formula follows from the determinant's first-order term; an integrating factor then gives Teschl, Lemma 3.11, formula (3.91).

theorem fundamental_matrix_liouville_det
    {n : ℕ} (A : ℝ → Matrix (Fin n) (Fin n) ℝ) (t₀ : ℝ)
    (hA : Continuous A)
    (Φ : ℝ → Matrix (Fin n) (Fin n) ℝ)
    (hΦ0 : Φ t₀ = 1) (hΦ : ∀ t, HasDerivAt Φ (A t * Φ t) t) :
    ∀ t, (Φ t).det = (Φ t₀).det * Real.exp (∫ s in t₀..t, (A s).trace)

Sources

• G. Teschl, Ordinary Differential Equations and Dynamical Systems, Section 3.4; https://en.wikipedia.org/wiki/Abel%27s_identity.

Uses 1

Proof usesJacobi's formula when the derivative is a left multiple of the matrix

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.