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 for this module

• A. The initial conditions
• B. Trajectories associated with the initial conditions
• C. Trajectories and Equation of motion
• D. The energy of the trajectories
• E. The trajectories at zero velocity
• 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₀ : Space 1

  The initial position of the harmonic oscillator.

• v₀ : Space 1

  The initial velocity of the harmonic oscillator.

Part A.1.I

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 inital condition given by an initial position and an initial velocity to other specifications of initial conditions. This is currently not implemented, and is a TODO.

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 } }

Part A.3.I

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 → Space 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₀

Part B.1.I

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 satsify 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 → Space 1) : 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 implmentation:

• 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 enrgy 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)

E. The trajectories at zero velocity

We study the properties of the trajectories when the vleocity 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₀ 0 / (S.ω * IC.x₀ 0)

E.2. A time when the velocity is zero

We show that as long as the inital 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₀ 0 / (S.ω * IC.x₀ 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, as long as the initial conditions are not both zero. This is currently a TODO.

theorem ClassicalMechanics.HarmonicOscillator.InitialConditions.trajectory_velocity_eq_zero_iff (S : HarmonicOscillator) (IC : InitialConditions) (t : Time) (hx : IC.x₀ ≠ 0 ∨ IC.v₀ ≠ 0) : 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.