diff --git a/Physlib.lean b/Physlib.lean index dea1f994df..7b861c3182 100644 --- a/Physlib.lean +++ b/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 diff --git a/Physlib/SpaceAndTime/ReferenceFrame/API-map.yaml b/Physlib/SpaceAndTime/ReferenceFrame/API-map.yaml index d4a9d91664..57bda396e9 100644 --- a/Physlib/SpaceAndTime/ReferenceFrame/API-map.yaml +++ b/Physlib/SpaceAndTime/ReferenceFrame/API-map.yaml @@ -41,61 +41,69 @@ 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 @@ -103,7 +111,7 @@ Requirements: 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 diff --git a/Physlib/SpaceAndTime/ReferenceFrame.lean b/Physlib/SpaceAndTime/ReferenceFrame/Basic.lean similarity index 97% rename from Physlib/SpaceAndTime/ReferenceFrame.lean rename to Physlib/SpaceAndTime/ReferenceFrame/Basic.lean index dc10452ae4..4d644c4e58 100644 --- a/Physlib/SpaceAndTime/ReferenceFrame.lean +++ b/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 diff --git a/Physlib/SpaceAndTime/ReferenceFrame/Velocity.lean b/Physlib/SpaceAndTime/ReferenceFrame/Velocity.lean new file mode 100644 index 0000000000..dbe30cb666 --- /dev/null +++ b/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