The Classical Harmonic Oscillator

Description

The classical harmonic oscillator is a classical mechanics system. It physically corresponds to a particle of mass m attached to a spring providing a force of - k x.

Current status

Basic

The main components of the basic module (this module) are:

• The structure HarmonicOscillator containing the physical parameters of the system.
• The definition of the lagrangian lagrangian of the system.

Solution

The main components of the Solution module are:

• The structure InitialConditions containing the initial conditions of the system.
• The definition sol which given a set of initial conditions is the solution to the Harmonic Oscillator.
• The energy sol_energy of each solution.
• The action sol_action of each solution.

TODOs

There are a number of TODOs related to the classical harmonic oscillator. These include:

• 6VZGU: Deriving the force from the lagrangian.
• 6VZG4: Deriving the Euler-Lagrange equations.
• 6YATB: Show that the solutions satisfy the equations of motion (the Euler-Lagrange equations).
• 6VZHC: Include damping into the harmonic oscillator.

Note the item TODO 6YATB. In particular it is yet to be shown that the solutions satisfy the equation of motion.

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

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

The angular frequence 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 frequence of the classical harmonic osscilator is positive.

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

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

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

The angular frequence 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 frequence of the classical harmonic osscilator is m/k.

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

The kinetic energy of the harmonic oscillator is 1/2 m (dx/dt) ^ 2.

Equations

• S.kineticEnergy x t = 1 / 2 * S.m * deriv x t ^ 2

noncomputable def ClassicalMechanics.HarmonicOscillator.potentialEnergy (S : HarmonicOscillator) (x : Time → ℝ) : Time → ℝ

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

Equations

• S.potentialEnergy x t = 1 / 2 * S.k * x t ^ 2

noncomputable def ClassicalMechanics.HarmonicOscillator.energy (S : HarmonicOscillator) (x : Time → ℝ) : 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

noncomputable def ClassicalMechanics.HarmonicOscillator.lagrangian (S : HarmonicOscillator) (x : Time → ℝ) : Time → ℝ

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

Equations

• S.lagrangian x t = S.kineticEnergy x t - S.potentialEnergy x t

theorem ClassicalMechanics.HarmonicOscillator.lagrangian_parity (S : HarmonicOscillator) (x : Time → ℝ) (hx : Differentiable ℝ x) : S.lagrangian (-x) = S.lagrangian x

The lagrangian of the classical harmonic oscillator obeys the condition

lagrangian S (- x) = lagrangian S x.