feat(ClassicalMechanics): add rigid-body angular velocity tensor

Physlib.lean

@@ -17,6 +17,7 @@ public import Physlib.ClassicalMechanics.OrbitalMechanics.VisViva
 public import Physlib.ClassicalMechanics.Pendulum.CoplanarDoublePendulum
 public import Physlib.ClassicalMechanics.Pendulum.MiscellaneousPendulumPivotMotions
 public import Physlib.ClassicalMechanics.Pendulum.SlidingPendulum
+public import Physlib.ClassicalMechanics.RigidBody.AngularVelocity
 public import Physlib.ClassicalMechanics.RigidBody.Basic
 public import Physlib.ClassicalMechanics.RigidBody.Motion
 public import Physlib.ClassicalMechanics.RigidBody.SolidSphere
@@ -435,6 +436,7 @@ public import Physlib.SpaceAndTime.SpaceTime.LorentzAction
 public import Physlib.SpaceAndTime.SpaceTime.TimeSlice
 public import Physlib.SpaceAndTime.Time.Basic
 public import Physlib.SpaceAndTime.Time.Derivatives
+public import Physlib.SpaceAndTime.Time.MatrixDerivatives
 public import Physlib.SpaceAndTime.Time.TimeMan
 public import Physlib.SpaceAndTime.Time.TimeTransMan
 public import Physlib.SpaceAndTime.Time.TimeUnit

Physlib/ClassicalMechanics/RigidBody/AngularVelocity.lean

@@ -0,0 +1,95 @@
+/-
+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.ClassicalMechanics.RigidBody.Motion
+public import Physlib.SpaceAndTime.Time.MatrixDerivatives
+/-!
+
+# The angular velocity of a rigid body
+
+For a rigid body in motion the orientation `R(t) = orientation t` is a time-dependent rotation. Its
+instantaneous rate of change is encoded by the *angular velocity tensor*
+`Ω(t) = Ṙ(t) R(t)ᵀ`, the antisymmetric tensor `Ω` appearing in the Landau–Lifshitz decomposition
+`v = V + Ω × r` of the velocity of a point of the body.
+
+A basic consistency check is that `Ω` is skew-symmetric, `Ωᵀ = -Ω` (equivalently `Ω ∈ 𝔰𝔬(d)`); this
+follows by differentiating the orthogonality identity `R Rᵀ = 1`. The general product and transpose
+rules for time derivatives of matrices used for this live in
+`Physlib.SpaceAndTime.Time.MatrixDerivatives`.
+
+## References
+- Landau and Lifshitz, Mechanics, Section 31.
+-/
+
+@[expose] public section
+
+open Time Manifold Matrix
+
+attribute [local instance] Matrix.linftyOpNormedAddCommGroup Matrix.linftyOpNormedSpace
+  Matrix.linftyOpNormedRing Matrix.linftyOpNormedAlgebra
+
+namespace RigidBodyMotion
+
+variable {d : ℕ}
+
+/-- The orientation of the body as a matrix-valued function of time: the underlying matrix of
+`orientation`. -/
+noncomputable def orientationMatrix (M : RigidBodyMotion d) : Time → Matrix (Fin d) (Fin d) ℝ :=
+  fun s => (M.orientation s).val
+
+lemma orientationMatrix_apply (M : RigidBodyMotion d) (t : Time) :
+    M.orientationMatrix t = (M.orientation t).val := rfl
+
+/-- The orientation matrix is special orthogonal, so `R Rᵀ = 1`. -/
+lemma orientationMatrix_mul_transpose (M : RigidBodyMotion d) (t : Time) :
+    M.orientationMatrix t * (M.orientationMatrix t)ᵀ = 1 :=
+  (mem_orthogonalGroup_iff (Fin d) ℝ).mp
+    (mem_specialOrthogonalGroup_iff.mp (M.orientation t).2).1
+
+/-- The angular velocity tensor `Ω(t) = Ṙ(t) R(t)ᵀ` of a rigid body in motion, where
+`R(t) = orientation t`. It is the antisymmetric tensor `Ω` in the Landau–Lifshitz decomposition
+`v = V + Ω × r` of the velocity of a point of the body. -/
+noncomputable def angularVelocityTensor (M : RigidBodyMotion d) (t : Time) :
+    Matrix (Fin d) (Fin d) ℝ :=
+  ∂ₜ M.orientationMatrix t * (M.orientationMatrix t)ᵀ
+
+lemma angularVelocityTensor_eq (M : RigidBodyMotion d) (t : Time) :
+    M.angularVelocityTensor t = ∂ₜ M.orientationMatrix t * (M.orientationMatrix t)ᵀ := rfl
+
+/-- The angular velocity tensor is skew-symmetric, `Ωᵀ = -Ω`: it lies in the Lie algebra `𝔰𝔬(d)`.
+This is the litmus check that `Ω = Ṙ Rᵀ` is a genuine angular-velocity tensor, and follows by
+differentiating the orthogonality identity `R Rᵀ = 1`. -/
+lemma angularVelocityTensor_transpose (M : RigidBodyMotion d) (t : Time)
+    (hR : DifferentiableAt ℝ M.orientationMatrix t) :
+    (M.angularVelocityTensor t)ᵀ = - M.angularVelocityTensor t := by
+  have hconst : (fun s => M.orientationMatrix s * (M.orientationMatrix s)ᵀ)
+      = fun _ => (1 : Matrix (Fin d) (Fin d) ℝ) := by
+    funext s
+    exact M.orientationMatrix_mul_transpose s
+  have hderiv0 : ∂ₜ (fun s => M.orientationMatrix s * (M.orientationMatrix s)ᵀ) t = 0 := by
+    rw [hconst]
+    exact Time.deriv_const 1
+  have hRt : DifferentiableAt ℝ (fun s => (M.orientationMatrix s)ᵀ) t :=
+    Matrix.transposeCLM.differentiableAt.comp t hR
+  have hprod :=
+    Time.deriv_matrix_mul M.orientationMatrix (fun s => (M.orientationMatrix s)ᵀ) t hR hRt
+  rw [Time.deriv_matrix_transpose M.orientationMatrix t hR, hderiv0] at hprod
+  rw [angularVelocityTensor, transpose_mul, transpose_transpose]
+  exact eq_neg_of_add_eq_zero_left hprod.symm
+
+/-- A rigid body whose orientation is constant in time has zero angular velocity. -/
+lemma angularVelocityTensor_of_orientation_const (M : RigidBodyMotion d)
+    (R : Matrix.specialOrthogonalGroup (Fin d) ℝ) (h : M.orientation = fun _ => R) :
+    M.angularVelocityTensor = 0 := by
+  funext t
+  have hconst : M.orientationMatrix = fun _ => R.val := by
+    funext s
+    rw [orientationMatrix_apply, h]
+  rw [angularVelocityTensor_eq, hconst, Time.deriv_eq]
+  simp
+
+end RigidBodyMotion

Physlib/SpaceAndTime/Time/MatrixDerivatives.lean

@@ -0,0 +1,69 @@
+/-
+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
+and the commutation of the derivative with transpose. Together with `Matrix.transposeCLM` (transpose
+as a continuous linear map) 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 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
+
+open Time Manifold Matrix
+open scoped RightActions
+
+attribute [local instance] Matrix.linftyOpNormedAddCommGroup Matrix.linftyOpNormedSpace
+  Matrix.linftyOpNormedRing Matrix.linftyOpNormedAlgebra
+
+namespace Matrix
+
+variable {d : ℕ}
+
+/-- Transpose as a continuous linear map on square real matrices. -/
+noncomputable def transposeCLM :
+    Matrix (Fin d) (Fin d) ℝ →L[ℝ] Matrix (Fin d) (Fin d) ℝ :=
+  (Matrix.transposeLinearEquiv (Fin d) (Fin d) ℝ ℝ).toLinearMap.toContinuousLinearMap
+
+@[simp]
+lemma transposeCLM_apply (A : Matrix (Fin d) (Fin d) ℝ) : transposeCLM A = Aᵀ := rfl
+
+end Matrix
+
+namespace Time
+
+variable {d : ℕ}
+
+/-- 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 := by
+  have h : HasFDerivAt (fun s => A s * B s)
+      (A t • fderiv ℝ B t + fderiv ℝ A t <• B t) t := hA.hasFDerivAt.mul' hB.hasFDerivAt
+  rw [Time.deriv_eq, h.fderiv, Time.deriv_eq, Time.deriv_eq, _root_.add_apply]
+  simp only [_root_.smul_apply, smul_eq_mul, op_smul_eq_mul]
+
+/-- 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)ᵀ := by
+  have h : HasFDerivAt (fun s => (A s)ᵀ) (Matrix.transposeCLM.comp (fderiv ℝ A t)) t :=
+    Matrix.transposeCLM.hasFDerivAt.comp t hA.hasFDerivAt
+  rw [Time.deriv_eq, h.fderiv, Time.deriv_eq]
+  simp
+
+end Time