Physlib.SpaceAndTime.Time.MatrixDerivatives

Physlib
SpaceAndTime
Time
MatrixDerivatives

Imports

/-
Copyright (c) 2026 Giuseppe Sorge. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Giuseppe Sorge
-/
module

public import Physlib.SpaceAndTime.Time.Derivatives
public import Mathlib.Analysis.Matrix.Normed

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.

@[expose] public section

attribute [local instance] Matrix.linftyOpNormedAddCommGroup Matrix.linftyOpNormedSpace
  Matrix.linftyOpNormedRing Matrix.linftyOpNormedAlgebra

The transpose of a differentiable matrix-valued function is differentiable (cf. Continuous.matrix_transpose).

lemma DifferentiableAt.matrix_transpose {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    {A : E → Matrix (Fin d) (Fin d) ℝ} {t : E} (hA : DifferentiableAt ℝ A t) :
    DifferentiableAt ℝ (fun s => (A s)ᵀ) t :=
  ((transposeLinearEquiv (Fin d) (Fin d) ℝ ℝ).toLinearMap.toContinuousLinearMap).differentiableAt
    |>.comp t hA

Product rule for the time derivative of a product of matrix-valued functions.


lemma deriv_matrix_mul (A B : Time → Matrix (Fin d) (Fin d) ℝ) (t : Time)
    (hA : DifferentiableAt ℝ A t) (hB : DifferentiableAt ℝ B t) :
    ∂ₜ (fun s => A s * B s) t = A t * ∂ₜ B t + ∂ₜ A t * B t := byd:ℕA:Time → Matrix (Fin d) (Fin d) ℝB:Time → Matrix (Fin d) (Fin d) ℝt:TimehA:DifferentiableAt ℝ A thB:DifferentiableAt ℝ B t⊢ ∂ₜ (fun s => A s * B s) t = A t * ∂ₜ B t + ∂ₜ A t * B t
  have h : HasFDerivAt (fun s => A s * B s)
      (A t • fderiv ℝ B t + fderiv ℝ A t <• B t) t := hA.hasFDerivAt.mul' hB.hasFDerivAtd:ℕA:Time → Matrix (Fin d) (Fin d) ℝB:Time → Matrix (Fin d) (Fin d) ℝt:TimehA:DifferentiableAt ℝ A thB:DifferentiableAt ℝ B th:HasFDerivAt (fun s => A s * B s) (A t •> fderiv ℝ B t + fderiv ℝ A t <• B t) t⊢ ∂ₜ (fun s => A s * B s) t = A t * ∂ₜ B t + ∂ₜ A t * B t
  rw [Time.deriv_eq,d:ℕA:Time → Matrix (Fin d) (Fin d) ℝB:Time → Matrix (Fin d) (Fin d) ℝt:TimehA:DifferentiableAt ℝ A thB:DifferentiableAt ℝ B th:HasFDerivAt (fun s => A s * B s) (A t •> fderiv ℝ B t + fderiv ℝ A t <• B t) t⊢ (fderiv ℝ (fun s => A s * B s) t) 1 = A t * ∂ₜ B t + ∂ₜ A t * B td:ℕA:Time → Matrix (Fin d) (Fin d) ℝB:Time → Matrix (Fin d) (Fin d) ℝt:TimehA:DifferentiableAt ℝ A thB:DifferentiableAt ℝ B th:HasFDerivAt (fun s => A s * B s) (A t •> fderiv ℝ B t + fderiv ℝ A t <• B t) t⊢ (A t •> fderiv ℝ B t) 1 + (fderiv ℝ A t <• B t) 1 = A t * (fderiv ℝ B t) 1 + (fderiv ℝ A t) 1 * B t h.fderiv,d:ℕA:Time → Matrix (Fin d) (Fin d) ℝB:Time → Matrix (Fin d) (Fin d) ℝt:TimehA:DifferentiableAt ℝ A thB:DifferentiableAt ℝ B th:HasFDerivAt (fun s => A s * B s) (A t •> fderiv ℝ B t + fderiv ℝ A t <• B t) t⊢ (A t •> fderiv ℝ B t + fderiv ℝ A t <• B t) 1 = A t * ∂ₜ B t + ∂ₜ A t * B td:ℕA:Time → Matrix (Fin d) (Fin d) ℝB:Time → Matrix (Fin d) (Fin d) ℝt:TimehA:DifferentiableAt ℝ A thB:DifferentiableAt ℝ B th:HasFDerivAt (fun s => A s * B s) (A t •> fderiv ℝ B t + fderiv ℝ A t <• B t) t⊢ (A t •> fderiv ℝ B t) 1 + (fderiv ℝ A t <• B t) 1 = A t * (fderiv ℝ B t) 1 + (fderiv ℝ A t) 1 * B t Time.deriv_eq,d:ℕA:Time → Matrix (Fin d) (Fin d) ℝB:Time → Matrix (Fin d) (Fin d) ℝt:TimehA:DifferentiableAt ℝ A thB:DifferentiableAt ℝ B th:HasFDerivAt (fun s => A s * B s) (A t •> fderiv ℝ B t + fderiv ℝ A t <• B t) t⊢ (A t •> fderiv ℝ B t + fderiv ℝ A t <• B t) 1 = A t * (fderiv ℝ B t) 1 + ∂ₜ A t * B td:ℕA:Time → Matrix (Fin d) (Fin d) ℝB:Time → Matrix (Fin d) (Fin d) ℝt:TimehA:DifferentiableAt ℝ A thB:DifferentiableAt ℝ B th:HasFDerivAt (fun s => A s * B s) (A t •> fderiv ℝ B t + fderiv ℝ A t <• B t) t⊢ (A t •> fderiv ℝ B t) 1 + (fderiv ℝ A t <• B t) 1 = A t * (fderiv ℝ B t) 1 + (fderiv ℝ A t) 1 * B t Time.deriv_eq,d:ℕA:Time → Matrix (Fin d) (Fin d) ℝB:Time → Matrix (Fin d) (Fin d) ℝt:TimehA:DifferentiableAt ℝ A thB:DifferentiableAt ℝ B th:HasFDerivAt (fun s => A s * B s) (A t •> fderiv ℝ B t + fderiv ℝ A t <• B t) t⊢ (A t •> fderiv ℝ B t + fderiv ℝ A t <• B t) 1 = A t * (fderiv ℝ B t) 1 + (fderiv ℝ A t) 1 * B td:ℕA:Time → Matrix (Fin d) (Fin d) ℝB:Time → Matrix (Fin d) (Fin d) ℝt:TimehA:DifferentiableAt ℝ A thB:DifferentiableAt ℝ B th:HasFDerivAt (fun s => A s * B s) (A t •> fderiv ℝ B t + fderiv ℝ A t <• B t) t⊢ (A t •> fderiv ℝ B t) 1 + (fderiv ℝ A t <• B t) 1 = A t * (fderiv ℝ B t) 1 + (fderiv ℝ A t) 1 * B t _root_.add_applyd:ℕA:Time → Matrix (Fin d) (Fin d) ℝB:Time → Matrix (Fin d) (Fin d) ℝt:TimehA:DifferentiableAt ℝ A thB:DifferentiableAt ℝ B th:HasFDerivAt (fun s => A s * B s) (A t •> fderiv ℝ B t + fderiv ℝ A t <• B t) t⊢ (A t •> fderiv ℝ B t) 1 + (fderiv ℝ A t <• B t) 1 = A t * (fderiv ℝ B t) 1 + (fderiv ℝ A t) 1 * B td:ℕA:Time → Matrix (Fin d) (Fin d) ℝB:Time → Matrix (Fin d) (Fin d) ℝt:TimehA:DifferentiableAt ℝ A thB:DifferentiableAt ℝ B th:HasFDerivAt (fun s => A s * B s) (A t •> fderiv ℝ B t + fderiv ℝ A t <• B t) t⊢ (A t •> fderiv ℝ B t) 1 + (fderiv ℝ A t <• B t) 1 = A t * (fderiv ℝ B t) 1 + (fderiv ℝ A t) 1 * B t]d:ℕA:Time → Matrix (Fin d) (Fin d) ℝB:Time → Matrix (Fin d) (Fin d) ℝt:TimehA:DifferentiableAt ℝ A thB:DifferentiableAt ℝ B th:HasFDerivAt (fun s => A s * B s) (A t •> fderiv ℝ B t + fderiv ℝ A t <• B t) t⊢ (A t •> fderiv ℝ B t) 1 + (fderiv ℝ A t <• B t) 1 = A t * (fderiv ℝ B t) 1 + (fderiv ℝ A t) 1 * B t
  simp only [_root_.smul_apply, smul_eq_mul, op_smul_eq_mul]All goals completed! 🐙

The time derivative commutes with transpose.


lemma deriv_matrix_transpose (A : Time → Matrix (Fin d) (Fin d) ℝ) (t : Time)
    (hA : DifferentiableAt ℝ A t) :
    ∂ₜ (fun s => (A s)ᵀ) t = (∂ₜ A t)ᵀ := byd:ℕA:Time → Matrix (Fin d) (Fin d) ℝt:TimehA:DifferentiableAt ℝ A t⊢ ∂ₜ (fun s => (A s)ᵀ) t = (∂ₜ A t)ᵀ
  let T : Matrix (Fin d) (Fin d) ℝ →L[ℝ] Matrix (Fin d) (Fin d) ℝ :=
    (transposeLinearEquiv (Fin d) (Fin d) ℝ ℝ).toLinearMap.toContinuousLinearMapd:ℕA:Time → Matrix (Fin d) (Fin d) ℝt:TimehA:DifferentiableAt ℝ A tT:Matrix (Fin d) (Fin d) ℝ →L[ℝ] Matrix (Fin d) (Fin d) ℝ := LinearMap.toContinuousLinearMap ↑(transposeLinearEquiv (Fin d) (Fin d) ℝ ℝ)⊢ ∂ₜ (fun s => (A s)ᵀ) t = (∂ₜ A t)ᵀ
  have h : HasFDerivAt (fun s => (A s)ᵀ) (T.comp (fderiv ℝ A t)) t :=
    T.hasFDerivAt.comp t hA.hasFDerivAtd:ℕA:Time → Matrix (Fin d) (Fin d) ℝt:TimehA:DifferentiableAt ℝ A tT:Matrix (Fin d) (Fin d) ℝ →L[ℝ] Matrix (Fin d) (Fin d) ℝ := LinearMap.toContinuousLinearMap ↑(transposeLinearEquiv (Fin d) (Fin d) ℝ ℝ)h:HasFDerivAt (fun s => (A s)ᵀ) (T ∘SL fderiv ℝ A t) t⊢ ∂ₜ (fun s => (A s)ᵀ) t = (∂ₜ A t)ᵀ
  rw [Time.deriv_eq,d:ℕA:Time → Matrix (Fin d) (Fin d) ℝt:TimehA:DifferentiableAt ℝ A tT:Matrix (Fin d) (Fin d) ℝ →L[ℝ] Matrix (Fin d) (Fin d) ℝ := LinearMap.toContinuousLinearMap ↑(transposeLinearEquiv (Fin d) (Fin d) ℝ ℝ)h:HasFDerivAt (fun s => (A s)ᵀ) (T ∘SL fderiv ℝ A t) t⊢ (fderiv ℝ (fun s => (A s)ᵀ) t) 1 = (∂ₜ A t)ᵀd:ℕA:Time → Matrix (Fin d) (Fin d) ℝt:TimehA:DifferentiableAt ℝ A tT:Matrix (Fin d) (Fin d) ℝ →L[ℝ] Matrix (Fin d) (Fin d) ℝ := LinearMap.toContinuousLinearMap ↑(transposeLinearEquiv (Fin d) (Fin d) ℝ ℝ)h:HasFDerivAt (fun s => (A s)ᵀ) (T ∘SL fderiv ℝ A t) t⊢ (T ∘SL fderiv ℝ A t) 1 = ((fderiv ℝ A t) 1)ᵀ h.fderiv,d:ℕA:Time → Matrix (Fin d) (Fin d) ℝt:TimehA:DifferentiableAt ℝ A tT:Matrix (Fin d) (Fin d) ℝ →L[ℝ] Matrix (Fin d) (Fin d) ℝ := LinearMap.toContinuousLinearMap ↑(transposeLinearEquiv (Fin d) (Fin d) ℝ ℝ)h:HasFDerivAt (fun s => (A s)ᵀ) (T ∘SL fderiv ℝ A t) t⊢ (T ∘SL fderiv ℝ A t) 1 = (∂ₜ A t)ᵀd:ℕA:Time → Matrix (Fin d) (Fin d) ℝt:TimehA:DifferentiableAt ℝ A tT:Matrix (Fin d) (Fin d) ℝ →L[ℝ] Matrix (Fin d) (Fin d) ℝ := LinearMap.toContinuousLinearMap ↑(transposeLinearEquiv (Fin d) (Fin d) ℝ ℝ)h:HasFDerivAt (fun s => (A s)ᵀ) (T ∘SL fderiv ℝ A t) t⊢ (T ∘SL fderiv ℝ A t) 1 = ((fderiv ℝ A t) 1)ᵀ Time.deriv_eqd:ℕA:Time → Matrix (Fin d) (Fin d) ℝt:TimehA:DifferentiableAt ℝ A tT:Matrix (Fin d) (Fin d) ℝ →L[ℝ] Matrix (Fin d) (Fin d) ℝ := LinearMap.toContinuousLinearMap ↑(transposeLinearEquiv (Fin d) (Fin d) ℝ ℝ)h:HasFDerivAt (fun s => (A s)ᵀ) (T ∘SL fderiv ℝ A t) t⊢ (T ∘SL fderiv ℝ A t) 1 = ((fderiv ℝ A t) 1)ᵀd:ℕA:Time → Matrix (Fin d) (Fin d) ℝt:TimehA:DifferentiableAt ℝ A tT:Matrix (Fin d) (Fin d) ℝ →L[ℝ] Matrix (Fin d) (Fin d) ℝ := LinearMap.toContinuousLinearMap ↑(transposeLinearEquiv (Fin d) (Fin d) ℝ ℝ)h:HasFDerivAt (fun s => (A s)ᵀ) (T ∘SL fderiv ℝ A t) t⊢ (T ∘SL fderiv ℝ A t) 1 = ((fderiv ℝ A t) 1)ᵀ]d:ℕA:Time → Matrix (Fin d) (Fin d) ℝt:TimehA:DifferentiableAt ℝ A tT:Matrix (Fin d) (Fin d) ℝ →L[ℝ] Matrix (Fin d) (Fin d) ℝ := LinearMap.toContinuousLinearMap ↑(transposeLinearEquiv (Fin d) (Fin d) ℝ ℝ)h:HasFDerivAt (fun s => (A s)ᵀ) (T ∘SL fderiv ℝ A t) t⊢ (T ∘SL fderiv ℝ A t) 1 = ((fderiv ℝ A t) 1)ᵀ
  rflAll goals completed! 🐙

The time derivative commutes with taking a matrix entry.


lemma deriv_matrix_apply (A : Time → Matrix (Fin d) (Fin d) ℝ) (t : Time)
    (hA : DifferentiableAt ℝ A t) (i j : Fin d) :
    ∂ₜ (fun s => A s i j) t = (∂ₜ A t) i j := byd:ℕA:Time → Matrix (Fin d) (Fin d) ℝt:TimehA:DifferentiableAt ℝ A ti:Fin dj:Fin d⊢ ∂ₜ (fun s => A s i j) t = ∂ₜ A t i j
  let E : Matrix (Fin d) (Fin d) ℝ →L[ℝ] ℝ :=
    (Matrix.entryLinearMap ℝ ℝ i j).toContinuousLinearMapd:ℕA:Time → Matrix (Fin d) (Fin d) ℝt:TimehA:DifferentiableAt ℝ A ti:Fin dj:Fin dE:Matrix (Fin d) (Fin d) ℝ →L[ℝ] ℝ := LinearMap.toContinuousLinearMap (entryLinearMap ℝ ℝ i j)⊢ ∂ₜ (fun s => A s i j) t = ∂ₜ A t i j
  have h : HasFDerivAt (fun s => A s i j) (E.comp (fderiv ℝ A t)) t :=
    E.hasFDerivAt.comp t hA.hasFDerivAtd:ℕA:Time → Matrix (Fin d) (Fin d) ℝt:TimehA:DifferentiableAt ℝ A ti:Fin dj:Fin dE:Matrix (Fin d) (Fin d) ℝ →L[ℝ] ℝ := LinearMap.toContinuousLinearMap (entryLinearMap ℝ ℝ i j)h:HasFDerivAt (fun s => A s i j) (E ∘SL fderiv ℝ A t) t⊢ ∂ₜ (fun s => A s i j) t = ∂ₜ A t i j
  rw [Time.deriv_eq,d:ℕA:Time → Matrix (Fin d) (Fin d) ℝt:TimehA:DifferentiableAt ℝ A ti:Fin dj:Fin dE:Matrix (Fin d) (Fin d) ℝ →L[ℝ] ℝ := LinearMap.toContinuousLinearMap (entryLinearMap ℝ ℝ i j)h:HasFDerivAt (fun s => A s i j) (E ∘SL fderiv ℝ A t) t⊢ (fderiv ℝ (fun s => A s i j) t) 1 = ∂ₜ A t i jd:ℕA:Time → Matrix (Fin d) (Fin d) ℝt:TimehA:DifferentiableAt ℝ A ti:Fin dj:Fin dE:Matrix (Fin d) (Fin d) ℝ →L[ℝ] ℝ := LinearMap.toContinuousLinearMap (entryLinearMap ℝ ℝ i j)h:HasFDerivAt (fun s => A s i j) (E ∘SL fderiv ℝ A t) t⊢ (E ∘SL fderiv ℝ A t) 1 = (fderiv ℝ A t) 1 i j h.fderiv,d:ℕA:Time → Matrix (Fin d) (Fin d) ℝt:TimehA:DifferentiableAt ℝ A ti:Fin dj:Fin dE:Matrix (Fin d) (Fin d) ℝ →L[ℝ] ℝ := LinearMap.toContinuousLinearMap (entryLinearMap ℝ ℝ i j)h:HasFDerivAt (fun s => A s i j) (E ∘SL fderiv ℝ A t) t⊢ (E ∘SL fderiv ℝ A t) 1 = ∂ₜ A t i jd:ℕA:Time → Matrix (Fin d) (Fin d) ℝt:TimehA:DifferentiableAt ℝ A ti:Fin dj:Fin dE:Matrix (Fin d) (Fin d) ℝ →L[ℝ] ℝ := LinearMap.toContinuousLinearMap (entryLinearMap ℝ ℝ i j)h:HasFDerivAt (fun s => A s i j) (E ∘SL fderiv ℝ A t) t⊢ (E ∘SL fderiv ℝ A t) 1 = (fderiv ℝ A t) 1 i j Time.deriv_eqd:ℕA:Time → Matrix (Fin d) (Fin d) ℝt:TimehA:DifferentiableAt ℝ A ti:Fin dj:Fin dE:Matrix (Fin d) (Fin d) ℝ →L[ℝ] ℝ := LinearMap.toContinuousLinearMap (entryLinearMap ℝ ℝ i j)h:HasFDerivAt (fun s => A s i j) (E ∘SL fderiv ℝ A t) t⊢ (E ∘SL fderiv ℝ A t) 1 = (fderiv ℝ A t) 1 i jd:ℕA:Time → Matrix (Fin d) (Fin d) ℝt:TimehA:DifferentiableAt ℝ A ti:Fin dj:Fin dE:Matrix (Fin d) (Fin d) ℝ →L[ℝ] ℝ := LinearMap.toContinuousLinearMap (entryLinearMap ℝ ℝ i j)h:HasFDerivAt (fun s => A s i j) (E ∘SL fderiv ℝ A t) t⊢ (E ∘SL fderiv ℝ A t) 1 = (fderiv ℝ A t) 1 i j]d:ℕA:Time → Matrix (Fin d) (Fin d) ℝt:TimehA:DifferentiableAt ℝ A ti:Fin dj:Fin dE:Matrix (Fin d) (Fin d) ℝ →L[ℝ] ℝ := LinearMap.toContinuousLinearMap (entryLinearMap ℝ ℝ i j)h:HasFDerivAt (fun s => A s i j) (E ∘SL fderiv ℝ A t) t⊢ (E ∘SL fderiv ℝ A t) 1 = (fderiv ℝ A t) 1 i j
  rflAll goals completed! 🐙