feat(ReferenceFrame): velocity of a trajectory in a frame via derivVec

Physlib.lean

@@ -483,7 +483,8 @@ public import Physlib.Relativity.Tensors.TensorSpecies.Basic
 public import Physlib.Relativity.Tensors.Tensorial
 public import Physlib.Relativity.Tensors.UnitTensor
 public import Physlib.SpaceAndTime.GalileanGroup.Basic
-public import Physlib.SpaceAndTime.ReferenceFrame
+public import Physlib.SpaceAndTime.ReferenceFrame.Basic
+public import Physlib.SpaceAndTime.ReferenceFrame.Velocity
 public import Physlib.SpaceAndTime.Space.Basic
 public import Physlib.SpaceAndTime.Space.ConstantSliceDist
 public import Physlib.SpaceAndTime.Space.CrossProduct

Physlib/SpaceAndTime/ReferenceFrame/API-map.yaml

@@ -41,69 +41,77 @@ Requirements:
 
   - description: "The key data structure `ReferenceFrame d`, recording an affine origin and a displacement basis at each time, is defined."
     done: true
-    location: "Physlib/SpaceAndTime/ReferenceFrame.lean (ReferenceFrame, ReferenceFrame.origin, ReferenceFrame.basis)"
+    location: "Physlib/SpaceAndTime/ReferenceFrame/Basic.lean (ReferenceFrame, ReferenceFrame.origin, ReferenceFrame.basis)"
 
   - description: "The API contains a construction of a frame from the trajectories of a collection of reference points forming an affine basis at each time."
     done: true
-    location: "Physlib/SpaceAndTime/ReferenceFrame.lean (ReferenceFrame.fromReferencePoints)"
+    location: "Physlib/SpaceAndTime/ReferenceFrame/Basic.lean (ReferenceFrame.fromReferencePoints)"
 
   - description: "The API contains the condition that a frame induces the same inner product on coordinates at every time."
     done: true
-    location: "Physlib/SpaceAndTime/ReferenceFrame.lean (ReferenceFrame.IsMetricConserved)"
+    location: "Physlib/SpaceAndTime/ReferenceFrame/Basic.lean (ReferenceFrame.IsMetricConserved)"
 
   - description: "The API contains the condition that a frame's axes are orthonormal at every time, the result that such a frame conserves its coordinate metric, and the instance making that available to typeclass inference."
     done: true
-    location: "Physlib/SpaceAndTime/ReferenceFrame.lean (ReferenceFrame.Orthonormal, Orthonormal.isMetricConserved, Fact frame.IsMetricConserved)"
+    location: "Physlib/SpaceAndTime/ReferenceFrame/Basic.lean (ReferenceFrame.Orthonormal, Orthonormal.isMetricConserved, Fact frame.IsMetricConserved)"
 
   - description: "The API contains the condition for a frame to be inertial, namely that its origin moves with constant velocity and its axes are the same at every time."
     done: true
-    location: "Physlib/SpaceAndTime/ReferenceFrame.lean (ReferenceFrame.IsInertial, origin_moves_uniformly, basis_conserved)"
+    location: "Physlib/SpaceAndTime/ReferenceFrame/Basic.lean (ReferenceFrame.IsInertial, origin_moves_uniformly, basis_conserved)"
 
   - description: "The API contains the constant velocity of an inertial frame's origin."
     done: true
-    location: "Physlib/SpaceAndTime/ReferenceFrame.lean (IsInertial.velocity)"
+    location: "Physlib/SpaceAndTime/ReferenceFrame/Basic.lean (IsInertial.velocity)"
 
   - description: "The API contains the result that an inertial frame conserves its coordinate metric, and the instance making that available to typeclass inference."
     done: true
-    location: "Physlib/SpaceAndTime/ReferenceFrame.lean (IsInertial.isMetricConserved, Fact frame.IsMetricConserved)"
+    location: "Physlib/SpaceAndTime/ReferenceFrame/Basic.lean (IsInertial.isMetricConserved, Fact frame.IsMetricConserved)"
 
   - description: "The API contains the carrier `frame.Vector` for the components of a vector quantity measured relative to a frame, together with its equivalence to coordinate tuples."
     done: true
-    location: "Physlib/SpaceAndTime/ReferenceFrame.lean (ReferenceFrame.Vector, components, componentEquiv, componentLinearEquiv)"
+    location: "Physlib/SpaceAndTime/ReferenceFrame/Basic.lean (ReferenceFrame.Vector, components, componentEquiv, componentLinearEquiv)"
 
   - description: "The API contains the additive and scalar structure on frame vectors, inherited componentwise."
     done: true
-    location: "Physlib/SpaceAndTime/ReferenceFrame.lean (AddCommGroup frame.Vector, Module ℝ frame.Vector)"
+    location: "Physlib/SpaceAndTime/ReferenceFrame/Basic.lean (AddCommGroup frame.Vector, Module ℝ frame.Vector)"
 
   - description: "The API contains the identification of a frame vector with a geometric displacement in space at a given time, through the frame's basis, in both linear and continuous linear form."
     done: true
-    location: "Physlib/SpaceAndTime/ReferenceFrame.lean (dispEquiv, contDispEquiv)"
+    location: "Physlib/SpaceAndTime/ReferenceFrame/Basic.lean (dispEquiv, contDispEquiv)"
 
   - description: "The API contains the topology on frame vectors, its continuous linear equivalence with coordinate tuples, and finite dimensionality."
     done: true
-    location: "Physlib/SpaceAndTime/ReferenceFrame.lean (componentContLinearEquiv, TopologicalSpace frame.Vector, FiniteDimensional ℝ frame.Vector)"
+    location: "Physlib/SpaceAndTime/ReferenceFrame/Basic.lean (componentContLinearEquiv, TopologicalSpace frame.Vector, FiniteDimensional ℝ frame.Vector)"
 
   - description: "The API contains the norm and inner product on frame vectors of a frame with conserved coordinate metric, pulled back through the frame basis from geometric displacement space, so that a displacement keeps its length and its angles when the axes are skew or unequally scaled."
     done: true
-    location: "Physlib/SpaceAndTime/ReferenceFrame.lean (NormedAddCommGroup frame.Vector, InnerProductSpace ℝ frame.Vector)"
+    location: "Physlib/SpaceAndTime/ReferenceFrame/Basic.lean (NormedAddCommGroup frame.Vector, InnerProductSpace ℝ frame.Vector)"
 
   - description: "The API contains the Euclidean component formulas for the norm and inner product in an orthonormal frame."
     done: true
-    location: "Physlib/SpaceAndTime/ReferenceFrame.lean (norm_euclidean_if_orthonormal, inner_euclidean_if_orthonormal)"
+    location: "Physlib/SpaceAndTime/ReferenceFrame/Basic.lean (norm_euclidean_if_orthonormal, inner_euclidean_if_orthonormal)"
+
+  - description: "The API contains the velocity of a trajectory read off a frame's axes as a frame vector, its vanishing for a trajectory at rest, and its value for an inertial frame's own origin."
+    done: true
+    location: "Physlib/SpaceAndTime/ReferenceFrame/Velocity.lean (velocityComponents, velocityComponents_const, velocityComponents_origin)"
 
   - description: "The API shall contain a choice of time origin for a frame, so that time translations can act on frames."
     done: false
     location: N/A
 
-  - description: "The API shall contain the defining property of an inertial frame's origin velocity, and the origin and basis of a frame built from reference points."
+  - description: "The API contains the defining property of an inertial frame's origin velocity, both as the displacement law and as the time derivative of the origin."
+    done: true
+    location: "Physlib/SpaceAndTime/ReferenceFrame/Basic.lean (IsInertial.origin_vsub); Physlib/SpaceAndTime/ReferenceFrame/Velocity.lean (IsInertial.derivVec_origin)"
+
+  - description: "The API shall contain the origin and basis of a frame built from reference points."
     done: false
     location: N/A
 
   - description: "The API shall contain the relative motion of two inertial frames, expressed as the boost, rotation and translation carrying one to the other, together with the induced transformation law for frame vectors."
     done: false
     location: N/A
 
-  - description: "The API shall contain the derivative of a trajectory expressed in a frame, giving the velocity and acceleration measured by that frame as the time derivative of its coordinate components."
+  - description: "The API shall contain the derivative of a trajectory expressed in a frame, giving the velocity and acceleration measured by that frame as the time derivative of its coordinate components, recorded as a TODO in Physlib/SpaceAndTime/ReferenceFrame/Velocity.lean."
     done: false
     location: N/A
 

Physlib/SpaceAndTime/ReferenceFrame.lean → Physlib/SpaceAndTime/ReferenceFrame/Basic.lean

@@ -5,7 +5,6 @@ Authors: Raunak Chhatwal
 -/
 module
 
-public import Mathlib.LinearAlgebra.AffineSpace.Basis
 public import Mathlib.Topology.Algebra.Module.TransferInstance
 public import Physlib.SpaceAndTime.Space.Basic
 public import Physlib.SpaceAndTime.Time.Basic
@@ -116,6 +115,11 @@ structure IsInertial (frame : ReferenceFrame d) : Prop where
 def IsInertial.velocity (h : frame.IsInertial) : EuclideanSpace ℝ (Fin d) :=
   Classical.choose h.origin_moves_uniformly
 
+/-- The displacement of the origin is elapsed time times `h.velocity`. -/
+lemma IsInertial.origin_vsub (h : frame.IsInertial) (t₁ t₂ : Time) :
+    frame.origin t₂ -ᵥ frame.origin t₁ = (t₂ - t₁).val • h.velocity :=
+  Classical.choose_spec h.origin_moves_uniformly t₁ t₂
+
 /-- An inertial frame conserves its coordinate metric. -/
 lemma IsInertial.isMetricConserved (h : frame.IsInertial) : frame.IsMetricConserved := by
   intro t₁ t₂ i j

Physlib/SpaceAndTime/ReferenceFrame/Velocity.lean

@@ -0,0 +1,96 @@
+/-
+Copyright (c) 2026 Zhi Kai Pong. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Zhi Kai Pong
+-/
+module
+
+public import Physlib.SpaceAndTime.ReferenceFrame.Basic
+public import Physlib.SpaceAndTime.Time.Derivatives
+/-!
+# Velocity in a reference frame
+
+## i. Overview
+
+The velocity of a trajectory is a displacement per unit time, so it is read off a frame's axes
+as a `frame.Vector`. This is the velocity of the trajectory in space, expressed in the frame's
+axes at that instant. For a frame whose axes turn with time it is not the velocity an observer
+carried along by the frame would measure; that quantity, the time derivative of the coordinate
+components, requires regularity of `frame.basis` and is recorded as a TODO at the end of the file.
+
+The velocity of an inertial frame's origin, `IsInertial.velocity`, is defined through the
+uniform motion of the origin. Here it is identified with the time derivative of the origin.
+
+## ii. Key results
+
+- `velocityComponents` : the velocity of a trajectory in the components of a frame.
+- `velocityComponents_const` : a trajectory at rest has zero velocity in every frame.
+- `IsInertial.derivVec_origin` : the velocity of an inertial frame's origin is the time
+  derivative of that origin.
+- `velocityComponents_origin` : the velocity of an inertial frame's origin, measured in that
+  frame.
+
+## iii. Table of contents
+
+- A. The velocity of a trajectory in a frame
+- B. The velocity of an inertial frame's origin
+
+## iv. References
+
+-/
+
+@[expose] public noncomputable section
+
+namespace ClassicalMechanics
+namespace ReferenceFrame
+
+open Time
+
+variable {d : ℕ} {frame : ReferenceFrame d}
+
+/-!
+## A. The velocity of a trajectory in a frame
+-/
+
+/-- The velocity of the trajectory `x`, in the components of `frame` at time `t`. -/
+def velocityComponents (frame : ReferenceFrame d) (x : Time → Space d) (t : Time) :
+    frame.Vector :=
+  (Vector.dispEquiv t).symm (∂ₜᵥ x t)
+
+lemma velocityComponents_eq (x : Time → Space d) (t : Time) :
+    frame.velocityComponents x t = (Vector.dispEquiv t).symm (∂ₜᵥ x t) := rfl
+
+/-- A trajectory at rest has zero velocity in every frame. -/
+@[simp]
+lemma velocityComponents_const (p : Space d) (t : Time) :
+    frame.velocityComponents (fun _ => p) t = 0 := by
+  rw [velocityComponents_eq, Time.derivVec_const, map_zero]
+
+/-!
+## B. The velocity of an inertial frame's origin
+-/
+
+/-- The velocity of an inertial frame's origin is the time derivative of that origin. -/
+lemma IsInertial.derivVec_origin (h : frame.IsInertial) (t : Time) :
+    h.velocity = ∂ₜᵥ frame.origin t := by
+  simp only [Time.derivVec_eq, h.origin_vsub, Time.sub_val]
+  rw [fderiv_smul_const (by fun_prop), ContinuousLinearMap.smulRight_apply, fderiv_sub_const,
+    Time.fderiv_val, one_smul]
+
+/-- The velocity of an inertial frame's origin, measured in that frame. -/
+lemma velocityComponents_origin (h : frame.IsInertial) (t : Time) :
+    frame.velocityComponents frame.origin t = (Vector.dispEquiv t).symm h.velocity := by
+  rw [velocityComponents_eq, ← h.derivVec_origin]
+
+TODO "ReferenceFrame API-map requirement: the derivative of a trajectory expressed in a
+  frame, giving the velocity and acceleration measured by that frame as the time derivative
+  of its coordinate components. Plan: define the coordinate components of a trajectory,
+  `(dispEquiv t).symm (x t -ᵥ frame.origin t)`, and for an inertial frame identify their
+  time derivative with `velocityComponents x t` minus the origin's velocity components;
+  acceleration is one further time derivative. A general frame needs regularity of
+  `frame.basis`, which `ReferenceFrame` does not yet carry."
+
+end ReferenceFrame
+end ClassicalMechanics
+
+end