Solutions to the classical harmonic oscillator

i. Overview

In this module we define the solutions to the classical harmonic oscillator, prove that they satisfy the equation of motion, and prove some properties of the solutions.

ii. Key results

• InitialConditions is a structure for the initial conditions for the harmonic oscillator.
• trajectories is the trajectories to the harmonic oscillator for given initial conditions.
• trajectories_equationOfMotion proves that the solution satisfies the equation of motion.

iii. Table of contents

• A. The initial conditions
  • A.1. Definition of the initial conditions
    • A.1.1. Extensionality lemma
  • A.2. Relation to other types of initial conditions
  • A.3. The zero initial conditions
    • A.3.1. Simple results for the zero initial conditions
• B. Trajectories associated with the initial conditions
  • B.1. The trajectory associated with the initial conditions
    • B.1.1. Definitional equality for the trajectory
  • B.2. The trajectory for zero initial conditions
  • B.3. Smoothness of the trajectories
  • B.4. Velocity of the trajectories
  • B.5. Acceleration of the trajectories
  • B.6. The initial conditions of the trajectories
• C. Trajectories and Equation of motion
  • C.1. Uniqueness of the solutions
• D. The energy of the trajectories
• E. The trajectories at zero velocity
  • E.1. The times at which the velocity is zero
  • E.2. A time when the velocity is zero
  • E.3. The position when the velocity is zero
• F. Some open TODOs

iv. References

References for the classical harmonic oscillator include:

• Landau & Lifshitz, Mechanics, page 58, section 21.

A. The initial conditions

We define the type of initial conditions for the harmonic oscillator. The initial conditions are currently defined as an initial position and an initial velocity, that is the values of the solution and its time derivative at time 0.

A.1. Definition of the initial conditions

We start by defining the type of initial conditions for the harmonic oscillator.

structure ClassicalMechanics.HarmonicOscillator.InitialConditions : Type

The initial conditions for the harmonic oscillator specified by an initial position, and an initial velocity.

• x₀ : EuclideanSpace ℝ (Fin 1)

  The initial position of the harmonic oscillator.

• v₀ : EuclideanSpace ℝ (Fin 1)

  The initial velocity of the harmonic oscillator.

A.1.1. Extensionality lemma

We prove an extensionality lemma for InitialConditions. That is, a lemma which states that two initial conditions are equal if their initial positions and initial velocities are equal.

theorem ClassicalMechanics.HarmonicOscillator.InitialConditions.ext {IC₁ IC₂ : InitialConditions} (h1 : IC₁.x₀ = IC₂.x₀) (h2 : IC₁.v₀ = IC₂.v₀) : IC₁ = IC₂

theorem ClassicalMechanics.HarmonicOscillator.InitialConditions.ext_iff {IC₁ IC₂ : InitialConditions} : IC₁ = IC₂ ↔ IC₁.x₀ = IC₂.x₀ ∧ IC₁.v₀ = IC₂.v₀

A.2. Relation to other types of initial conditions

We relate the initial condition given by an initial position and an initial velocity to other specifications of initial conditions.

In this section, we implement alternative ways to specify initial conditions for the harmonic oscillator. The standard InitialConditions type specifies position and velocity at time t=0, but in practice it is often useful to specify initial conditions at other times or in other forms.

Currently implemented:

• Initial conditions at arbitrary time: Specify position and velocity at any time t₀, not necessarily at t=0. This is useful for problems where the natural reference time is not zero.

Future work (to be added in separate PRs) :

• Initial conditions from two positions at different times
• Initial conditions from two velocities at different times
• Amplitude-phase parametrization

All alternative forms can be converted to the standard InitialConditions type via conversion functions, and we prove that the converted initial conditions produce trajectories that satisfy the original specifications.

A.2.1. Initial conditions at arbitrary time

We define a type for initial conditions specified at an arbitrary time t₀, rather than at t=0. This is useful when the natural reference point for a problem is not at time zero.

structure ClassicalMechanics.HarmonicOscillator.InitialConditionsAtTime : Type

Initial conditions for the harmonic oscillator specified at an arbitrary time t₀.

This structure allows specifying the position and velocity at any time t₀, not necessarily at t=0. This is useful for problems where the natural reference time is not zero.

The conditions can be converted to the standard InitialConditions format (at t=0) using the toInitialConditions function.

• t₀ : Time

  The time at which the initial conditions are specified.

• x_t₀ : EuclideanSpace ℝ (Fin 1)

  The position at time t₀.

• v_t₀ : EuclideanSpace ℝ (Fin 1)

  The velocity at time t₀.

A.2.1.1. Extensionality lemma

We prove an extensionality lemma for InitialConditionsAtTime.

theorem ClassicalMechanics.HarmonicOscillator.InitialConditionsAtTime.ext {IC₁ IC₂ : InitialConditionsAtTime} (h1 : IC₁.t₀ = IC₂.t₀) (h2 : IC₁.x_t₀ = IC₂.x_t₀) (h3 : IC₁.v_t₀ = IC₂.v_t₀) : IC₁ = IC₂

theorem ClassicalMechanics.HarmonicOscillator.InitialConditionsAtTime.ext_iff {IC₁ IC₂ : InitialConditionsAtTime} : IC₁ = IC₂ ↔ IC₁.t₀ = IC₂.t₀ ∧ IC₁.x_t₀ = IC₂.x_t₀ ∧ IC₁.v_t₀ = IC₂.v_t₀

A.2.1.2. Conversion to standard initial conditions

We now define the conversion from InitialConditionsAtTime to the standard InitialConditions.

The conversion works by "running the trajectory backward in time" from t₀ to 0. Given that we know x(t₀) and v(t₀), we use the harmonic oscillator solution formula with time-reversal to determine what x(0) and v(0) must have been.

Mathematically, if x(t) = cos(ωt)·x₀ + (sin(ωt)/ω)·v₀, then setting t = t₀: x(t₀) = cos(ωt₀)·x₀ + (sin(ωt₀)/ω)·v₀ v(t₀) = -ω·sin(ωt₀)·x₀ + cos(ωt₀)·v₀

Solving this linear system for x₀ and v₀ gives the formulas below.

noncomputable def ClassicalMechanics.HarmonicOscillator.InitialConditionsAtTime.toInitialConditions (S : HarmonicOscillator) (IC : InitialConditionsAtTime) : InitialConditions

Convert initial conditions at time t₀ to standard initial conditions at t=0.

This conversion uses the harmonic oscillator solution formula with time-reversal. The resulting InitialConditions will produce a trajectory that passes through x_t₀ with velocity v_t₀ at time t₀.

See toInitialConditions_trajectory_at_t₀ and toInitialConditions_velocity_at_t₀ for the correctness proofs.

Equations

• One or more equations did not get rendered due to their size.

The correctness proofs showing that the conversion produces the expected trajectory are given later in section D.1, after the trajectory machinery has been defined.

A.3. The zero initial conditions

The zero initial conditions are the initial conditions with zero initial position and zero initial velocity.

In the end, we will see that this corresponds to the solution which is identically zero, i.e. the particle remains at rest at the origin.

instance ClassicalMechanics.HarmonicOscillator.InitialConditions.instZero : Zero InitialConditions

The zero initial condition.

Equations

• ClassicalMechanics.HarmonicOscillator.InitialConditions.instZero = { zero := { x₀ := 0, v₀ := 0 } }

A.3.1. Simple results for the zero initial conditions

Some simple results about the zero initial conditions.

@[simp]

theorem ClassicalMechanics.HarmonicOscillator.InitialConditions.x₀_zero : x₀ 0 = 0

The zero initial condition has zero starting point.

@[simp]

theorem ClassicalMechanics.HarmonicOscillator.InitialConditions.v₀_zero : v₀ 0 = 0

The zero initial condition has zero starting velocity.

B. Trajectories associated with the initial conditions

To each initial condition we association a trajectory. We will prove some basic properties of these trajectories.

Eventually we will show that these trajectories satisfy the equation of motion, for now we can think of them as some choice of trajectory associated with the initial conditions.

B.1. The trajectory associated with the initial conditions

noncomputable def ClassicalMechanics.HarmonicOscillator.InitialConditions.trajectory (S : HarmonicOscillator) (IC : InitialConditions) : Time → EuclideanSpace ℝ (Fin 1)

Given initial conditions, the solution to the classical harmonic oscillator.

Equations

• ClassicalMechanics.HarmonicOscillator.InitialConditions.trajectory S IC t = Real.cos (S.ω * t.val) • IC.x₀ + (Real.sin (S.ω * t.val) / S.ω) • IC.v₀

B.1.1. Definitional equality for the trajectory

We show a basic definitional equality for the trajectory.

theorem ClassicalMechanics.HarmonicOscillator.InitialConditions.trajectory_eq (S : HarmonicOscillator) (IC : InitialConditions) : trajectory S IC = fun (t : Time) => Real.cos (S.ω * t.val) • IC.x₀ + (Real.sin (S.ω * t.val) / S.ω) • IC.v₀

B.2. The trajectory for zero initial conditions

The trajectory for zero initial conditions is the zero function.

@[simp]

theorem ClassicalMechanics.HarmonicOscillator.InitialConditions.trajectory_zero (S : HarmonicOscillator) : trajectory S 0 = fun (x : Time) => 0

For zero initial conditions, the trajectory is zero.

B.3. Smoothness of the trajectories

The trajectories for any initial conditions are smooth functions of time.

theorem ClassicalMechanics.HarmonicOscillator.InitialConditions.trajectory_contDiff (S : HarmonicOscillator) (IC : InitialConditions) {n : WithTop ℕ∞} : ContDiff ℝ n (trajectory S IC)

B.4. Velocity of the trajectories

We give a simplification of the velocity of the trajectory.

theorem ClassicalMechanics.HarmonicOscillator.InitialConditions.trajectory_velocity (S : HarmonicOscillator) (IC : InitialConditions) : Time.deriv (trajectory S IC) = fun (t : Time) => -S.ω • Real.sin (S.ω * t.val) • IC.x₀ + Real.cos (S.ω * t.val) • IC.v₀

B.5. Acceleration of the trajectories

We give a simplification of the acceleration of the trajectory.

theorem ClassicalMechanics.HarmonicOscillator.InitialConditions.trajectory_acceleration (S : HarmonicOscillator) (IC : InitialConditions) : Time.deriv (Time.deriv (trajectory S IC)) = fun (t : Time) => -S.ω ^ 2 • Real.cos (S.ω * t.val) • IC.x₀ - S.ω • Real.sin (S.ω * t.val) • IC.v₀

B.6. The initial conditions of the trajectories

We show that, unsurprisingly, the trajectories have the initial conditions used to define them.

@[simp]

theorem ClassicalMechanics.HarmonicOscillator.InitialConditions.trajectory_position_at_zero (S : HarmonicOscillator) (IC : InitialConditions) : trajectory S IC 0 = IC.x₀

For a set of initial conditions IC the position of the solution at time 0 is IC.x₀.

@[simp]

theorem ClassicalMechanics.HarmonicOscillator.InitialConditions.trajectory_velocity_at_zero (S : HarmonicOscillator) (IC : InitialConditions) : Time.deriv (trajectory S IC) 0 = IC.v₀

C. Trajectories and Equation of motion

The trajectories satisfy the equation of motion for the harmonic oscillator.

theorem ClassicalMechanics.HarmonicOscillator.InitialConditions.trajectory_equationOfMotion (S : HarmonicOscillator) (IC : InitialConditions) : S.EquationOfMotion (trajectory S IC)

C.1. Uniqueness of the solutions

We show that the trajectories are the unique solutions to the equation of motion for the given initial conditions. This is currently a TODO.

theorem ClassicalMechanics.HarmonicOscillator.InitialConditions.trajectories_unique (S : HarmonicOscillator) (IC : InitialConditions) (x : Time → EuclideanSpace ℝ (Fin 1)) (hx : ContDiff ℝ (↑⊤) x) : S.EquationOfMotion x ∧ x 0 = IC.x₀ ∧ Time.deriv x 0 = IC.v₀ → x = trajectory S IC

The trajectories to the equation of motion for a given set of initial conditions are unique.

Semiformal implementation:

• One may needed the added condition of smoothness on x here.
• EquationOfMotion needs defining before this can be proved.

D. The energy of the trajectories

For a given set of initial conditions, the energy of the trajectory is constant, due to the conservation of energy. Here we show it's value.

theorem ClassicalMechanics.HarmonicOscillator.InitialConditions.trajectory_energy (S : HarmonicOscillator) (IC : InitialConditions) : S.energy (trajectory S IC) = fun (x : Time) => 1 / 2 * (S.m * ‖IC.v₀‖ ^ 2 + S.k * ‖IC.x₀‖ ^ 2)

D.1. Correctness of InitialConditionsAtTime conversion

We now prove the correctness lemmas for the InitialConditionsAtTime.toInitialConditions conversion function. These show that the conversion produces a trajectory that passes through the specified position and velocity at the specified time.

@[simp]

theorem ClassicalMechanics.HarmonicOscillator.InitialConditionsAtTime.toInitialConditions_trajectory_at_t₀ (S : HarmonicOscillator) (IC : InitialConditionsAtTime) : InitialConditions.trajectory S (toInitialConditions S IC) IC.t₀ = IC.x_t₀

The trajectory resulting from toInitialConditions passes through the specified position x_t₀ at time t₀.

@[simp]

theorem ClassicalMechanics.HarmonicOscillator.InitialConditionsAtTime.toInitialConditions_velocity_at_t₀ (S : HarmonicOscillator) (IC : InitialConditionsAtTime) : Time.deriv (InitialConditions.trajectory S (toInitialConditions S IC)) IC.t₀ = IC.v_t₀

The trajectory resulting from toInitialConditions has the specified velocity v_t₀ at time t₀.

theorem ClassicalMechanics.HarmonicOscillator.InitialConditionsAtTime.toInitialConditions_energy_at_t₀ (S : HarmonicOscillator) (IC : InitialConditionsAtTime) : S.energy (InitialConditions.trajectory S (toInitialConditions S IC)) IC.t₀ = 1 / 2 * (S.m * ‖IC.v_t₀‖ ^ 2 + S.k * ‖IC.x_t₀‖ ^ 2)

The energy of the trajectory at time t₀ equals the energy computed from the initial conditions at t₀.

E. The trajectories at zero velocity

We study the properties of the trajectories when the velocity is zero.

E.1. The times at which the velocity is zero

We show that if the velocity of the trajectory is zero, then the time satisfies the condition that

tan (S.ω * t) = IC.v₀ 0 / (S.ω * IC.x₀ 0)

theorem ClassicalMechanics.HarmonicOscillator.InitialConditions.tan_time_eq_of_trajectory_velocity_eq_zero (S : HarmonicOscillator) (IC : InitialConditions) (t : Time) (h : Time.deriv (trajectory S IC) t = 0) (hx : IC.x₀ ≠ 0 ∨ IC.v₀ ≠ 0) : Real.tan (S.ω * t.val) = IC.v₀.ofLp 0 / (S.ω * IC.x₀.ofLp 0)

E.2. A time when the velocity is zero

We show that as long as the initial position is non-zero, then at the time arctan (IC.v₀ 0 / (S.ω * IC.x₀ 0)) / S.ω the velocity is zero.

theorem ClassicalMechanics.HarmonicOscillator.InitialConditions.trajectory_velocity_eq_zero_at_arctan (S : HarmonicOscillator) (IC : InitialConditions) (hx : IC.x₀ ≠ 0) : Time.deriv (trajectory S IC) { val := Real.arctan (IC.v₀.ofLp 0 / (S.ω * IC.x₀.ofLp 0)) / S.ω } = 0

E.3. The position when the velocity is zero

We show that the position is equal to √(‖IC.x₀‖^2 + (‖IC.v₀‖/S.ω)^2) when the velocity is zero.

theorem ClassicalMechanics.HarmonicOscillator.InitialConditions.trajectory_velocity_eq_zero_iff (S : HarmonicOscillator) (IC : InitialConditions) (t : Time) : Time.deriv (trajectory S IC) t = 0 ↔ ‖trajectory S IC t‖ = √(‖IC.x₀‖ ^ 2 + (‖IC.v₀‖ / S.ω) ^ 2)

F. Some open TODOs

We give some open TODOs for the classical harmonic oscillator.