The Classical Harmonic Oscillator

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.

@[simp]

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 : ℝ → ℝ) : ℝ → ℝ

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 : ℝ → ℝ) : ℝ → ℝ

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 : ℝ → ℝ) : ℝ → ℝ

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 : ℝ → ℝ) : ℝ → ℝ

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 : ℝ → ℝ) (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.