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.ClassicalMechanics.RigidBody.Motion
public import Physlib.Mathematics.CrossProductMatrix
public import Physlib.SpaceAndTime.Time.MatrixDerivativesThe 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.
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.
The angular velocity can equally be expressed in the body frame: the moving coordinate system
rigidly attached to the body, with origin at the centre of mass and axes rotating with the body,
in which every material point has time-independent coordinates. The orientation R(t) is
precisely the rotational part of the change of frame: a point fixed at position a in the body
frame sits at r = R(t) a relative to the centre of mass in the lab frame (the inertial frame in
which the trajectories of RigidBodyMotion are written), and a vector with lab-frame components
u has body-frame components R(t)ᵀ u. The body frame is in general not inertial — it rotates
with the body, and its origin follows the (generally accelerating) centre of mass — but it is the
natural setting for the inertia tensor and Euler's equations, since the mass distribution, and
with it the inertia tensor, is time-independent in body-fixed axes.
The body-frame angular velocity tensor Ω_body(t) = R(t)ᵀ Ṙ(t) is defined directly from the
orientation, mirroring the spatial Ω = Ṙ Rᵀ rather than being derived from it — the two tensors
are the derivative Ṙ translated back to the identity from the two sides — and they are related
by conjugation, Ω_body = Rᵀ Ω R. The body-frame tensor is again skew-symmetric; in three
dimensions its dual is the body-frame angular velocity vector ω_body = Ω_bodyᵛ, the angular
velocity ω resolved along the body-fixed axes, ω_body = Rᵀ ω.
References
Landau and Lifshitz, Mechanics, Sections 31 and 32.
@[expose] public sectionattribute [local instance] Matrix.linftyOpNormedAddCommGroup Matrix.linftyOpNormedSpace
Matrix.linftyOpNormedRing Matrix.linftyOpNormedAlgebralemma 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.
d:ℕM:RigidBodyMotion dt:TimehR:DifferentiableAt ℝ (fun s => ↑(M.orientation s)) thconst:(fun s => ↑(M.orientation s) * (↑(M.orientation s))ᵀ) = fun x => 1hderiv0:∂ₜ (fun s => ↑(M.orientation s) * (↑(M.orientation s))ᵀ) t = 0hprod:0 =
↑(M.orientation t) * (∂ₜ (fun s => ↑(M.orientation s)) t)ᵀ +
∂ₜ (fun s => ↑(M.orientation s)) t * (↑(M.orientation t))ᵀ⊢ ↑(M.orientation t) * (∂ₜ (fun s => ↑(M.orientation s)) t)ᵀ =
-(∂ₜ (fun s => ↑(M.orientation s)) t * (↑(M.orientation t))ᵀ)
All goals completed! 🐙A rigid body whose orientation is constant in time has zero angular velocity.
d:ℕM:RigidBodyMotion dR:↥(specialOrthogonalGroup (Fin d) ℝ)h:M.orientation = fun x => Rt:Timehconst:(fun s => ↑(M.orientation s)) = fun x => ↑R⊢ (fderiv ℝ (fun x => ↑R) t) 1 * (↑(M.orientation t))ᵀ = 0 t
All goals completed! 🐙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.
All goals completed! 🐙A rigid body whose orientation is constant in time has zero angular velocity vector.
M:RigidBodyMotion 3R:↥(specialOrthogonalGroup (Fin 3) ℝ)h:M.orientation = fun x => Rt:Timei:Fin 3⊢ (0 t).crossProductVee i = 0 t i
M:RigidBodyMotion 3R:↥(specialOrthogonalGroup (Fin 3) ℝ)h:M.orientation = fun x => Rt:Time⊢ (0 t).crossProductVee ((fun i => i) ⟨0, ⋯⟩) = 0 t ((fun i => i) ⟨0, ⋯⟩)M:RigidBodyMotion 3R:↥(specialOrthogonalGroup (Fin 3) ℝ)h:M.orientation = fun x => Rt:Time⊢ (0 t).crossProductVee ((fun i => i) ⟨1, ⋯⟩) = 0 t ((fun i => i) ⟨1, ⋯⟩)M:RigidBodyMotion 3R:↥(specialOrthogonalGroup (Fin 3) ℝ)h:M.orientation = fun x => Rt:Time⊢ (0 t).crossProductVee ((fun i => i) ⟨2, ⋯⟩) = 0 t ((fun i => i) ⟨2, ⋯⟩) M:RigidBodyMotion 3R:↥(specialOrthogonalGroup (Fin 3) ℝ)h:M.orientation = fun x => Rt:Time⊢ (0 t).crossProductVee ((fun i => i) ⟨0, ⋯⟩) = 0 t ((fun i => i) ⟨0, ⋯⟩)M:RigidBodyMotion 3R:↥(specialOrthogonalGroup (Fin 3) ℝ)h:M.orientation = fun x => Rt:Time⊢ (0 t).crossProductVee ((fun i => i) ⟨1, ⋯⟩) = 0 t ((fun i => i) ⟨1, ⋯⟩)M:RigidBodyMotion 3R:↥(specialOrthogonalGroup (Fin 3) ℝ)h:M.orientation = fun x => Rt:Time⊢ (0 t).crossProductVee ((fun i => i) ⟨2, ⋯⟩) = 0 t ((fun i => i) ⟨2, ⋯⟩) All goals completed! 🐙
The time derivative of the orientation is Ṙ = Ω R, recovering the orientation path from its
angular velocity tensor Ω = Ṙ Rᵀ via the orthogonality Rᵀ R = 1.
All goals completed! 🐙
The rotational part of the velocity of the body point y is the cross product of the
angular velocity with the point's position relative to the centre of mass:
Ṙ(t) (y − c) = ω(t) × (displacement t y − comTrajectory t).
All goals completed! 🐙
The Landau–Lifshitz velocity decomposition v = V + ω × r for a rigid body in three
dimensions: the velocity of a body point is the centre-of-mass velocity plus the cross product of
the angular velocity with the point's position relative to the centre of mass.
All goals completed! 🐙lemma bodyAngularVelocityTensor_eq (M : RigidBodyMotion d) (t : Time) :
M.bodyAngularVelocityTensor t = ((M.orientation t).1)ᵀ * ∂ₜ (fun s => (M.orientation s).1) t :=
rfl
The time derivative of the orientation is Ṙ = R Ω_body, recovering the orientation path from
its body-frame angular velocity tensor via the orthogonality R Rᵀ = 1.
All goals completed! 🐙
The spatial tensor is the body-frame tensor rotated into the inertial frame,
Ω = R Ω_body Rᵀ.
All goals completed! 🐙
The body-frame tensor is the spatial tensor conjugated into the body frame,
Ω_body = Rᵀ Ω R.
All goals completed! 🐙
The body-frame angular velocity tensor is skew-symmetric, Ω_bodyᵀ = -Ω_body: it lies in the
Lie algebra 𝔰𝔬(d), inherited from the spatial tensor by conjugation.
All goals completed! 🐙lemma bodyAngularVelocity_eq (M : RigidBodyMotion 3) (t : Time) :
M.bodyAngularVelocity t = crossProductVee (M.bodyAngularVelocityTensor t) := rfl
The hat map recovers the body-frame angular velocity tensor from the body-frame angular
velocity vector, [ω_body]ₓ = Ω_body; it holds because Ω_body is skew-symmetric.
All goals completed! 🐙A rigid body whose orientation is constant in time has zero body-frame angular velocity tensor.
d:ℕM:RigidBodyMotion dR:↥(specialOrthogonalGroup (Fin d) ℝ)h:M.orientation = fun x => Rt:Timehconst:(fun s => ↑(M.orientation s)) = fun x => ↑R⊢ (↑(M.orientation t))ᵀ * (fderiv ℝ (fun x => ↑R) t) 1 = 0 t
All goals completed! 🐙A rigid body whose orientation is constant in time has zero body-frame angular velocity vector.
M:RigidBodyMotion 3R:↥(specialOrthogonalGroup (Fin 3) ℝ)h:M.orientation = fun x => Rt:Timei:Fin 3⊢ (0 t).crossProductVee i = 0 t i
M:RigidBodyMotion 3R:↥(specialOrthogonalGroup (Fin 3) ℝ)h:M.orientation = fun x => Rt:Time⊢ (0 t).crossProductVee ((fun i => i) ⟨0, ⋯⟩) = 0 t ((fun i => i) ⟨0, ⋯⟩)M:RigidBodyMotion 3R:↥(specialOrthogonalGroup (Fin 3) ℝ)h:M.orientation = fun x => Rt:Time⊢ (0 t).crossProductVee ((fun i => i) ⟨1, ⋯⟩) = 0 t ((fun i => i) ⟨1, ⋯⟩)M:RigidBodyMotion 3R:↥(specialOrthogonalGroup (Fin 3) ℝ)h:M.orientation = fun x => Rt:Time⊢ (0 t).crossProductVee ((fun i => i) ⟨2, ⋯⟩) = 0 t ((fun i => i) ⟨2, ⋯⟩) M:RigidBodyMotion 3R:↥(specialOrthogonalGroup (Fin 3) ℝ)h:M.orientation = fun x => Rt:Time⊢ (0 t).crossProductVee ((fun i => i) ⟨0, ⋯⟩) = 0 t ((fun i => i) ⟨0, ⋯⟩)M:RigidBodyMotion 3R:↥(specialOrthogonalGroup (Fin 3) ℝ)h:M.orientation = fun x => Rt:Time⊢ (0 t).crossProductVee ((fun i => i) ⟨1, ⋯⟩) = 0 t ((fun i => i) ⟨1, ⋯⟩)M:RigidBodyMotion 3R:↥(specialOrthogonalGroup (Fin 3) ℝ)h:M.orientation = fun x => Rt:Time⊢ (0 t).crossProductVee ((fun i => i) ⟨2, ⋯⟩) = 0 t ((fun i => i) ⟨2, ⋯⟩) All goals completed! 🐙
The rotational velocity written through the body-frame angular velocity,
Ṙ(t) v = R(t) (ω_body(t) × v): the derivative of the orientation acts as the body-frame angular
velocity ω_body crossed with v, rotated back into the inertial frame by R.
All goals completed! 🐙