The solid sphere as a rigid body

In this module we consider the solid sphere as a rigid body, and compute its mass, center of mass and inertia tensor.

noncomputable def RigidBody.solidSphere (d : ℕ) (m R : NNReal) : RigidBody d

The solid sphere as a rigid body.

Equations

• One or more equations did not get rendered due to their size.

theorem RigidBody.solidSphere_mass {d : ℕ} (m R : NNReal) (hr : R ≠ 0) : (solidSphere d.succ m R).mass = ↑m

theorem RigidBody.solidSphere_centerOfMass {d : ℕ} (m R : NNReal) (hr : R ≠ 0) : (solidSphere d.succ m R).centerOfMass = 0

The center of mass of a solid sphere located at the origin is 0.

theorem RigidBody.solidSphere_inertiaTensor (m R : NNReal) (hr : R ≠ 0) : (solidSphere 3 m R).inertiaTensor = (2 / 5 * ↑m * ↑R ^ 2) • 1

The moment of inertia tensor of a solid sphere through its center of mass is 2/5 m R^2 * I.