feat(ClassicalMechanics): add the angular velocity vector of a rigid body

Physlib/ClassicalMechanics/RigidBody/API-map.yaml

@@ -8,6 +8,13 @@ Overview: |
     provides the body's total mass, centre of mass and inertia tensor, and works out the
     solid sphere as a concrete example.
 
+    A rigid body *in motion*, `RigidBodyMotion d`, additionally records the centre-of-mass
+    trajectory and the time-dependent orientation. From these the API builds the
+    centre-of-mass velocity and linear momentum, the rigid displacement and the moved mass
+    distribution, and the angular velocity — as the skew-symmetric tensor `Ω = Ṙ Rᵀ` in any
+    dimension and, in three dimensions, as the dual vector `ω` obtained from `Ω` via the hat
+    map.
+
 ParentAPIs:
   - Space (Physlib/SpaceAndTime/Space)
 
@@ -55,12 +62,14 @@ Requirements:
     location: N/A
 
   - description: The API contains the definition of the angular velocity of rotation of the rigid body.
-    done: false
-    location: N/A
+    done: true
+    location: >
+      Physlib/ClassicalMechanics/RigidBody/AngularVelocity.lean
+      (RigidBodyMotion.angularVelocityTensor, RigidBodyMotion.angularVelocity)
 
   - description: The API contains the definition of the velocity of the centre of mass of the rigid body.
-    done: false
-    location: N/A
+    done: true
+    location: Physlib/ClassicalMechanics/RigidBody/Motion.lean (RigidBodyMotion.centerOfMassVelocity)
 
   - description: The API contains the definition of the kinetic energy of the rigid body.
     done: false

Physlib/ClassicalMechanics/RigidBody/AngularVelocity.lean

@@ -6,6 +6,7 @@ Authors: Giuseppe Sorge
 module
 
 public import Physlib.ClassicalMechanics.RigidBody.Motion
+public import Physlib.Mathematics.CrossProductMatrix
 public import Physlib.SpaceAndTime.Time.MatrixDerivatives
 /-!
 
@@ -21,6 +22,10 @@ follows by differentiating the orthogonality identity `R Rᵀ = 1`. The general
 rules for time derivatives of matrices used for this live in
 `Physlib.SpaceAndTime.Time.MatrixDerivatives`.
 
+In three dimensions the skew-symmetric tensor `Ω` is dual to the *angular velocity vector*
+`ω(t) = Ωᵛ` via the hat map (`Physlib.Mathematics.CrossProductMatrix`), with `[ω]ₓ = Ω`; `ω` is the
+angular velocity proper, appearing in the decomposition `v = V + ω × r` as an honest cross product.
+
 ## References
 - Landau and Lifshitz, Mechanics, Section 31.
 -/
@@ -77,4 +82,31 @@ lemma angularVelocityTensor_of_orientation_const (M : RigidBodyMotion d)
   rw [angularVelocityTensor_eq, hconst, Time.deriv_eq]
   simp
 
+/-- The angular velocity *vector* `ω(t)` of a rigid body moving in three-dimensional space: the
+vector dual to the angular velocity tensor `Ω(t)` under the hat map, `ω = Ωᵛ`. It is the angular
+velocity `ω` in the Landau–Lifshitz decomposition `v = V + ω × r` of the velocity of a point of the
+body, where `ω × r` is the cross product with `ω`. -/
+noncomputable def angularVelocity (M : RigidBodyMotion 3) (t : Time) : Fin 3 → ℝ :=
+  crossProductVee (M.angularVelocityTensor t)
+
+lemma angularVelocity_eq (M : RigidBodyMotion 3) (t : Time) :
+    M.angularVelocity t = crossProductVee (M.angularVelocityTensor t) := rfl
+
+/-- The hat map recovers the angular velocity tensor from the angular velocity vector, `[ω]ₓ = Ω`.
+This is the defining relationship between the vector and tensor forms of the angular velocity in
+three dimensions; it holds because `Ω` is skew-symmetric. -/
+lemma crossProductMatrix_angularVelocity (M : RigidBodyMotion 3) (t : Time)
+    (hR : DifferentiableAt ℝ (fun s => (M.orientation s).1) t) :
+    crossProductMatrix (M.angularVelocity t) = M.angularVelocityTensor t := by
+  rw [angularVelocity_eq,
+    crossProductMatrix_crossProductVee (M.angularVelocityTensor_transpose t hR)]
+
+/-- A rigid body whose orientation is constant in time has zero angular velocity vector. -/
+lemma angularVelocity_of_orientation_const (M : RigidBodyMotion 3)
+    (R : Matrix.specialOrthogonalGroup (Fin 3) ℝ) (h : M.orientation = fun _ => R) :
+    M.angularVelocity = 0 := by
+  funext t i
+  rw [angularVelocity_eq, congrFun (M.angularVelocityTensor_of_orientation_const R h) t]
+  fin_cases i <;> simp [crossProductVee]
+
 end RigidBodyMotion

Physlib/Mathematics/CrossProductMatrix.lean

@@ -53,4 +53,18 @@ lemma crossProductVee_crossProductMatrix (ω : Fin 3 → ℝ) :
   funext i
   fin_cases i <;> simp [crossProductVee, crossProductMatrix]
 
+/-- On skew-symmetric matrices the hat map is also a right inverse of the vee map: if `Aᵀ = -A`
+then `[Aᵛ]ₓ = A`. Together with `crossProductVee_crossProductMatrix` this identifies `ℝ³` with the
+skew-symmetric `3 × 3` matrices `𝖘𝖔(3)`. -/
+lemma crossProductMatrix_crossProductVee {A : Matrix (Fin 3) (Fin 3) ℝ} (hA : Aᵀ = -A) :
+    crossProductMatrix (crossProductVee A) = A := by
+  have h : ∀ i j, A i j = - A j i := fun i j => by
+    simpa using congrFun (congrFun hA j) i
+  have hdiag : ∀ i, A i i = 0 := fun i => CharZero.eq_neg_self_iff.mp (h i i)
+  ext i j
+  fin_cases i <;> fin_cases j <;> simp [crossProductVee, crossProductMatrix] <;>
+    first
+      | exact (h _ _).symm
+      | exact (hdiag _).symm
+
 end Matrix