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,86 @@
+/-
+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 matrix is special orthogonal, so `R Rᵀ = 1`. -/
+lemma orientation_mul_transpose (M : RigidBodyMotion d) (t : Time) :
+    (M.orientation t).1 * ((M.orientation t).1)ᵀ = 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) ℝ :=
+  ∂ₜ (fun s => (M.orientation s).1) t * ((M.orientation t).1)ᵀ
+
+lemma angularVelocityTensor_eq (M : RigidBodyMotion d) (t : Time) :
+    M.angularVelocityTensor t = ∂ₜ (fun s => (M.orientation s).1) t * ((M.orientation t).1)ᵀ :=
+  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 ℝ (fun s => (M.orientation s).1) t) :
+    (M.angularVelocityTensor t)ᵀ = - M.angularVelocityTensor t := by
+  have hconst : (fun s => (M.orientation s).1 * ((M.orientation s).1)ᵀ)
+      = fun _ => (1 : Matrix (Fin d) (Fin d) ℝ) := by
+    funext s
+    exact M.orientation_mul_transpose s
+  have hderiv0 : ∂ₜ (fun s => (M.orientation s).1 * ((M.orientation s).1)ᵀ) t = 0 := by
+    rw [hconst]
+    exact Time.deriv_const 1
+  have hprod := Time.deriv_matrix_mul (fun s => (M.orientation s).1)
+    (fun s => ((M.orientation s).1)ᵀ) t hR hR.matrix_transpose
+  rw [Time.deriv_matrix_transpose (fun s => (M.orientation s).1) 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 : (fun s => (M.orientation s).1) = fun _ => R.1 := by
+    funext s
+    rw [h]
+  rw [angularVelocityTensor_eq, hconst, Time.deriv_eq]
+  simp
+
+end RigidBodyMotion

Physlib/SpaceAndTime/Time/MatrixDerivatives.lean

@@ -0,0 +1,65 @@
+/-
+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. 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
+
+open Time Manifold Matrix
+open scoped RightActions
+
+attribute [local instance] Matrix.linftyOpNormedAddCommGroup Matrix.linftyOpNormedSpace
+  Matrix.linftyOpNormedRing Matrix.linftyOpNormedAlgebra
+
+variable {d : ℕ}
+
+/-- 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
+
+namespace Time
+
+/-- 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
+  let T : Matrix (Fin d) (Fin d) ℝ →L[ℝ] Matrix (Fin d) (Fin d) ℝ :=
+    (transposeLinearEquiv (Fin d) (Fin d) ℝ ℝ).toLinearMap.toContinuousLinearMap
+  have h : HasFDerivAt (fun s => (A s)ᵀ) (T.comp (fderiv ℝ A t)) t :=
+    T.hasFDerivAt.comp t hA.hasFDerivAt
+  rw [Time.deriv_eq, h.fderiv, Time.deriv_eq]
+  rfl
+
+end Time