feat(ClassicalMechanics): add rotational kinetic energy and prove T = ½ω·Iω

Physlib.lean

@@ -21,6 +21,7 @@ public import Physlib.ClassicalMechanics.Pendulum.SlidingPendulum
 public import Physlib.ClassicalMechanics.RigidBody.AngularMomentum
 public import Physlib.ClassicalMechanics.RigidBody.AngularVelocity
 public import Physlib.ClassicalMechanics.RigidBody.Basic
+public import Physlib.ClassicalMechanics.RigidBody.KineticEnergy
 public import Physlib.ClassicalMechanics.RigidBody.Motion
 public import Physlib.ClassicalMechanics.RigidBody.SolidSphere
 public import Physlib.ClassicalMechanics.Scattering.RigidSphere

Physlib/ClassicalMechanics/RigidBody/KineticEnergy.lean

@@ -0,0 +1,56 @@
+/-
+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
+/-!
+
+# Rotational kinetic 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.
+
+## References
+- Landau and Lifshitz, Mechanics, Section 32.
+-/
+
+@[expose] public section
+
+open Manifold Matrix
+
+namespace RigidBody
+
+/-- The rotational kinetic energy of a rigid body rotating with angular velocity `ω` about its
+reference point: half the contraction of `ω` with the inertia tensor, `T = ½ ω · (I ω)`. -/
+noncomputable def rotationalKineticEnergy (R : RigidBody 3) (ω : Fin 3 → ℝ) : ℝ :=
+  (1 / 2) * (ω ⬝ᵥ R.inertiaTensor *ᵥ ω)
+
+/-- The rotational kinetic energy is half the contraction of the angular velocity with the angular
+momentum: `T = ½ ω · L`. -/
+lemma rotationalKineticEnergy_eq_angularMomentum (R : RigidBody 3) (ω : Fin 3 → ℝ) :
+    R.rotationalKineticEnergy ω = (1 / 2) * (ω ⬝ᵥ R.angularMomentum ω) := by
+  rw [rotationalKineticEnergy, angularMomentum_eq_inertiaTensor_mulVec]
+
+/-- The rotational kinetic energy equals the mass integral of the local rotational speed squared:
+`T = ½ ∫ |ω × r|² dm`. -/
+theorem rotationalKineticEnergy_eq_integral (R : RigidBody 3) (ω : Fin 3 → ℝ) :
+    R.rotationalKineticEnergy ω
+      = (1 / 2) * R.ρ ⟨fun x => (ω ⨯₃ (x : Fin 3 → ℝ)) ⬝ᵥ (ω ⨯₃ (x : Fin 3 → ℝ)),
+        ContDiff.contMDiff <| (contDiff_cross_dotProduct_cross ω).comp
+          (contDiff_pi.mpr fun i => Space.eval_contDiff i)⟩ := by
+  rw [rotationalKineticEnergy_eq_angularMomentum]
+  congr 1
+  simp_rw [dotProduct, angularMomentum, ← smul_eq_mul, ← map_smul, ← map_sum]
+  congr 1
+  ext x
+  rw [← ContMDiffMap.coeFnAddMonoidHom_apply, map_sum, Finset.sum_apply]
+  simp only [ContMDiffMap.coeFnAddMonoidHom_apply, ContMDiffMap.coe_smul, Pi.smul_apply,
+    ContMDiffMap.coeFn_mk, smul_eq_mul]
+  exact dotProduct_cross_cross_self (x : Fin 3 → ℝ) ω
+
+end RigidBody

Physlib/Mathematics/CrossProduct.lean

@@ -5,6 +5,7 @@ Authors: Giuseppe Sorge
 -/
 module
 
+public import Mathlib.Analysis.Calculus.ContDiff.Operations
 public import Mathlib.Data.Matrix.Mul
 public import Mathlib.Data.Real.Basic
 public import Mathlib.LinearAlgebra.CrossProduct
@@ -30,4 +31,19 @@ lemma cross_cross_self_apply (v w : Fin 3 → ℝ) (i : Fin 3) :
   simp only [Pi.sub_apply, Pi.smul_apply, smul_eq_mul, dotProduct, Fin.sum_univ_three]
   ring
 
+/-- Contracting `w` with the triple cross product `v ⨯₃ (w ⨯₃ v)` gives `(w ⨯₃ v) ⬝ᵥ (w ⨯₃ v)`
+(over `ℝ`, the squared length `|w × v|²`), by two cyclic permutations of the scalar triple
+product. -/
+lemma dotProduct_cross_cross_self {R : Type*} [CommRing R] (v w : Fin 3 → R) :
+    w ⬝ᵥ (v ⨯₃ (w ⨯₃ v)) = (w ⨯₃ v) ⬝ᵥ (w ⨯₃ v) := by
+  rw [triple_product_permutation, triple_product_permutation]
+
+/-- The squared length `(ω ⨯₃ v) ⬝ᵥ (ω ⨯₃ v)` of the cross product with a fixed vector `ω` is a
+smooth function of `v`. -/
+lemma contDiff_cross_dotProduct_cross (ω : Fin 3 → ℝ) :
+    ContDiff ℝ ⊤ fun v : Fin 3 → ℝ => (ω ⨯₃ v) ⬝ᵥ (ω ⨯₃ v) := by
+  simp only [dotProduct, Fin.sum_univ_three, cross_apply, Matrix.cons_val_zero,
+    Matrix.cons_val_one, Matrix.head_cons, Matrix.cons_val_two, Matrix.tail_cons]
+  fun_prop
+
 end Matrix