From 187a2400edc75e4eeab24c577dd87e0bfe001d7a Mon Sep 17 00:00:00 2001 From: Giuseppe Sorge Date: Fri, 3 Jul 2026 19:38:27 +0200 Subject: [PATCH 1/2] =?UTF-8?q?feat(ClassicalMechanics):=20add=20rigid-bod?= =?UTF-8?q?y=20angular=20momentum=20and=20prove=20L=20=3D=20I=CF=89?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit For a body rotating with angular velocity ω about its reference point, each point at r moves with velocity ω × r, so the angular momentum is L = ∫ r × (ω × r) dm. Expanding the double cross product (r × (ω × r) = |r|² ω − (r·ω) r) shows L = I ω: - RigidBody.angularMomentum ω, defined as the componentwise ρ of r × (ω × r) - Matrix.cross_cross_self_apply (Mathematics/CrossProductMatrix.lean): the general bac−cab expansion v ⨯₃ (w ⨯₃ v) = |v|² w − (v·w) v, kept in the general cross-product file rather than the classical-mechanics one - angularMomentum_eq_inertiaTensor_mulVec: L = inertiaTensor *ᵥ ω Toward #893. Co-Authored-By: Claude Fable 5 --- Physlib.lean | 1 + .../RigidBody/AngularMomentum.lean | 63 +++++++++++++++++++ Physlib/Mathematics/CrossProductMatrix.lean | 12 ++++ 3 files changed, 76 insertions(+) create mode 100644 Physlib/ClassicalMechanics/RigidBody/AngularMomentum.lean diff --git a/Physlib.lean b/Physlib.lean index 897c12407..b4c47de4c 100644 --- a/Physlib.lean +++ b/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 diff --git a/Physlib/ClassicalMechanics/RigidBody/AngularMomentum.lean b/Physlib/ClassicalMechanics/RigidBody/AngularMomentum.lean new file mode 100644 index 000000000..86daa5e37 --- /dev/null +++ b/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.CrossProductMatrix +/-! + +# 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 diff --git a/Physlib/Mathematics/CrossProductMatrix.lean b/Physlib/Mathematics/CrossProductMatrix.lean index 898d612eb..cc68d5f30 100644 --- a/Physlib/Mathematics/CrossProductMatrix.lean +++ b/Physlib/Mathematics/CrossProductMatrix.lean @@ -17,6 +17,9 @@ The hat map sends a vector `ω : Fin 3 → ℝ` to the skew-symmetric matrix `[ `[ω]ₓ *ᵥ v = ω ⨯₃ v`. It realises the correspondence between `ℝ³` and the skew-symmetric `3 × 3` matrices (the Lie algebra `𝖘𝖔(3)`), and underlies the angular velocity of a rigid body. +The file also records the component form of the triple (`bac−cab`) cross product `v ⨯₃ (w ⨯₃ v)`, +used to express the angular momentum of a rigid body. + -/ @[expose] public section @@ -67,4 +70,13 @@ lemma crossProductMatrix_crossProductVee {A : Matrix (Fin 3) (Fin 3) ℝ} (hA : | exact (h _ _).symm | exact (hdiag _).symm +/-- 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 From a3cd647c1d22c0e6104df6703dbdafe1a43efd6c Mon Sep 17 00:00:00 2001 From: Giuseppe Sorge Date: Mon, 6 Jul 2026 22:49:15 +0200 Subject: [PATCH 2/2] refactor(Mathematics): move cross_cross_self_apply to a new CrossProduct file Address review: keep CrossProductMatrix.lean focused on the hat map, and put the general triple-cross-product identity in its own file Physlib/Mathematics/CrossProduct.lean. AngularMomentum.lean now imports Physlib.Mathematics.CrossProduct. Co-authored-by: Claude Opus 4.8 --- Physlib.lean | 1 + .../RigidBody/AngularMomentum.lean | 2 +- Physlib/Mathematics/CrossProduct.lean | 33 +++++++++++++++++++ Physlib/Mathematics/CrossProductMatrix.lean | 12 ------- 4 files changed, 35 insertions(+), 13 deletions(-) create mode 100644 Physlib/Mathematics/CrossProduct.lean diff --git a/Physlib.lean b/Physlib.lean index b4c47de4c..7df28dc78 100644 --- a/Physlib.lean +++ b/Physlib.lean @@ -81,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 diff --git a/Physlib/ClassicalMechanics/RigidBody/AngularMomentum.lean b/Physlib/ClassicalMechanics/RigidBody/AngularMomentum.lean index 86daa5e37..7a0617407 100644 --- a/Physlib/ClassicalMechanics/RigidBody/AngularMomentum.lean +++ b/Physlib/ClassicalMechanics/RigidBody/AngularMomentum.lean @@ -6,7 +6,7 @@ Authors: Giuseppe Sorge module public import Physlib.ClassicalMechanics.RigidBody.Basic -public import Physlib.Mathematics.CrossProductMatrix +public import Physlib.Mathematics.CrossProduct /-! # Angular momentum of a rigid body diff --git a/Physlib/Mathematics/CrossProduct.lean b/Physlib/Mathematics/CrossProduct.lean new file mode 100644 index 000000000..02664bb17 --- /dev/null +++ b/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 diff --git a/Physlib/Mathematics/CrossProductMatrix.lean b/Physlib/Mathematics/CrossProductMatrix.lean index cc68d5f30..898d612eb 100644 --- a/Physlib/Mathematics/CrossProductMatrix.lean +++ b/Physlib/Mathematics/CrossProductMatrix.lean @@ -17,9 +17,6 @@ The hat map sends a vector `ω : Fin 3 → ℝ` to the skew-symmetric matrix `[ `[ω]ₓ *ᵥ v = ω ⨯₃ v`. It realises the correspondence between `ℝ³` and the skew-symmetric `3 × 3` matrices (the Lie algebra `𝖘𝖔(3)`), and underlies the angular velocity of a rigid body. -The file also records the component form of the triple (`bac−cab`) cross product `v ⨯₃ (w ⨯₃ v)`, -used to express the angular momentum of a rigid body. - -/ @[expose] public section @@ -70,13 +67,4 @@ lemma crossProductMatrix_crossProductVee {A : Matrix (Fin 3) (Fin 3) ℝ} (hA : | exact (h _ _).symm | exact (hdiag _).symm -/-- 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