Rigid bodies

A rigid body is one where the distance and relative orientation between particles does not change. In other words, the body remains undeformed.

In this module we will define the basic properties of a rigid body, including

• mass
• center of mass
• inertia tensor

References

• Landau and Lifshitz, Mechanics, page 100, Section 32

structure RigidBody (d : ℕ) : Type

A Rigid body defined by its mass distribution.

• ρ : ContMDiffMap (modelWithCornersSelf ℝ (Space d)) (modelWithCornersSelf ℝ ℝ) (Space d) ℝ ⊤ →ₗ[ℝ] ℝ

  The mass distribution of the rigid body.

def RigidBody.mass {d : ℕ} (R : RigidBody d) : ℝ

The total mass of the rigid body.

Equations

• R.mass = R.ρ ⟨fun (x : Space d) => 1, ⋯⟩

noncomputable def RigidBody.centerOfMass {d : ℕ} (R : RigidBody d) : Space d

The center of mass of the rigid body.

Equations

• R.centerOfMass i = (1 / R.mass) • R.ρ ⟨fun (x : Space d) => x i, ⋯⟩

noncomputable def RigidBody.inertiaTensor {d : ℕ} (R : RigidBody d) : Matrix (Fin d) (Fin d) ℝ

The inertia tensor of the rigid body.

Equations

• R.inertiaTensor i j = R.ρ ⟨fun (x : Space d) => (if i = j then 1 else 0) * ∑ k : Fin d, x k ^ 2 - x i * x j, ⋯⟩

theorem RigidBody.inertiaTensor_symmetric {d : ℕ} (R : RigidBody d) (i j : Fin d) : R.inertiaTensor i j = R.inertiaTensor j i

def RigidBody.kineticEnergy : InformalDefinition

The kinetic energy of a rigid body.

Equations

• RigidBody.kineticEnergy = { deps := [`RigidBody], tag := "MEYBM" }

def RigidBody.coordinate_system : InformalDefinition

One can describe the motion of rigid body with a fixed (inertial) coordinate system (X,Y,Z) and a moving system (x₁,x₂,x₃) rigidly attached to the body.

Equations

• RigidBody.coordinate_system = { deps := [`RigidBody], tag := "LL31.3" }

def RigidBody.rigid_body_dof : InformalLemma

A rigid body in three-dimensional space has six degrees of freedom: three translational (for the position of its centre of mass) and three rotational (for its orientation).

Equations

• RigidBody.rigid_body_dof = { deps := [`RigidBody], tag := "LL32-6DF" }

def RigidBody.velocity_decomposition : InformalLemma

The velocity v of any point in a rigid body is v = V + Ω × r, where V is the velocity of the origin of the moving system and Ω is the angular velocity.

Equations

• RigidBody.velocity_decomposition = { deps := [`RigidBody], tag := "LL31.L3" }

def RigidBody.angular_velocity_is_well_defined : InformalLemma

The angular velocity of rotation of a rigid body from a system of coordinates fixed in the body is independent of the system chosen.

Equations

• RigidBody.angular_velocity_is_well_defined = { deps := [`RigidBody], tag := "LL32-AM" }

def RigidBody.decomposition_of_motion : InformalLemma

The motion of a rigid body can be decomposed into a translation of some reference point plus a rotation about that point. There exists a time-dependent vector V(t) and angular velocity ω(t) such that v(r) = V + ω × r, where r is measured from the reference point.

Equations

• RigidBody.decomposition_of_motion = { deps := [`RigidBody], tag := "LL32-DM" }

def RigidBody.center_of_mass_point_moves_as_particle : InformalLemma

The centre of mass of a rigid body moves as if all mass were concentrated at that point and acted upon by the resultant external force: M a_CM = ∑ F_ext.

Equations

• RigidBody.center_of_mass_point_moves_as_particle = { deps := [`RigidBody], tag := "LL32-CM" }

def RigidBody.angular_momentum_about_point : InformalLemma

The total angular momentum about a point O is L = ∫ r × v dm. With v = V + ω × r about the centre of mass, L = R × (M V) + I_CM ω, where R is the centre of mass position.

Equations

• RigidBody.angular_momentum_about_point = { deps := [`RigidBody], tag := "LL32-L" }

def RigidBody.translational_equation_inertial : InformalLemma

In the inertial frame, the translational equation of motion of a rigid body is given by dP/dt = F, where P is the total linear momentum and F is the total external force acting on the body.

Equations

• RigidBody.translational_equation_inertial = { deps := [`RigidBody], tag := "LL32-TR" }

def RigidBody.rotational_equation_inertial : InformalLemma

In the inertial frame, the rotational equation of motion of a rigid body about the center of mass is given by dM/dt = K, where M is the total angular momentum and K is the total external torque.

Equations

• RigidBody.rotational_equation_inertial = { deps := [`RigidBody], tag := "LL32-ROT" }

def RigidBody.kinetic_energy_decomposition : InformalLemma

The kinetic energy decomposes into translational and rotational parts: T = (1/2) M |V|² + (1/2) ω ⋅ I_CM ω. Here V is the velocity of the centre of mass and I_CM is the inertia tensor about that point.

Equations

• RigidBody.kinetic_energy_decomposition = { deps := [`RigidBody], tag := "LL32-TK" }

def RigidBody.parallel_axis_theorem : InformalLemma

If I_O is the inertia tensor about a point O, then the inertia tensor about a parallel point O' displaced by a is I_{O'} = I_O + M(|a|² 1 − a ⊗ a). This is the parallel-axis theorem.

Equations

• RigidBody.parallel_axis_theorem = { deps := [`RigidBody], tag := "LL32-PA" }

def RigidBody.principal_axes_of_inertia : InformalDefinition

Because the inertia tensor is real symmetric, there exists an orthonormal basis of principal axes in which it is diagonal. The corresponding directions are the principal axes of inertia.

Equations

• RigidBody.principal_axes_of_inertia = { deps := [`RigidBody], tag := "LL32-PAE" }

def RigidBody.principal_axes_of_inertia_bound : InformalLemma

None of the principal moments of inertia can exceed the sum of other two.

Equations

• RigidBody.principal_axes_of_inertia_bound = { deps := [`RigidBody], tag := "LL32-PAEB" }

def RigidBody.asymmetrical_top : InformalDefinition

An asymmetrical top is when none of the principal moments of inertia are equal.

Equations

• RigidBody.asymmetrical_top = { deps := [`RigidBody], tag := "LL32-AST" }

def RigidBody.symmetrical_top : InformalDefinition

A symmetrical top is when only two of the principal moments of inertia are equal.

Equations

• RigidBody.symmetrical_top = { deps := [`RigidBody], tag := "LL32-ST" }

def RigidBody.spherical_top : InformalDefinition

A spherical top is when all three of the principal moments of inertia are equal.

Equations

• RigidBody.spherical_top = { deps := [`RigidBody], tag := "LL32-SPT" }

def RigidBody.RotatingFrame : InformalDefinition

A rotating body-fixed frame is a coordinate system attached to the body that rotates with the body relative to an inertial (fixed) frame. The frame is characterised by its angular velocity vector Ω(t).

Equations

• RigidBody.RotatingFrame = { deps := [`RigidBody], tag := "LL32-RF" }

def RigidBody.rotating_frame_derivative : InformalDefinition

The time derivative in the rotating frame, d'/dt, is the derivative of the components of a vector with respect to time when expressed in the rotating (body-fixed) frame.

Equations

• RigidBody.rotating_frame_derivative = { deps := [`RigidBody], tag := "LL32-dprime" }

def RigidBody.transport_law_inertial_rotating : InformalLemma

For any vector field A(t), its inertial-frame time derivative equals the rotating-frame derivative plus the contribution from the frame rotation: (dA/dt)_inertial = (dA/dt)_rotating + Ω × A. Here Ω is the angular velocity of the rotating frame.

Equations

• RigidBody.transport_law_inertial_rotating = { deps := [`RigidBody], tag := "LL36-Ltransport" }

def RigidBody.transport_law_for_momentum : InformalLemma

For linear momentum, the relation between inertial and rotating derivatives is (dP/dt)_inertial = d'P/dt + Ω × P. So, d'P/dt + Ω × P = F which is the linear-momentum equation in the rotating frame.

Equations

• RigidBody.transport_law_for_momentum = { deps := [`RigidBody], tag := "LL32-transportP" }

def RigidBody.transport_law_for_angular_momentum : InformalLemma

For angular momentum, the relation between inertial and rotating derivatives is (dM/dt)_inertial = d'M/dt + Ω × M, and with the rotational form of Newton's law M_tot = (dM/dt)_inertial this yields d'M/dt + Ω × M = K, the angular-momentum equation in the rotating frame.

Equations

• RigidBody.transport_law_for_angular_momentum = { deps := [`RigidBody], tag := "LL32-transportM" }

def RigidBody.euler_equations : InformalLemma

When motion is described in body-fixed principal axes (I₁, I₂, I₃ diagonal), the equations of rotational motion (Euler’s equations) are: I₁ dω₁/dt + (I₃ − I₂) ω₂ ω₃ = M₁, with cyclic permutations. M is the external torque about the centre of mass.

Equations

• RigidBody.euler_equations = { deps := [`RigidBody], tag := "LL32-EQ" }

def RigidBody.steady_rotation_conditions : InformalLemma

A rigid body can perform steady (uniform) rotation about any principal axis if the torque about that axis vanishes. Stability depends on the ordering of principal moments.

Equations

• RigidBody.steady_rotation_conditions = { deps := [`RigidBody], tag := "LL32-SR" }

def RigidBody.intermediate_axis_instability : InformalLemma

Rotations about the largest and smallest principal axes are stable under small perturbations; rotation about the intermediate axis is unstable (tennis-racket effect).

Equations

• RigidBody.intermediate_axis_instability = { deps := [`RigidBody], tag := "LL32-IAI" }

def RigidBody.reduction_to_two_body : InformalLemma

If a rigid body is confined to planar motion, its dynamics reduce to a two-dimensional problem: the inertia reduces to a scalar moment and rotation is described by a single angular velocity.

Equations

• RigidBody.reduction_to_two_body = { deps := [`RigidBody], tag := "LL32-RTB" }

def RigidBody.rigid_body_work_and_power : InformalLemma

The power delivered to a rigid body by forces is P = ∑ Fᵢ ⋅ vᵢ = F_tot ⋅ V + M ⋅ ω, where F_tot is total force, V the reference point velocity, and M the torque. Translational and rotational contributions separate.

Equations

• RigidBody.rigid_body_work_and_power = { deps := [`RigidBody], tag := "LL32-WP" }

def RigidBody.small_oscillations_about_equilibrium : InformalLemma

Small oscillations about a stable equilibrium orientation are governed by linearised equations obtained by expanding energy to second order in angular displacements. Normal modes and frequencies depend on inertia and restoring torques.

Equations

• RigidBody.small_oscillations_about_equilibrium = { deps := [`RigidBody], tag := "LL32-SO" }