Imports
/-
Copyright (c) 2026 Raunak Chhatwal. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
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.BasicReference frames
A point in space and a list of coordinates are different kinds of data. Assigning coordinates to a
point requires an origin and a basis for measuring displacements from that origin. A
ReferenceFrame records those choices at every time.
This distinction is built into Space d, which is an affine space. Two points determine a
displacement, but no point is automatically the zero point. The chosen origin therefore belongs to
the frame, not to space itself. Similarly, a displacement has coordinate components only after a
basis has been chosen.
Most applications should use frames that are both inertial and orthonormal. In orthonormal frames, the norm and inner product of coordinate vectors are given by the familiar Euclidean formulas. The extra generality here also permits nonorthonormal coordinate grids. Giving every coordinate tuple the standard Euclidean norm and dot product, independently of its basis, would make coordinate transformations involving such a grid non-isometric: the same geometric displacement could acquire different lengths, or a pair of displacements a different angle, merely by changing frames. Instead, the metric on frame vectors is pulled back from geometric displacement space through the frame basis. The usual component formulas are recovered for orthonormal frames.
@[expose] public noncomputable sectionA. Reference frames
A reference frame can be pictured as a coordinate grid carried through time. It is part of how motion is described, not an additional physical object moving with the particles.
TODO "Add `timeOrigin` to enable time translations."
A time-indexed choice of affine origin and displacement basis in d-dimensional space.
The point assigned coordinate zero at each time.
The basis used to turn displacement vectors into coordinate components at each time.
structure ReferenceFrame (d : ℕ) where origin : Time → Space d basis : Time → Module.Basis (Fin d) ℝ (EuclideanSpace ℝ (Fin d))Build a reference frame from the trajectories of a collection of reference points.
At each time, the reference points must form an affine basis: none is redundant, and together they span the whole space. One reference point is chosen as the origin, and the displacements from it to the remaining points form the coordinate basis. The resulting frame need not be inertial or orthonormal.
def ReferenceFrame.fromReferencePoints
(referencePoints : Finset (Time → Space d))
(independence : ∀ t, AffineIndependent ℝ fun point : referencePoints => point.val t)
(spans_space : ∀ t, affineSpan ℝ {point.val t | point : referencePoints} = ⊤) :
ReferenceFrame d :=
let affineBasis (t : Time) : AffineBasis referencePoints ℝ (Space d) :=
⟨fun point => point.val t, independence t, spans_space t⟩
let reference_points_not_empty := (affineBasis 0).nonempty
let origin := Classical.choice reference_points_not_empty
letI := Fintype.ofFinite {point : referencePoints // point ≠ origin}
let basis t := (affineBasis t).basisOf origin
let other_reference_points_size_eq_dim :
Fintype.card {point : referencePoints // point ≠ origin} = d :=
d:ℕreferencePoints:Finset (Time → Space d)independence:∀ (t : Time), AffineIndependent ℝ fun point => ↑point tspans_space:∀ (t : Time), affineSpan ℝ {x | ∃ point, ↑point t = x} = ⊤affineBasis:Time → AffineBasis ↥referencePoints ℝ (Space d) := fun t => { toFun := fun point => ↑point t, ind' := ⋯, tot' := ⋯ }reference_points_not_empty:Nonempty ↥referencePoints := ···origin:↥referencePoints := Classical.choice reference_points_not_emptythis:Fintype { point // point ≠ origin } := Fintype.ofFinite { point // point ≠ origin }basis:Time → Module.Basis { j // j ≠ origin } ℝ (EuclideanSpace ℝ (Fin d)) := fun t => (affineBasis t).basisOf origin⊢ Fintype.card { point // point ≠ origin } = d All goals completed! 🐙
let basisReindexed t :=
(basis t).reindex (Fintype.equivFinOfCardEq other_reference_points_size_eq_dim)
{ origin := origin, basis := basisReindexed }B. Inertial reference frames
In Newtonian mechanics, an inertial coordinate grid does not rotate or change scale, and its origin moves in a straight line at constant velocity. These conditions restrict the frame, not the particles described in that frame.
Whether the frame basis induces the same inner product on coordinates at every time.
def IsMetricConserved (frame : ReferenceFrame d) : Prop :=
∀ t₁ t₂ i j,
inner ℝ (frame.basis t₁ i) (frame.basis t₁ j) = inner ℝ (frame.basis t₂ i) (frame.basis t₂ j)Whether the frame's coordinate basis is orthonormal at every time.
def Orthonormal (frame : ReferenceFrame d) : Prop :=
∀ t, _root_.Orthonormal ℝ (frame.basis t)An orthonormal frame conserves its coordinate metric.
All goals completed! 🐙instance [h : Fact frame.Orthonormal] : Fact frame.IsMetricConserved := ⟨h.out.isMetricConserved⟩Whether a reference frame is related to its initial grid by uniform translation alone.
Elapsed time times velocity is exactly the origin's displacement.
The coordinate axes neither rotate nor change scale with time.
structure IsInertial (frame : ReferenceFrame d) : Prop where origin_moves_uniformly :
∃ velocity, ∀ t₁ t₂, frame.origin t₂ -ᵥ frame.origin t₁ = (t₂ - t₁).val • velocity basis_conserved : ∀ t₁ t₂, frame.basis t₁ = frame.basis t₂The time-independent velocity of an inertial frame's coordinate origin.
def IsInertial.velocity (h : frame.IsInertial) : EuclideanSpace ℝ (Fin d) :=
Classical.choose h.origin_moves_uniformlyAn inertial frame conserves its coordinate metric.
All goals completed! 🐙Inertiality provides the conserved metric needed for metric operations on frame vectors.
instance [h : Fact frame.IsInertial] : Fact frame.IsMetricConserved := ⟨h.out.isMetricConserved⟩C. Vectors in a reference frame
frame.Vector is the common coordinate carrier for vector quantities expressed relative to
frame. It intentionally records the coordinate frame but not the physical dimension, so relative
position, velocity, acceleration, force, momentum, and similar quantities can use the same
componentwise calculations. Their different physical roles, units, and transformation laws must be
supplied by the surrounding definitions. When a vector represents a displacement, dispEquiv
converts its coordinates into the corresponding geometric displacement at a given time.
The d real components used to express a vector quantity relative to frame.
One scalar coefficient for each axis of the frame.
structure Vector (frame : ReferenceFrame d) where components : Fin d → ℝEquivalence between frame vectors and coordinate components
def componentEquiv : frame.Vector ≃ (Fin d → ℝ) :=
Equiv.mk components mk Eq.refl Eq.reflinstance : AddCommGroup frame.Vector := componentEquiv.addCommGroupinstance : Module ℝ frame.Vector := componentEquiv.module ℝLinear equivalence between frame vectors and coordinate components.
def componentLinearEquiv : frame.Vector ≃ₗ[ℝ] (Fin d → ℝ) :=
{componentEquiv with map_add' _ _ := rfl, map_smul' _ _ := rfl}
Equivalence between frame vectors and geometric displacements in space,
defined by the frame's basis at t.
def dispEquiv (t : Time) : frame.Vector ≃ₗ[ℝ] EuclideanSpace ℝ (Fin d) :=
componentLinearEquiv.trans (frame.basis t).equivFun.symmUse the same topology for frame vectors as components' product topology.
instance : TopologicalSpace frame.Vector := componentEquiv.topologicalSpaceContinuous linear equivalence between frame vectors and coordinate components.
def componentContLinearEquiv (frame : ReferenceFrame d) : frame.Vector ≃L[ℝ] (Fin d → ℝ) :=
{ componentLinearEquiv with
continuous_toFun := continuous_induced_dom
continuous_invFun := componentEquiv.homeomorph.continuous_invFun }instance : FiniteDimensional ℝ frame.Vector :=
FiniteDimensional.of_injective componentLinearEquiv.toLinearMap componentEquiv.injective
Continuous equivalence between frame vectors and geometric displacements in space,
defined by the frame's basis at t.
def contDispEquiv (t : Time) : frame.Vector ≃L[ℝ] EuclideanSpace ℝ (Fin d) :=
(componentContLinearEquiv frame).trans (frame.basis t).equivFun.toContinuousLinearEquiv.symmThe physical norm on frame vectors, pulled back from geometric displacement space.
instance [_h : Fact frame.IsMetricConserved] : NormedAddCommGroup frame.Vector :=
let normedSpace :=
NormedAddCommGroup.induced _ _ (dispEquiv 0).toLinearMap (dispEquiv 0).injective
let metricSpace :=
normedSpace.replaceTopology <| (contDispEquiv 0).toHomeomorph.isInducing.eq_induced
{ metricSpace with norm := normedSpace.norm, dist_eq := normedSpace.dist_eq }The physical inner product on frame vectors, pulled back from geometric displacement space.
All goals completed! 🐙In an orthonormal frame, the norm is the square root of squared components.
All goals completed! 🐙
_ = _ := EuclideanSpace.real_norm_sq_eq _In an orthonormal frame, the inner product is the sum of component products.
d:ℕframe:ReferenceFrame dh:Fact frame.Orthonormalv:frame.Vectorw:frame.Vectorbasis:OrthonormalBasis (Fin d) ℝ (EuclideanSpace ℝ (Fin d)) := (frame.basis 0).toOrthonormalBasis ⋯⊢ ∑ i, inner ℝ ((WithLp.toLp 2 v.components).ofLp i) ((WithLp.toLp 2 w.components).ofLp i) =
∑ i, v.components i * w.components i; simp_rw d:ℕframe:ReferenceFrame dh:Fact frame.Orthonormalv:frame.Vectorw:frame.Vectorbasis:OrthonormalBasis (Fin d) ℝ (EuclideanSpace ℝ (Fin d)) := (frame.basis 0).toOrthonormalBasis ⋯⊢ ∑ x, inner ℝ (v.components x) (w.components x) = ∑ i, v.components i * w.components iAll goals completed! 🐙]