feat(ClassicalMechanics): add rigid-body angular momentum and prove L = Iω

Physlib.lean

@@ -17,6 +17,7 @@ public import Physlib.ClassicalMechanics.OrbitalMechanics.VisViva
 public import Physlib.ClassicalMechanics.Pendulum.CoplanarDoublePendulum
 public import Physlib.ClassicalMechanics.Pendulum.MiscellaneousPendulumPivotMotions
 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.Motion
@@ -80,6 +81,7 @@ public import Physlib.Mathematics.Calculus.ParametricIntegration
 public import Physlib.Mathematics.Calculus.Wirtinger.Basic
 public import Physlib.Mathematics.Calculus.Wirtinger.Coordinate
 public import Physlib.Mathematics.ConjModule
+public import Physlib.Mathematics.CrossProduct
 public import Physlib.Mathematics.CrossProductMatrix
 public import Physlib.Mathematics.DataStructures.FourTree.Basic
 public import Physlib.Mathematics.DataStructures.FourTree.UniqueMap

Physlib/ClassicalMechanics/RigidBody/AngularMomentum.lean

@@ -0,0 +1,63 @@
+/-
+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.Basic
+public import Physlib.Mathematics.CrossProduct
+/-!
+
+# Angular momentum of a rigid body
+
+For a rigid body rotating with angular velocity `ω` about its reference point, each body point at
+position `r` moves with velocity `ω × r`, so the body's angular momentum about that point is
+`L = ∫ r × (ω × r) dm`. Expanding the double cross product,
+`r × (ω × r) = |r|² ω − (r · ω) r`, shows that `L` is linear in `ω` with matrix the inertia tensor:
+`L = I ω`.
+
+## References
+- Landau and Lifshitz, Mechanics, Section 32.
+-/
+
+@[expose] public section
+
+open Manifold Matrix
+
+namespace RigidBody
+
+/-- The angular momentum `L = ∫ r × (ω × r) dm` of a rigid body rotating with angular velocity `ω`
+about its reference point (each body point at `r` moving with velocity `ω × r`). Its `i`-th
+component is `ρ` applied to the scalar field `[r × (ω × r)]ᵢ`. -/
+noncomputable def angularMomentum (R : RigidBody 3) (ω : Fin 3 → ℝ) : Fin 3 → ℝ := fun i =>
+  R.ρ ⟨fun x => ((x : Fin 3 → ℝ) ⨯₃ (ω ⨯₃ (x : Fin 3 → ℝ))) i, ContDiff.contMDiff <| by
+    have h : (fun x : Space 3 => ((x : Fin 3 → ℝ) ⨯₃ (ω ⨯₃ (x : Fin 3 → ℝ))) i)
+        = fun x => (∑ k, (x k) ^ 2) * ω i - (∑ j, x j * ω j) * x i :=
+      funext fun x => cross_cross_self_apply (x : Fin 3 → ℝ) ω i
+    rw [h]; fun_prop⟩
+
+/-- The angular momentum of a rigid body equals its inertia tensor applied to the angular velocity:
+`L = I ω`. -/
+theorem angularMomentum_eq_inertiaTensor_mulVec (R : RigidBody 3) (ω : Fin 3 → ℝ) :
+    R.angularMomentum ω = R.inertiaTensor *ᵥ ω := by
+  funext i
+  simp only [angularMomentum, mulVec, dotProduct, inertiaTensor]
+  have hsmul : ∀ j : Fin 3,
+      R.ρ ⟨fun x => (if i = j then 1 else 0) * ∑ k, (x k) ^ 2 - x i * x j,
+        ContDiff.contMDiff <| by fun_prop⟩ * ω j
+      = R.ρ (ω j • ⟨fun x => (if i = j then 1 else 0) * ∑ k, (x k) ^ 2 - x i * x j,
+        ContDiff.contMDiff <| by fun_prop⟩) := by
+    intro j
+    rw [map_smul, smul_eq_mul, mul_comm]
+  rw [Finset.sum_congr rfl (fun j _ => hsmul j), ← map_sum]
+  congr 1
+  ext x
+  simp only [ContMDiffMap.coeFn_mk]
+  rw [cross_cross_self_apply, ← 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]
+  fin_cases i <;> simp [Fin.sum_univ_three] <;> ring
+
+end RigidBody

Physlib/Mathematics/CrossProduct.lean

@@ -0,0 +1,33 @@
+/-
+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 Mathlib.Data.Matrix.Mul
+public import Mathlib.Data.Real.Basic
+public import Mathlib.LinearAlgebra.CrossProduct
+/-!
+
+# The cross product of three-dimensional vectors
+
+Identities for the cross product `⨯₃` on `Fin 3 → ℝ`, beyond those already in Mathlib, used in the
+formalisation of rigid-body dynamics.
+
+-/
+
+@[expose] public section
+
+namespace Matrix
+
+/-- The component form of the triple cross product `v ⨯₃ (w ⨯₃ v)`: by the `bac−cab` identity its
+`i`-th entry is `|v|² wᵢ − (v · w) vᵢ`, written with the explicit component sums `∑ k, (v k)²` and
+`∑ j, v j * w j`. -/
+lemma cross_cross_self_apply (v w : Fin 3 → ℝ) (i : Fin 3) :
+    (v ⨯₃ (w ⨯₃ v)) i = (∑ k, (v k) ^ 2) * w i - (∑ j, v j * w j) * v i := by
+  rw [cross_cross_eq_smul_sub_smul']
+  simp only [Pi.sub_apply, Pi.smul_apply, smul_eq_mul, dotProduct, Fin.sum_univ_three]
+  ring
+
+end Matrix