feat(ClassicalMechanics): add rigid-body angular velocity tensor#1353
Conversation
Add `RigidBodyMotion.angularVelocityTensor`, the angular velocity tensor Ω(t) = Ṙ(t) R(t)ᵀ (Landau–Lifshitz §31), with its skew-symmetry litmus `angularVelocityTensor_transpose` (Ω ∈ 𝔰𝔬(d), obtained by differentiating R Rᵀ = 1) and `angularVelocityTensor_of_orientation_const` (a body of constant orientation has zero angular velocity). The general matrix-calculus tools this needs — a time-derivative product rule `Time.deriv_matrix_mul`, the transpose-commutes rule `Time.deriv_matrix_transpose`, and `Matrix.transposeCLM` — go in a new general file `SpaceAndTime/Time/MatrixDerivatives.lean` rather than the classical-mechanics file. Toward leanprover-community#893. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
|
Thank you for this PR, which will now be reviewed. If submitting to ./Physlib or ./QuantumInfo, please see our review guidelines if you are not familiar with the process. You should expect a back and forth with a reviewer before your PR is merged. See also that link for how to add appropriate labels to your PR. The PR will also go through a number of automated checks. You can learn more about these here, including how to run them locally. If you are submitting to ./PhyslibAlpha there will be a lighter review process, though your PR must still pass the automated checks. If you want to bring attention to this PR, please write a message on this thread of the Lean Zulip. Important: If a reviewer adds an |
jstoobysmith
left a comment
jstoobysmith
left a comment
There was a problem hiding this comment.
Some comments, but otherwise looks good.
| variable {d : ℕ} | ||
|
|
||
| /-- Transpose as a continuous linear map on square real matrices. -/ | ||
| noncomputable def transposeCLM : |
There was a problem hiding this comment.
If we can help it i wouldn't make this definition, I would just use what is already in Mathlib where needed
There was a problem hiding this comment.
Removed. The lemmas now use (Matrix.transposeLinearEquiv (Fin d) (Fin d) ℝ ℝ).toLinearMap.toContinuousLinearMap from Mathlib directly. Mathlib has no differentiability analogue of Continuous.matrix_transpose, so that step is a lemma (DifferentiableAt.matrix_transpose, stated for a general normed domain) rather than a definition.
|
|
||
| /-- The orientation of the body as a matrix-valued function of time: the underlying matrix of | ||
| `orientation`. -/ | ||
| noncomputable def orientationMatrix (M : RigidBodyMotion d) : Time → Matrix (Fin d) (Fin d) ℝ := |
There was a problem hiding this comment.
If you can get away without this, and just use (M.orientation s).1 everywhere, I think that would be better (it may even be shorter).
There was a problem hiding this comment.
Done - orientationMatrix is gone and everything is stated on (M.orientation s).1 directly. You were right, it is shorter: net -13 lines.
jstoobysmith
added
the
awaiting-author
…ular velocity Review changes for PR leanprover-community#1353: - drop Matrix.transposeCLM: the transpose lemmas now use Mathlib's transposeLinearEquiv, viewed as a continuous linear map, directly - drop RigidBodyMotion.orientationMatrix: everything is stated on (M.orientation s).1, with orientationMatrix_mul_transpose renamed to orientation_mul_transpose - add DifferentiableAt.matrix_transpose (Mathlib has only Continuous.matrix_transpose), stated for a general normed domain Toward leanprover-community#893. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
|
-awaiting-author |
github-actions
Bot
removed
the
awaiting-author
| variable {d : ℕ} | ||
|
|
||
| /-- The orientation matrix is special orthogonal, so `R Rᵀ = 1`. -/ | ||
| lemma orientation_mul_transpose (M : RigidBodyMotion d) (t : Time) : |
There was a problem hiding this comment.
One last thing, I would now move this to the file where orientation is defined (maybe the Basic.lean file)?
There was a problem hiding this comment.
Done - moved to Motion.lean, which is where the orientation field of RigidBodyMotion is defined (Basic.lean only has the static RigidBody, with no orientation).
jstoobysmith
added
the
awaiting-author
…orientation Review: the R Rᵀ = 1 lemma belongs in Motion.lean, where the orientation field of RigidBodyMotion is defined, not in AngularVelocity.lean. Toward leanprover-community#893. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
|
-awaiting-author |
github-actions
Bot
removed
the
awaiting-author
jstoobysmith
left a comment
jstoobysmith
left a comment
There was a problem hiding this comment.
Approved - looks good to me. Will merge shortly.
jstoobysmith
added
the
ready-to-merge
2 participants
Summary
Adds the angular velocity tensor of a rigid body in motion,
Ω(t) = Ṙ(t) R(t)ᵀwhereR(t) = orientation t(Landau–Lifshitz, Mechanics §31), building onRigidBodyMotionfrom #1320.New declarations in
Physlib/ClassicalMechanics/RigidBody/AngularVelocity.lean:RigidBodyMotion.orientationMatrix— the orientation as a matrix-valued function of time.RigidBodyMotion.angularVelocityTensor—Ω(t) = Ṙ(t) R(t)ᵀ.angularVelocityTensor_transpose— litmus test:Ωis skew-symmetric (Ωᵀ = -Ω, i.e.Ω ∈ 𝔰𝔬(d)), obtained by differentiating the orthogonality identityR Rᵀ = 1.angularVelocityTensor_of_orientation_const— a body of constant orientation hasΩ = 0.The supporting general matrix-calculus lemmas live in a new general file
Physlib/SpaceAndTime/Time/MatrixDerivatives.lean(kept out of the classical-mechanics file, per theAGENTS.md file-placement guideline):
Time.deriv_matrix_mul— product rule for∂ₜ (A * B).Time.deriv_matrix_transpose—∂ₜcommutes with transpose.Matrix.transposeCLM— transpose as a continuous linear map on square real matrices.The
d = 3angular-velocity vectorω(via the hat/vee map from #1324) and the identity[ω]ₓ = Ωare left to a follow-up.Toward #893.