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.Basic
public import Physlib.SpaceAndTime.Time.Derivatives
public import Physlib.SpaceAndTime.Time.MatrixDerivatives
public import Mathlib.LinearAlgebra.UnitaryGroupRigid body motion
The static RigidBody records a body-fixed mass distribution. To describe a rigid body in
motion we record, in addition, the trajectory of its centre of mass in the inertial frame and the
body's time-dependent orientation (a rotation about the centre of mass).
From this configuration we define the velocity of the centre of mass and the body's linear momentum. The reference point is taken to be the centre of mass, following the decomposition of a rigid motion into a translation of the centre of mass plus a rotation about it.
References
Landau and Lifshitz, Mechanics, Section 32.
@[expose] public sectionattribute [local instance] Matrix.linftyOpNormedAddCommGroup Matrix.linftyOpNormedSpace
Matrix.linftyOpNormedRing Matrix.linftyOpNormedAlgebra
A motion of a rigid body in d-dimensional space: the body together with the inertial-frame
trajectory of its centre of mass and its time-dependent orientation (a rotation about the centre
of mass).
The position of the centre of mass in the inertial frame as a function of time.
The orientation of the body, a rotation about the centre of mass, as a function of time.
structure RigidBodyMotion (d : ℕ) extends RigidBody d where comTrajectory : Time → Space d orientation : Time → Matrix.specialOrthogonalGroup (Fin d) ℝ
The orientation matrix is special orthogonal, so R Rᵀ = 1.
lemma orientation_mul_transpose {d : ℕ} (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).1lemma centerOfMassVelocity_eq {d : ℕ} (M : RigidBodyMotion d) :
M.centerOfMassVelocity = ∂ₜ M.comTrajectory := rflA rigid body whose centre of mass is stationary has zero centre-of-mass velocity.
d:ℕM:RigidBodyMotion dc:Space dh:M.comTrajectory = fun x => c⊢ (∂ₜ fun x => c) = 0
d:ℕM:RigidBodyMotion dc:Space dh:M.comTrajectory = fun x => ct:Time⊢ ∂ₜ (fun x => c) t = 0 t
All goals completed! 🐙lemma linearMomentum_eq {d : ℕ} (M : RigidBodyMotion d) :
M.linearMomentum = fun t => M.mass • M.centerOfMassVelocity t := rflTODO "Define an action of the rotation and translation groups on `RigidBodyMotion`, and recover
`displacement` as the composite of those group actions."
The k-th coordinate of the rigid displacement applied to y.
lemma displacement_apply {d : ℕ} (M : RigidBodyMotion d) (t : Time) (y : Space d) (k : Fin d) :
M.displacement t y k =
(∑ j, (M.orientation t).val k j * (y j - M.centerOfMass j)) + M.comTrajectory t k := rfllemma displacement_contDiff {d : ℕ} (M : RigidBodyMotion d) (t : Time) :
ContDiff ℝ ⊤ (M.displacement t) := d:ℕM:RigidBodyMotion dt:Time⊢ ContDiff ℝ ⊤ (M.displacement t)
d:ℕM:RigidBodyMotion dt:Time⊢ ContDiff ℝ ⊤ fun y =>
{ val := fun k => ∑ j, ↑(M.orientation t) k j * (y.val j - M.centerOfMass.val j) + (M.comTrajectory t).val k }
All goals completed! 🐙
Rotating the body-frame position of y relative to the centre of mass gives its
inertial-frame position relative to the moving centre of mass:
R(t) (y − c) = displacement t y − comTrajectory t.
d:ℕM:RigidBodyMotion dt:Timey:Space dk:Fin d⊢ (↑(M.orientation t) *ᵥ fun j => y.val j - M.centerOfMass.val j) k + (M.comTrajectory t).val k =
∑ j, ↑(M.orientation t) k j * (y.val j - M.centerOfMass.val j) + (M.comTrajectory t).val k
All goals completed! 🐙
The motion preserves the total mass: the mass distribution at any time t has the same total
mass as the body.
@[simp]
lemma massDistribution_mass {d : ℕ} (M : RigidBodyMotion d) (t : Time) :
(M.massDistribution t).mass = M.mass := d:ℕM:RigidBodyMotion dt:Time⊢ (M.massDistribution t).mass = M.mass
d:ℕM:RigidBodyMotion dt:Time⊢ M.ρ (ContMDiffMap.comp ⟨fun x => 1, ⋯⟩ ⟨M.displacement t, ⋯⟩) = M.ρ ⟨fun x => 1, ⋯⟩
All goals completed! 🐙Evaluation commutes with finite sums of smooth functions.
private lemma contMDiffMap_sum_apply {d : ℕ} {ι : Type*} (s : Finset ι)
(f : ι → C^⊤⟮𝓘(ℝ, Space d), Space d; 𝓘(ℝ, ℝ), ℝ⟯) (y : Space d) :
(∑ j ∈ s, f j) y = ∑ j ∈ s, f j y := d:ℕι:Type u_1s:Finset ιf:ι → C^⊤⟮𝓘(ℝ, Space d), Space d; 𝓘(ℝ, ℝ), ℝ⟯y:Space d⊢ (∑ j ∈ s, f j) y = ∑ j ∈ s, (f j) y
classical
induction s using Finset.induction with
d:ℕι:Type u_1f:ι → C^⊤⟮𝓘(ℝ, Space d), Space d; 𝓘(ℝ, ℝ), ℝ⟯y:Space d⊢ (∑ j ∈ ∅, f j) y = ∑ j ∈ ∅, (f j) y All goals completed! 🐙
d:ℕι:Type u_1f:ι → C^⊤⟮𝓘(ℝ, Space d), Space d; 𝓘(ℝ, ℝ), ℝ⟯y:Space da:ιs:Finset ιha:a ∉ sih:(∑ j ∈ s, f j) y = ∑ j ∈ s, (f j) y⊢ (∑ j ∈ insert a s, f j) y = ∑ j ∈ insert a s, (f j) y
All goals completed! 🐙
The centre of mass of the moving mass distribution tracks the prescribed trajectory: for a
body of nonzero mass, the centre of mass of massDistribution M t is exactly comTrajectory t.
This is the decisive check that comTrajectory and orientation are wired correctly in
RigidBodyMotion.
All goals completed! 🐙lemma velocity_eq {d : ℕ} (M : RigidBodyMotion d) (y : Space d) (t : Time) :
M.velocity y t = ∂ₜ (fun s => M.displacement s y) t := rfl
The i-th component of the velocity of a body point is the time derivative of the i-th
coordinate of its inertial-frame trajectory.
d:ℕM:RigidBodyMotion dy:Space dt:Timei:Fin dhd:Differentiable ℝ fun s => M.displacement s y⊢ (∂ₜ (fun s => M.displacement s y) t).val i = ∂ₜ (fun s => (M.displacement s y).val i) t
All goals completed! 🐙
The material point at the centre of mass moves with the centre-of-mass velocity, for any
motion: v(centreOfMass) = V. This is the velocity counterpart of massDistribution_centerOfMass.
d:ℕM:RigidBodyMotion dt:Times:Timek:Fin d⊢ ∑ j, ↑(M.orientation s) k j * (M.centerOfMass.val j - M.centerOfMass.val j) + (M.comTrajectory s).val k =
(M.comTrajectory s).val k
All goals completed! 🐙
A rigid body in pure translation (constant orientation) has every point moving with the
centre-of-mass velocity: v = V.
All goals completed! 🐙
The velocity of a body point decomposes as v = Ṙ (y − c) + V: the rate of change of the
orientation acting on the body-frame position, plus the centre-of-mass velocity.
All goals completed! 🐙
The i-th coordinate of the closed-form velocity.
lemma velocityClosedForm_apply {d : ℕ} (M : RigidBodyMotion d) (t : Time) (y : Space d)
(i : Fin d) :
M.velocityClosedForm t y i
= (∂ₜ (fun s => (M.orientation s).1) t *ᵥ fun j => y j - M.centerOfMass j) i
+ M.centerOfMassVelocity t i := d:ℕM:RigidBodyMotion dt:Timey:Space di:Fin d⊢ (M.velocityClosedForm t y).val i =
(∂ₜ (fun s => ↑(M.orientation s)) t *ᵥ fun j => y.val j - M.centerOfMass.val j) i + (M.centerOfMassVelocity t).val i
All goals completed! 🐙
The closed-form velocity as a plain vector-valued function of the coordinates of y.
d:ℕM:RigidBodyMotion dt:Timey:Space di:Fin d⊢ (M.velocityClosedForm t y).val i =
(∂ₜ (fun s => ↑(M.orientation s)) t *ᵥ fun j => y.val j - M.centerOfMass.val j) i + (M.centerOfMassVelocity t).val i
All goals completed! 🐙For a differentiable motion the closed-form velocity is the honest point velocity.
All goals completed! 🐙The squared speed of a body point, in closed form, is a smooth function of the point.
lemma contDiff_velocityClosedForm_inner {d : ℕ} (M : RigidBodyMotion d) (t : Time) :
ContDiff ℝ ⊤ fun y : Space d => (⟪M.velocityClosedForm t y, M.velocityClosedForm t y⟫_ℝ) := d:ℕM:RigidBodyMotion dt:Time⊢ ContDiff ℝ ⊤ fun y => ⟪M.velocityClosedForm t y, M.velocityClosedForm t y⟫_ℝ
d:ℕM:RigidBodyMotion dt:Time⊢ ContDiff ℝ ⊤ fun y =>
∑ x,
(∑ x_1, ∂ₜ (fun s => ↑(M.orientation s)) t x x_1 * (y.val x_1 - M.centerOfMass.val x_1) +
(M.centerOfMassVelocity t).val x) *
(∑ x_1, ∂ₜ (fun s => ↑(M.orientation s)) t x x_1 * (y.val x_1 - M.centerOfMass.val x_1) +
(M.centerOfMassVelocity t).val x)
All goals completed! 🐙