Rigid bodies

A rigid body is one where the distance and relative orientation between particles does not change. In otherwords, 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" }