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.AngularMomentum
public import Physlib.ClassicalMechanics.RigidBody.AngularVelocity
public import Physlib.Mathematics.OrthogonalMatrixKinetic energy of a rigid body
For a rigid body rotating with angular velocity ω about its reference point the point at
position r has velocity ω × r, so its kinetic energy is T = ½ ∫ |ω × r|² dm. Since
|ω × r|² = ω · (r × (ω × r)) and the angular momentum is L = ∫ r × (ω × r) dm = I ω, the
kinetic energy is the quadratic form T = ½ ω · L = ½ ω · I ω in the inertia tensor.
For a rigid body in motion the total kinetic energy is the mass integral of half the squared
speed of its points, T = ½ ∫ ⟪v, v⟫ dm. König's theorem splits it into the kinetic energy of
the centre of mass plus the rotational energy about the centre of mass,
T = ½ M ⟪V, V⟫ + ½ ∫ |Ṙ (y − c)|² dm: the cross term vanishes because the first moment of the
mass distribution about its centre of mass is zero. In three dimensions the rotational term is
½ ∫ |ω × r|² dm, with ω the angular velocity vector and r the position of the body point
relative to the centre of mass.
The total kinetic energy is defined with the point velocity taken in the closed form
Ṙ(t) (y − c) + V(t) (velocityClosedForm), which is polynomial in the body point and hence
smooth for any motion; for differentiable motions it agrees with the honest point velocity
∂ₜ (displacement · y), recovering T = ½ ∫ ⟪v, v⟫ dm (kineticEnergy_eq_integral_velocity).
References
Landau and Lifshitz, Mechanics, Section 32.
@[expose] public sectionattribute [local instance] Matrix.linftyOpNormedAddCommGroup Matrix.linftyOpNormedSpace
Matrix.linftyOpNormedRing Matrix.linftyOpNormedAlgebra
The rotational kinetic energy is half the contraction of the angular velocity with the angular
momentum: T = ½ ω · L.
All goals completed! 🐙
The rotational kinetic energy equals the mass integral of the local rotational speed squared:
T = ½ ∫ |ω × r|² dm.
R:RigidBody 3ω:Fin 3 → ℝx:Space⊢ ∑ c, ContMDiffMap.coeFnAddMonoidHom (ω c • ⟨fun x => (crossProduct (x.val 3)) ((crossProduct ω) (x.val 3)) c, ⋯⟩) x =
⟨fun x => ∑ x_1, (crossProduct ω) (x.val 3) x_1 • (crossProduct ω) (x.val 3) x_1, ⋯⟩ x
R:RigidBody 3ω:Fin 3 → ℝx:Space⊢ ∑ x_1, ω x_1 * (crossProduct (x.val 3)) ((crossProduct ω) (x.val 3)) x_1 =
∑ x_1, (crossProduct ω) (x.val 3) x_1 * (crossProduct ω) (x.val 3) x_1
All goals completed! 🐙
For a differentiable motion the integrand of kineticEnergy is the squared speed of the
honest point velocity: T = ½ ∫ ⟪v, v⟫ dm with v = ∂ₜ (displacement · y).
d:ℕM:RigidBodyMotion dt:TimehR:Differentiable ℝ fun s => ↑(M.orientation s)hX:Differentiable ℝ M.comTrajectory⊢ 1 / 2 * M.ρ (cmap (fun y => ⟪M.velocityClosedForm t y, M.velocityClosedForm t y⟫_ℝ) ⋯) =
1 / 2 * M.ρ (cmap (fun y => ⟪M.velocity y t, M.velocity y t⟫_ℝ) ⋯)
d:ℕM:RigidBodyMotion dt:TimehR:Differentiable ℝ fun s => ↑(M.orientation s)hX:Differentiable ℝ M.comTrajectory⊢ cmap (fun y => ⟪M.velocityClosedForm t y, M.velocityClosedForm t y⟫_ℝ) ⋯ =
cmap (fun y => ⟪M.velocity y t, M.velocity y t⟫_ℝ) ⋯
d:ℕM:RigidBodyMotion dt:TimehR:Differentiable ℝ fun s => ↑(M.orientation s)hX:Differentiable ℝ M.comTrajectoryy:Space d⊢ (cmap (fun y => ⟪M.velocityClosedForm t y, M.velocityClosedForm t y⟫_ℝ) ⋯) y =
(cmap (fun y => ⟪M.velocity y t, M.velocity y t⟫_ℝ) ⋯) y
All goals completed! 🐙
The squared-speed integrand of kineticEnergy splits into the squared rotational speed
|Ṙ (y − c)|², a term linear in the body-frame coordinate y − c, and the constant squared
centre-of-mass speed ⟪V, V⟫.
d:ℕM:RigidBodyMotion dt:Timey:Space d⊢ (((∂ₜ (fun s => ↑(M.orientation s)) t *ᵥ fun j => y.val j - M.centerOfMass.val j) ⬝ᵥ
∂ₜ (fun s => ↑(M.orientation s)) t *ᵥ fun j => y.val j - M.centerOfMass.val j) +
(M.centerOfMassVelocity t).val ᵥ* ∂ₜ (fun s => ↑(M.orientation s)) t ⬝ᵥ fun j => y.val j - M.centerOfMass.val j) +
(((M.centerOfMassVelocity t).val ᵥ* ∂ₜ (fun s => ↑(M.orientation s)) t ⬝ᵥ fun j => y.val j - M.centerOfMass.val j) +
(M.centerOfMassVelocity t).val ⬝ᵥ (M.centerOfMassVelocity t).val) =
((∂ₜ (fun s => ↑(M.orientation s)) t *ᵥ fun j => y.val j - M.centerOfMass.val j) ⬝ᵥ
∂ₜ (fun s => ↑(M.orientation s)) t *ᵥ fun j => y.val j - M.centerOfMass.val j) +
∑ x,
2 * ((M.centerOfMassVelocity t).val ᵥ* ∂ₜ (fun s => ↑(M.orientation s)) t) x *
(y.val x - M.centerOfMass.val x) +
(M.centerOfMassVelocity t).val ⬝ᵥ (M.centerOfMassVelocity t).val
d:ℕM:RigidBodyMotion dt:Timey:Space d⊢ ∑ i,
(∂ₜ (fun s => ↑(M.orientation s)) t *ᵥ fun j => y.val j - M.centerOfMass.val j) i *
(∂ₜ (fun s => ↑(M.orientation s)) t *ᵥ fun j => y.val j - M.centerOfMass.val j) i +
∑ x, ((M.centerOfMassVelocity t).val ᵥ* ∂ₜ (fun s => ↑(M.orientation s)) t) x * (y.val x - M.centerOfMass.val x) +
(∑ x, ((M.centerOfMassVelocity t).val ᵥ* ∂ₜ (fun s => ↑(M.orientation s)) t) x * (y.val x - M.centerOfMass.val x) +
∑ i, (M.centerOfMassVelocity t).val i * (M.centerOfMassVelocity t).val i) =
∑ i,
(∂ₜ (fun s => ↑(M.orientation s)) t *ᵥ fun j => y.val j - M.centerOfMass.val j) i *
(∂ₜ (fun s => ↑(M.orientation s)) t *ᵥ fun j => y.val j - M.centerOfMass.val j) i +
(∑ x,
((M.centerOfMassVelocity t).val ᵥ* ∂ₜ (fun s => ↑(M.orientation s)) t) x * (y.val x - M.centerOfMass.val x) +
∑ x,
((M.centerOfMassVelocity t).val ᵥ* ∂ₜ (fun s => ↑(M.orientation s)) t) x * (y.val x - M.centerOfMass.val x)) +
∑ i, (M.centerOfMassVelocity t).val i * (M.centerOfMassVelocity t).val i
All goals completed! 🐙
König's theorem, general form: the total kinetic energy of a rigid body in motion splits
into the kinetic energy of the centre of mass plus the rotational energy about the centre of
mass, T = ½ M ⟪V, V⟫ + ½ ∫ |Ṙ (y − c)|² dm.
d:ℕM:RigidBodyMotion dt:Timeh:M.mass ≠ 0⊢ 1 / 2 *
(M.ρ
(cmap
(fun y =>
(∂ₜ (fun s => ↑(M.orientation s)) t *ᵥ fun j => y.val j - M.centerOfMass.val j) ⬝ᵥ
∂ₜ (fun s => ↑(M.orientation s)) t *ᵥ fun j => y.val j - M.centerOfMass.val j)
⋯) +
∑ x,
M.ρ
((2 * ((M.centerOfMassVelocity t).val ᵥ* ∂ₜ (fun s => ↑(M.orientation s)) t) x) •
cmap (fun y => y.val x - M.centerOfMass.val x) ⋯) +
M.ρ (⟪M.centerOfMassVelocity t, M.centerOfMassVelocity t⟫_ℝ • 1)) =
1 / 2 * M.mass * ⟪M.centerOfMassVelocity t, M.centerOfMassVelocity t⟫_ℝ +
1 / 2 *
M.ρ
(cmap
(fun y =>
(∂ₜ (fun s => ↑(M.orientation s)) t *ᵥ fun j => y.val j - M.centerOfMass.val j) ⬝ᵥ
∂ₜ (fun s => ↑(M.orientation s)) t *ᵥ fun j => y.val j - M.centerOfMass.val j)
⋯)
d:ℕM:RigidBodyMotion dt:Timeh:M.mass ≠ 0⊢ 1 / 2 *
(M.ρ
(cmap
(fun y =>
(∂ₜ (fun s => ↑(M.orientation s)) t *ᵥ fun j => y.val j - M.centerOfMass.val j) ⬝ᵥ
∂ₜ (fun s => ↑(M.orientation s)) t *ᵥ fun j => y.val j - M.centerOfMass.val j)
⋯) +
⟪M.centerOfMassVelocity t, M.centerOfMassVelocity t⟫_ℝ * M.mass) =
1 / 2 * M.mass * ⟪M.centerOfMassVelocity t, M.centerOfMassVelocity t⟫_ℝ +
1 / 2 *
M.ρ
(cmap
(fun y =>
(∂ₜ (fun s => ↑(M.orientation s)) t *ᵥ fun j => y.val j - M.centerOfMass.val j) ⬝ᵥ
∂ₜ (fun s => ↑(M.orientation s)) t *ᵥ fun j => y.val j - M.centerOfMass.val j)
⋯)
All goals completed! 🐙
König's theorem in three dimensions: the total kinetic energy of a rigid body in motion
splits as T = ½ M ⟪V, V⟫ + ½ ∫ |ω × r|² dm, with ω the angular velocity vector and
r = displacement − comTrajectory the position of the body point relative to the centre of
mass.
M:RigidBodyMotion 3t:Timeh:M.mass ≠ 0hR:DifferentiableAt ℝ (fun s => ↑(M.orientation s)) t⊢ 1 / 2 * M.mass * ⟪M.centerOfMassVelocity t, M.centerOfMassVelocity t⟫_ℝ +
1 / 2 *
M.ρ
(cmap
(fun y =>
(∂ₜ (fun s => ↑(M.orientation s)) t *ᵥ fun j => y.val 3 j - M.centerOfMass.val 3 j) ⬝ᵥ
∂ₜ (fun s => ↑(M.orientation s)) t *ᵥ fun j => y.val 3 j - M.centerOfMass.val 3 j)
⋯) =
1 / 2 * M.mass * ⟪M.centerOfMassVelocity t, M.centerOfMassVelocity t⟫_ℝ +
1 / 2 *
M.ρ
(cmap
(fun y =>
((crossProduct (M.angularVelocity t)) fun j =>
(M.displacement t y).val 3 j - (M.comTrajectory t).val 3 j) ⬝ᵥ
(crossProduct (M.angularVelocity t)) fun j => (M.displacement t y).val 3 j - (M.comTrajectory t).val 3 j)
⋯)
M:RigidBodyMotion 3t:Timeh:M.mass ≠ 0hR:DifferentiableAt ℝ (fun s => ↑(M.orientation s)) t⊢ 1 / 2 *
M.ρ
(cmap
(fun y =>
(∂ₜ (fun s => ↑(M.orientation s)) t *ᵥ fun j => y.val 3 j - M.centerOfMass.val 3 j) ⬝ᵥ
∂ₜ (fun s => ↑(M.orientation s)) t *ᵥ fun j => y.val 3 j - M.centerOfMass.val 3 j)
⋯) =
1 / 2 *
M.ρ
(cmap
(fun y =>
((crossProduct (M.angularVelocity t)) fun j => (M.displacement t y).val 3 j - (M.comTrajectory t).val 3 j) ⬝ᵥ
(crossProduct (M.angularVelocity t)) fun j => (M.displacement t y).val 3 j - (M.comTrajectory t).val 3 j)
⋯)
M:RigidBodyMotion 3t:Timeh:M.mass ≠ 0hR:DifferentiableAt ℝ (fun s => ↑(M.orientation s)) t⊢ cmap
(fun y =>
(∂ₜ (fun s => ↑(M.orientation s)) t *ᵥ fun j => y.val 3 j - M.centerOfMass.val 3 j) ⬝ᵥ
∂ₜ (fun s => ↑(M.orientation s)) t *ᵥ fun j => y.val 3 j - M.centerOfMass.val 3 j)
⋯ =
cmap
(fun y =>
((crossProduct (M.angularVelocity t)) fun j => (M.displacement t y).val 3 j - (M.comTrajectory t).val 3 j) ⬝ᵥ
(crossProduct (M.angularVelocity t)) fun j => (M.displacement t y).val 3 j - (M.comTrajectory t).val 3 j)
⋯
M:RigidBodyMotion 3t:Timeh:M.mass ≠ 0hR:DifferentiableAt ℝ (fun s => ↑(M.orientation s)) ty:Space⊢ (cmap
(fun y =>
(∂ₜ (fun s => ↑(M.orientation s)) t *ᵥ fun j => y.val 3 j - M.centerOfMass.val 3 j) ⬝ᵥ
∂ₜ (fun s => ↑(M.orientation s)) t *ᵥ fun j => y.val 3 j - M.centerOfMass.val 3 j)
⋯)
y =
(cmap
(fun y =>
((crossProduct (M.angularVelocity t)) fun j => (M.displacement t y).val 3 j - (M.comTrajectory t).val 3 j) ⬝ᵥ
(crossProduct (M.angularVelocity t)) fun j => (M.displacement t y).val 3 j - (M.comTrajectory t).val 3 j)
⋯)
y
All goals completed! 🐙
König's theorem in the body frame. The total kinetic energy M.kineticEnergy t, formed from
the lab-frame point velocities, splits at the centre of mass (centerOfMass = 0) as
T = ½ M ⟪V, V⟫ + rotationalKineticEnergy ω_body. The rotational energy is a frame-independent
scalar, so it is evaluated here from the body-frame angular velocity ω_body: the spatial form
|Ṙ (y − c)|² and the body form |ω_body × (y − c)|² agree because
Ṙ (y − c) = R (ω_body × (y − c)) and R, being orthogonal, preserves the norm.
All goals completed! 🐙