The Classical Harmonic Oscillator

i. Description

The classical harmonic oscillator is a classical mechanical system corresponding to a mass m under a force - k x where k is the spring constant and x is the position.

ii. Summary of the key results

The key results in the study of the classical harmonic oscillator are the follows:

In the Basic module:

• HarmonicOscillator contains the input data to the problem.
• EquationOfMotion defines the equation of motion for the harmonic oscillator.
• energy_conservation_of_equationOfMotion proves that a trajectory satisfying the equation of motion conserves energy.
• equationOfMotion_tfae proves that the equation of motion of motion is equivalent to
  • Newton's second law,
  • Hamilton's equations,
  • the variational principal for the action,
  • the Hamilton variation principal.

In the Solution module:

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

• A. The input data
• B. The angular frequency
• C. The energies
• D. Lagrangian and the equation of motion
• E. Newton's second law
• F. Energy conservation
• G. Hamiltonian formulation
• H. Equivalences between the different formulations of the equations of motion

iiv. References

References for the classical harmonic oscillator include:

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

A. The input data

We start by defining a structure containing the input data of the harmonic oscillator, and proving basic properties thereof. The input data consists of the mass m of the particle and the spring constant k.

structure ClassicalMechanics.HarmonicOscillator : Type

The classical harmonic oscillator is specified by a mass m, and a spring constant k. Both the mass and the string constant are assumed to be positive.

• m : ℝ

  The mass of the harmonic Oscillator.

• k : ℝ

  The spring constant of the harmonic oscillator.

• m_pos : 0 < self.m
• k_pos : 0 < self.k

@[simp]

theorem ClassicalMechanics.HarmonicOscillator.k_neq_zero (S : HarmonicOscillator) : S.k ≠ 0

@[simp]

theorem ClassicalMechanics.HarmonicOscillator.m_neq_zero (S : HarmonicOscillator) : S.m ≠ 0

B. The angular frequency

From the input data, it is possible to define the angular frequency ω of the harmonic oscillator, as √(k/m).

The angular frequency appears in the solutions to the equations of motion of the harmonic oscillator.

Here we both define and proof properties related to the angular frequency.

noncomputable def ClassicalMechanics.HarmonicOscillator.ω (S : HarmonicOscillator) : ℝ

The angular frequency of the classical harmonic osscilator, ω, is defined as √(k/m).

Equations

• S.ω = √(S.k / S.m)

@[simp]

theorem ClassicalMechanics.HarmonicOscillator.ω_pos (S : HarmonicOscillator) : 0 < S.ω

The angular frequency of the classical harmonic osscilator is positive.

theorem ClassicalMechanics.HarmonicOscillator.ω_sq (S : HarmonicOscillator) : S.ω ^ 2 = S.k / S.m

The square of the angular frequency of the classical harmonic osscilator is equal to k/m.

theorem ClassicalMechanics.HarmonicOscillator.ω_neq_zero (S : HarmonicOscillator) : S.ω ≠ 0

The angular frequency of the classical harmonic osscilator is not equal to zero.

theorem ClassicalMechanics.HarmonicOscillator.inverse_ω_sq (S : HarmonicOscillator) : (S.ω ^ 2)⁻¹ = S.m / S.k

The inverse of the square of the angular frequency of the classical harmonic osscilator is m/k.

C. The energies

The harmonic oscillator has a kinetic energy determined by it's velocity and a potential energy deetermined by it's position. These combine to give the total energy of the harmonic oscillator.

Here we state and prove a number of properties of these energies.

C.1. The definitions of the energies

We define the three energies, it is these energies which will control the dynamics of the harmonic oscillator, through the lagrangian.

noncomputable def ClassicalMechanics.HarmonicOscillator.kineticEnergy (S : HarmonicOscillator) (xₜ : Time → Space 1) : Time → ℝ

The kinetic energy of the harmonic oscillator is $\frac{1}{2} m ‖\dot x‖^2$.

Equations

• S.kineticEnergy xₜ t = 1 / 2 * S.m * inner ℝ (Time.deriv xₜ t) (Time.deriv xₜ t)

noncomputable def ClassicalMechanics.HarmonicOscillator.potentialEnergy (S : HarmonicOscillator) (x : Space 1) : ℝ

The potential energy of the harmonic oscillator is 1/2 k x ^ 2

Equations

• S.potentialEnergy x = (1 / 2) • S.k • inner ℝ x x

noncomputable def ClassicalMechanics.HarmonicOscillator.energy (S : HarmonicOscillator) (xₜ : Time → Space 1) : Time → ℝ

The energy of the harmonic oscillator is the kinetic energy plus the potential energy.

Equations

• S.energy xₜ t = S.kineticEnergy xₜ t + S.potentialEnergy (xₜ t)

C.2. Simple equalties for the energies

theorem ClassicalMechanics.HarmonicOscillator.kineticEnergy_eq (S : HarmonicOscillator) (xₜ : Time → Space 1) : S.kineticEnergy xₜ = fun (t : Time) => 1 / 2 * S.m * inner ℝ (Time.deriv xₜ t) (Time.deriv xₜ t)

theorem ClassicalMechanics.HarmonicOscillator.potentialEnergy_eq (S : HarmonicOscillator) (x : Space 1) : S.potentialEnergy x = (1 / 2) • S.k • inner ℝ x x

theorem ClassicalMechanics.HarmonicOscillator.energy_eq (S : HarmonicOscillator) (xₜ : Time → Space 1) : S.energy xₜ = fun (t : Time) => S.kineticEnergy xₜ t + S.potentialEnergy (xₜ t)

C.2. Differentiability of the energies

On smooth trajectories the energies are differentiable.

theorem ClassicalMechanics.HarmonicOscillator.kineticEnergy_differentiable (S : HarmonicOscillator) (xₜ : Time → Space 1) (hx : ContDiff ℝ (↑⊤) xₜ) : Differentiable ℝ (S.kineticEnergy xₜ)

theorem ClassicalMechanics.HarmonicOscillator.potentialEnergy_differentiable (S : HarmonicOscillator) (xₜ : Time → Space 1) (hx : ContDiff ℝ (↑⊤) xₜ) : Differentiable ℝ fun (t : Time) => S.potentialEnergy (xₜ t)

theorem ClassicalMechanics.HarmonicOscillator.energy_differentiable (S : HarmonicOscillator) (xₜ : Time → Space 1) (hx : ContDiff ℝ (↑⊤) xₜ) : Differentiable ℝ (S.energy xₜ)

C.3. Time derivatives of the energies

For a general smooth trajectory (which may not satisfy the equations of motion) we can compute the time derivatives of the energies.

theorem ClassicalMechanics.HarmonicOscillator.kineticEnergy_deriv (S : HarmonicOscillator) (xₜ : Time → Space 1) (hx : ContDiff ℝ (↑⊤) xₜ) : Time.deriv (S.kineticEnergy xₜ) = fun (t : Time) => inner ℝ (Time.deriv xₜ t) (S.m • Time.deriv (Time.deriv xₜ) t)

theorem ClassicalMechanics.HarmonicOscillator.potentialEnergy_deriv (S : HarmonicOscillator) (xₜ : Time → Space 1) (hx : ContDiff ℝ (↑⊤) xₜ) : (Time.deriv fun (t : Time) => S.potentialEnergy (xₜ t)) = fun (t : Time) => inner ℝ (Time.deriv xₜ t) (S.k • xₜ t)

theorem ClassicalMechanics.HarmonicOscillator.energy_deriv (S : HarmonicOscillator) (xₜ : Time → Space 1) (hx : ContDiff ℝ (↑⊤) xₜ) : Time.deriv (S.energy xₜ) = fun (t : Time) => inner ℝ (Time.deriv xₜ t) (S.m • Time.deriv (Time.deriv xₜ) t + S.k • xₜ t)

D. Lagrangian and the equation of motion

We state the lagrangian, and derive from that the equation of motion for the harmonic oscillator.

D.1. The Lagrangian

We define the lagrangian of the harmonic oscillator, as a function of phase-space. It is given by

$$L(t, x, v) := \frac{1}{2} m ‖v‖^2 - \frac{1}{2} k ‖x‖^2$$

In theory this definition is the kinetic energy minus the potential energy, however to make the lagrangian a function on phase-space we reserve this result for a lemma.

noncomputable def ClassicalMechanics.HarmonicOscillator.lagrangian (S : HarmonicOscillator) (t : Time) (x : Space 1) (v : EuclideanSpace ℝ (Fin 1)) : ℝ

The lagrangian of the harmonic oscillator is the kinetic energy minus the potential energy.

Equations

• S.lagrangian t x v = 1 / 2 * S.m * inner ℝ v v - S.potentialEnergy x

Part D.1.I

Equalitites for the lagrangian. We prove some simple equalities for the lagrangian, in particular that when applied to a trajectory it is the kinetic energy minus the potential energy.

theorem ClassicalMechanics.HarmonicOscillator.lagrangian_eq (S : HarmonicOscillator) : S.lagrangian = fun (t : Time) (x : Space 1) (v : EuclideanSpace ℝ (Fin 1)) => 1 / 2 * S.m * inner ℝ v v - 1 / 2 * S.k * inner ℝ x x

theorem ClassicalMechanics.HarmonicOscillator.lagrangian_eq_kineticEnergy_sub_potentialEnergy (S : HarmonicOscillator) (t : Time) (xₜ : Time → Space 1) : S.lagrangian t (xₜ t) (Time.deriv xₜ t) = S.kineticEnergy xₜ t - S.potentialEnergy (xₜ t)

Part D.1.II

The lagrangian is smooth in all its arguments.

theorem ClassicalMechanics.HarmonicOscillator.contDiff_lagrangian (S : HarmonicOscillator) (n : WithTop ℕ∞) : ContDiff ℝ n ↿S.lagrangian

Part D.1.III

We now show results related to the gradients of the lagrangian with respect to the position and velocity.

theorem ClassicalMechanics.HarmonicOscillator.gradient_lagrangian_position_eq (S : HarmonicOscillator) (t : Time) (x : Space 1) (v : EuclideanSpace ℝ (Fin 1)) : gradient (fun (x : Space 1) => S.lagrangian t x v) x = -S.k • x

theorem ClassicalMechanics.HarmonicOscillator.gradient_lagrangian_velocity_eq (S : HarmonicOscillator) (t : Time) (x : Space 1) (v : EuclideanSpace ℝ (Fin 1)) : gradient (S.lagrangian t x) v = S.m • v

D.2. The Euler-Lagrange operator

We now write down the Euler-Lagrange operator for the harmonic oscillator, for a trajectory $x(t)$ this is equal to

$$t\mapsto \left.\frac{\partial L(t, \dot x (t), q)}{\partial q}\right|_{q = x(t)} - \frac{d}{dt} \left.\frac{\partial L(t, v, x(t))}{\partial v}\right|_{v = \dot x (t)}$$

Setting this equal to zero corresponds to the Euler-Lagrange equations, and thereby the equation of motion.

noncomputable def ClassicalMechanics.HarmonicOscillator.eulerLagrangeOp (S : HarmonicOscillator) (xₜ : Time → Space 1) : Time → Space 1

The Euler-Lagrange operator for the classical harmonic osscilator.

Equations

• S.eulerLagrangeOp xₜ = ClassicalMechanics.eulerLagrangeOp S.lagrangian xₜ

Part D.2.I

Basic equaltities for the Euler-Lagrange operator.

theorem ClassicalMechanics.HarmonicOscillator.eulerLagrangeOp_eq (S : HarmonicOscillator) (xₜ : Time → Space 1) : S.eulerLagrangeOp xₜ = fun (t : Time) => gradient (fun (x : Space 1) => S.lagrangian t x (Time.deriv xₜ t)) (xₜ t) - Time.deriv (fun (t' : Time) => gradient (fun (x : EuclideanSpace ℝ (Fin 1)) => S.lagrangian t' (xₜ t') x) (Time.deriv xₜ t')) t

Part D.2.II

Relation of the Euler-Lagrange operator to variational derivative of the action.

theorem ClassicalMechanics.HarmonicOscillator.variational_gradient_action (S : HarmonicOscillator) (xₜ : Time → Space 1) (hq : ContDiff ℝ (↑⊤) xₜ) : varGradient (fun (q' : Time → Space 1) (t : Time) => S.lagrangian t (q' t) ((fderiv ℝ q' t) 1)) xₜ = S.eulerLagrangeOp xₜ

Part D.3. The equation of motion

The equation of motion for the harmonic oscillator is given by setting the Euler-Lagrange operator equal to zero.

def ClassicalMechanics.HarmonicOscillator.EquationOfMotion (S : HarmonicOscillator) (xₜ : Time → Space 1) : Prop

THe equation of motion for the Harmonic oscillator.

Equations

• S.EquationOfMotion xₜ = (S.eulerLagrangeOp xₜ = 0)

Part D.3.I.

We write a simple iff statment for the definition of the equation of motions.

theorem ClassicalMechanics.HarmonicOscillator.equationOfMotion_iff_eulerLagrangeOp (S : HarmonicOscillator) (xₜ : Time → Space 1) : S.EquationOfMotion xₜ ↔ S.eulerLagrangeOp xₜ = 0

E. Newton's second law

We define the force of the harmonic oscillator, and show that the equation of motion is equivalent to Newton's second law.

E.1. The force

We define the force of the harmoic oscillator as the negative gradient of the potential energy, and show that this is equal to - k x.

noncomputable def ClassicalMechanics.HarmonicOscillator.force (S : HarmonicOscillator) (x : Space 1) : EuclideanSpace ℝ (Fin 1)

The force of the classical harmonic oscillator defined as - dU(x)/dx where U(x) is the potential energy.

Equations

• S.force x = -Space.grad S.potentialEnergy x

part E.1.I

We now show that the force is equal to - k x.

theorem ClassicalMechanics.HarmonicOscillator.force_eq_linear (S : HarmonicOscillator) (x : Space 1) : S.force x = -S.k • x

The force on the classical harmonic oscillator is - k x.

E.2. Euler-Lagrange operator and force

We relate the Euler-Lagrange operator to the force, and show the relation to Newton's second law.

theorem ClassicalMechanics.HarmonicOscillator.eulerLagrangeOp_eq_force (S : HarmonicOscillator) (xₜ : Time → Space 1) (hx : ContDiff ℝ (↑⊤) xₜ) : S.eulerLagrangeOp xₜ = fun (t : Time) => S.force (xₜ t) - S.m • Time.deriv (Time.deriv xₜ) t

The Euler lagrange operator corresponds to Newton's second law.

E.3. Equation of motion if and only if Newton's second law

We show that the equation of motion is equivalent to Newton's second law.

theorem ClassicalMechanics.HarmonicOscillator.equationOfMotion_iff_newtons_2nd_law (S : HarmonicOscillator) (xₜ : Time → Space 1) (hx : ContDiff ℝ (↑⊤) xₜ) : S.EquationOfMotion xₜ ↔ ∀ (t : Time), S.m • Time.deriv (Time.deriv xₜ) t = S.force (xₜ t)

F. Energy conservation

In this section we show that any trajectory satisfying the equation of motion conserves energy. This result simply follows from the definition of the energies, and their derivatives, as well as the statement that the equations of motion are equivalent to Newton's second law.

F.1. Energy conservation in terms of time derivatives

We prove that the time derivative of the energy is zero for any trajectory satisfying the equation of motion.

theorem ClassicalMechanics.HarmonicOscillator.energy_conservation_of_equationOfMotion (S : HarmonicOscillator) (xₜ : Time → Space 1) (hx : ContDiff ℝ (↑⊤) xₜ) (h : S.EquationOfMotion xₜ) : Time.deriv (S.energy xₜ) = 0

F.1. Energy conservation in terms of constant energy

We prove that the energy is constant for any trajectory satisfying the equation of motion.

theorem ClassicalMechanics.HarmonicOscillator.energy_conservation_of_equationOfMotion' (S : HarmonicOscillator) (xₜ : Time → Space 1) (hx : ContDiff ℝ (↑⊤) xₜ) (h : S.EquationOfMotion xₜ) (t : Time) : S.energy xₜ t = S.energy xₜ 0

G. Hamiltonian formulation

We now turn to the Hamiltonian formulation of the harmonic oscillator. We define the canonical momentum, the Hamiltonian, and show that the equations of motion are equivalent to Hamilton's equations.

G.1. The canonical momentum

We define the canonical momentum as the gradient of the lagrangian with respect to the velocity.

noncomputable def ClassicalMechanics.HarmonicOscillator.toCanonicalMomentum (S : HarmonicOscillator) (t : Time) (x : Space 1) : EuclideanSpace ℝ (Fin 1) ≃ₗ[ℝ] EuclideanSpace ℝ (Fin 1)

The equivalence between velocity and canonical momentum.

Equations

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

Part G.1.I.

An simple equality for the canonical momentum.

theorem ClassicalMechanics.HarmonicOscillator.toCanonicalMomentum_eq (S : HarmonicOscillator) (t : Time) (x : Space 1) (v : EuclideanSpace ℝ (Fin 1)) : (S.toCanonicalMomentum t x) v = S.m • v

G.2. The Hamiltonian

THe hamiltonian is defined as a function of time, canonical momentum and position, as

H = ⟪p, v⟫ - L(t, x, v)

where v is a function of p and x through the canonical momentum.

noncomputable def ClassicalMechanics.HarmonicOscillator.hamiltonian (S : HarmonicOscillator) (t : Time) (p : EuclideanSpace ℝ (Fin 1)) (x : Space 1) : ℝ

The hamiltonian as a function of time, momentum and position.

Equations

• S.hamiltonian t p x = inner ℝ p ((S.toCanonicalMomentum t x).symm p) - S.lagrangian t x ((S.toCanonicalMomentum t x).symm p)

Part G.2.I.

We prove a simple equality for the Hamiltonian, to help in computations.

theorem ClassicalMechanics.HarmonicOscillator.hamiltonian_eq (S : HarmonicOscillator) : S.hamiltonian = fun (x : Time) (p : EuclideanSpace ℝ (Fin 1)) (x : Space 1) => 1 / 2 * (1 / S.m) * inner ℝ p p + 1 / 2 * S.k * inner ℝ x x

Part G.2.II.

We show that the Hamiltonian is smooth in all its arguments.

theorem ClassicalMechanics.HarmonicOscillator.hamiltonian_contDiff (S : HarmonicOscillator) (n : WithTop ℕ∞) : ContDiff ℝ n ↿S.hamiltonian

Part G.2.II.

We now write down the graidents of the Hamiltonian with respect to the momentum and position.

theorem ClassicalMechanics.HarmonicOscillator.gradient_hamiltonian_position_eq (S : HarmonicOscillator) (t : Time) (x : Space 1) (p : EuclideanSpace ℝ (Fin 1)) : gradient (S.hamiltonian t p) x = S.k • x

theorem ClassicalMechanics.HarmonicOscillator.gradient_hamiltonian_momentum_eq (S : HarmonicOscillator) (t : Time) (x : Space 1) (p : EuclideanSpace ℝ (Fin 1)) : gradient (fun (x_1 : EuclideanSpace ℝ (Fin 1)) => S.hamiltonian t x_1 x) p = (1 / S.m) • p

G.3. Relation between Hamiltonian and energy

We show that the Hamiltonian, when evaluated on any trajectory, is equal to the energy. This is independent of whether the trajectory satisfies the equations of motion or not.

theorem ClassicalMechanics.HarmonicOscillator.hamiltonian_eq_energy (S : HarmonicOscillator) (xₜ : Time → Space 1) : (fun (t : Time) => S.hamiltonian t ((S.toCanonicalMomentum t (xₜ t)) (Time.deriv xₜ t)) (xₜ t)) = S.energy xₜ

G.3. Hamilton equation operator

We define the operator on momentum-position phase-space whose vanishing is equivalent to Hamilton's equations.

noncomputable def ClassicalMechanics.HarmonicOscillator.hamiltonEqOp (S : HarmonicOscillator) (p : Time → EuclideanSpace ℝ (Fin 1)) (q : Time → Space 1) : Time → EuclideanSpace ℝ (Fin 1) × EuclideanSpace ℝ (Fin 1)

The operator on the momentum-position phase-space whose vanishing is equivalent to the hamilton's equations between the momentum and position.

Equations

• S.hamiltonEqOp p q = ClassicalMechanics.hamiltonEqOp S.hamiltonian p q

G.4. Equation of motion if and only if Hamilton's equations

We show that the equation of motion is equivalent to Hamilton's equations, that is to the vanishing of the Hamilton equation operator.

theorem ClassicalMechanics.HarmonicOscillator.equationOfMotion_iff_hamiltonEqOp_eq_zero (S : HarmonicOscillator) (xₜ : Time → Space 1) (hx : ContDiff ℝ (↑⊤) xₜ) : S.EquationOfMotion xₜ ↔ S.hamiltonEqOp (fun (t : Time) => (S.toCanonicalMomentum t (xₜ t)) (Time.deriv xₜ t)) xₜ = 0

H. Equivalences between the different formulations of the equations of motion

We show that the following are equivalent statements for a smooth trajectory xₜ:

• The equation of motion holds. (aka the Euler-Lagrange equations hold.)
• Newton's second law holds.
• Hamilton's equations hold.
• The variational principle for the action holds.
• The Hamilton variational principle holds.

theorem ClassicalMechanics.HarmonicOscillator.equationOfMotion_tfae (S : HarmonicOscillator) (xₜ : Time → Space 1) (hx : ContDiff ℝ (↑⊤) xₜ) : [S.EquationOfMotion xₜ, ∀ (t : Time), S.m • Time.deriv (Time.deriv xₜ) t = S.force (xₜ t), S.hamiltonEqOp (fun (t : Time) => (S.toCanonicalMomentum t (xₜ t)) (Time.deriv xₜ t)) xₜ = 0, varGradient (fun (q' : Time → Space 1) (t : Time) => S.lagrangian t (q' t) ((fderiv ℝ q' t) 1)) xₜ = 0, (varGradient (fun (pq' : Time → EuclideanSpace ℝ (Fin 1) × Space 1) (t : Time) => inner ℝ (pq' t).1 (Time.deriv (Prod.snd ∘ pq') t) - S.hamiltonian t (pq' t).1 (pq' t).2) fun (t : Time) => ((S.toCanonicalMomentum t (xₜ t)) (Time.deriv xₜ t), xₜ t)) = 0].TFAE