Physlib

Physlib.SpaceAndTime.Time.MatrixDerivatives

Time derivatives of matrix-valued functions

General lemmas on the time derivative `∂ₜ` of square-matrix-valued functions of time: a product rule, the commutation of the derivative with transpose, and the commutation of the derivative with taking a matrix entry. These are the tools needed to differentiate a path of matrices.

They rely on the (opt-in) operator-norm structure on matrices — activated here as local instances — only to invoke the product rule and to view transpose (through `Matrix.transposeLinearEquiv`) as a continuous linear map. Since all norms on a fixed finite-dimensional space induce the same topology, differentiability does not depend on this choice.

4 declarations

theorem

AA is differentiable at t  ⟹  A⊤t \implies A^\top is differentiable at tt

Let EE be a normed real vector space. If a matrix-valued function A:E→Rd×dA: E \to \mathbb{R}^{d \times d} is differentiable at a point t∈Et \in E, then the function s↦A(s)⊤s \mapsto A(s)^\top (the transpose of A(s)A(s)) is also differentiable at tt.

theorem

Product Rule for the Time Derivative of Matrix-Valued Functions ∂t(AB)\partial_t (A B)

Let A,B:Time→Rd×dA, B : \text{Time} \to \mathbb{R}^{d \times d} be functions mapping time to d×dd \times d real matrices. If AA and BB are differentiable at a specific time tt, then the time derivative ∂t\partial_t of their product at tt satisfies the product rule: ∂t(A⋅B)(t)=A(t)⋅∂tB(t)+∂tA(t)⋅B(t)\partial_t (A \cdot B)(t) = A(t) \cdot \partial_t B(t) + \partial_t A(t) \cdot B(t)

theorem

∂t(A⊤)=(∂tA)⊤\partial_t (A^\top) = (\partial_t A)^\top

Let A:Time→Rd×dA : \text{Time} \to \mathbb{R}^{d \times d} be a function mapping time to square matrices of dimension dd over the real numbers. For any t∈Timet \in \text{Time}, if AA is differentiable at tt, then the time derivative of the transpose of AA at tt is equal to the transpose of the time derivative of AA at tt: ∂t(s↦A(s)⊤)(t)=(∂tA(t))⊤\partial_t (s \mapsto A(s)^\top)(t) = (\partial_t A(t))^\top where M⊤M^\top denotes the transpose of a matrix MM and ∂t\partial_t denotes the time derivative.

theorem

The Time Derivative Commutes with Matrix Indexing

Let A:Time→Matrixd×d(R)A: \text{Time} \to \text{Matrix}_{d \times d}(\mathbb{R}) be a function that maps time to a square matrix. If AA is differentiable at a time tt, then for any row index ii and column index jj, the time derivative of the (i,j)(i, j)-th entry of AA at tt is equal to the (i,j)(i, j)-th entry of the time derivative of AA at tt: ∂t(A(s)ij)∣s=t=(∂tA(t))ij \partial_t (A(s)_{ij}) \big|_{s=t} = (\partial_t A(t))_{ij}