Imports
/-
Copyright (c) 2026 Nathaneal Sajan. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Nathaneal Sajan
-/
module
public import Physlib.ClassicalMechanics.HarmonicOscillator.Geometric.Basic
public import Physlib.SpaceAndTime.Time.Derivatives
public import Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
public import Mathlib.Geometry.Manifold.MFDeriv.BasicGeometric trajectories of the harmonic oscillator
i. Overview
A trajectory of the harmonic oscillator is a time-parametrized curve in the configuration
manifold Q. Since this model of Q has a single global coordinate valued in
EuclideanSpace ℝ (Fin 1), every geometric trajectory has an associated coordinate curve.
The coordinate diffeomorphism from Q to its model space lets smoothness of a geometric
trajectory be tested as ordinary smoothness of its coordinate curve.
ii. Key results
Trajectory : a curve from Time into the configuration manifold.
Trajectory.coord : the global Euclidean coordinate curve of a trajectory.
Trajectory.toSpace : the physical-space position along a trajectory.
Trajectory.contMDiff_iff_contDiff_coord : geometric smoothness of a trajectory is
equivalent to ordinary smoothness of its coordinate curve.
Trajectory.velocity : the geometric velocity of a trajectory as a tangent vector.
Trajectory.velocity_eq_deriv_coord : in the global coordinate, geometric velocity is
represented by the time derivative of the coordinate curve.
iii. Table of contents
A. The trajectory type and coordinate projection
B. Smoothness of trajectories
C. Velocity in the tangent bundle
iv. References
Ivo Terek, Introductory Variational Calculus on Manifolds, pages 1-2 (Section 1, Basic definitions and examples).
@[expose] public sectionA. The trajectory type and coordinate projection
A trajectory is a curve in the configuration manifold Q, parametrized by Time. The
coordinate projection reads the same curve in the chosen global coordinate, while toSpace
forgets the manifold structure and returns the corresponding physical-space position.
A trajectory of the oscillator: a curve in the configuration manifold Q.
abbrev Trajectory := Time → ConfigurationSpaceThe coordinate curve of a trajectory: its reading in the global Euclidean coordinate.
def coord (γ : Trajectory) : Time → EuclideanSpace ℝ (Fin 1) :=
fun t => chartAt (EuclideanSpace ℝ (Fin 1)) (γ t) (γ t)The physical position of the oscillator along a trajectory, over time.
def toSpace (γ : Trajectory) : Time → Space 1 := fun t => (γ t).toSpacelemma coord_apply (γ : Trajectory) (t : Time) : coord γ t = (γ t).val := rflB. Smoothness of trajectories
Because the global coordinate is a diffeomorphism, composing a trajectory with it preserves
and reflects manifold smoothness. Since both Time and the coordinate model are normed
spaces, this manifold-smoothness statement then becomes ordinary ContDiff smoothness.
A trajectory is smooth as a curve in Q iff its coordinate curve is ordinarily smooth.
n:WithTop ℕ∞γ:Trajectory⊢ ContMDiff 𝓘(ℝ, Time) (𝓡 1) n γ ↔ ContMDiff 𝓘(ℝ, Time) (𝓡 1) n (⇑ConfigurationSpace.valDiffeomorph ∘ γ)
All goals completed! 🐙C. Velocity in the tangent bundle
The velocity of a trajectory at time t is the tangent vector obtained by differentiating
the curve in the direction of the unit time vector. In this one-chart model, the tangent
space at each configuration is represented by the same Euclidean model space, so the
geometric velocity can be compared with the derivative of the coordinate curve.
A trajectory is MDifferentiableAt a time iff its coordinate curve is ordinarily
differentiable there, since the two differ by the coordinate diffeomorphism.
γ:Trajectoryt:Timehγ:MDiffAt γ t⊢ MDiffAt (⇑ConfigurationSpace.valDiffeomorph ∘ γ) t
All goals completed! 🐙
γ:Trajectoryt:Time⊢ MDiffAt γ.coord t → MDiffAt γ t γ:Trajectoryt:Timehcoord:MDiffAt γ.coord t⊢ MDiffAt γ t
γ:Trajectoryt:Timehcoord:MDiffAt γ.coord thγ:MDiffAt (⇑ConfigurationSpace.valDiffeomorph.symm ∘ γ.coord) t⊢ MDiffAt γ t
γ:Trajectoryt:Timehcoord:MDiffAt γ.coord thγ:MDiffAt (⇑ConfigurationSpace.valDiffeomorph.symm ∘ γ.coord) t⊢ γ = ⇑ConfigurationSpace.valDiffeomorph.symm ∘ γ.coord
γ:Trajectoryt:Timehcoord:MDiffAt γ.coord thγ:MDiffAt (⇑ConfigurationSpace.valDiffeomorph.symm ∘ γ.coord) ts:Time⊢ γ s = (⇑ConfigurationSpace.valDiffeomorph.symm ∘ γ.coord) s
All goals completed! 🐙
A trajectory and its coordinate curve have the same manifold derivative, since they
differ only by the coordinate diffeomorphism. This is the one lemma that unfolds the chart;
every later result uses only the stable mfderiv/fderiv API.
γ:Trajectoryt:Timehγ:¬MDiffAt γ t⊢ 0 = 0
All goals completed! 🐙In the global coordinate, geometric velocity is represented by the time derivative of the coordinate curve.
γ:Trajectoryt:Time⊢ (mfderiv% γ.coord t) 1 = ∂ₜ γ.coord t
All goals completed! 🐙