The Damped Harmonic Oscillator

i. Overview

The damped harmonic oscillator is a classical mechanical system corresponding to a mass m under a restoring force - k x and a damping force - γ ẋ, where k is the spring constant, γ is the damping coefficient, x is the position, and ẋ is the velocity.

The equation of motion for the damped harmonic oscillator is:

m ẍ + γ ẋ + k x = 0

Depending on the relationship between the damping coefficient and the natural frequency, the system exhibits three different behaviors:

• Underdamped (γ² < 4mk) : Oscillatory motion with exponentially decaying amplitude
• Critically damped (γ² = 4mk) : Fastest return to equilibrium without oscillation
• Overdamped (γ² > 4mk) : Slow return to equilibrium without oscillation

ii. Key results

This module is currently a placeholder for future implementation. The following results are planned to be formalized:

• DampedHarmonicOscillator: Structure containing the input data (mass, spring constant, damping coefficient)
• EquationOfMotion: The equation of motion for the damped harmonic oscillator
• Solutions for underdamped, critically damped, and overdamped cases
• Energy dissipation properties
• Quality factor and relaxation time

iii. Table of contents

• A. The input data (to be implemented)
• B. The damped angular frequency (to be implemented)
• C. The energies and energy dissipation (to be implemented)
• D. The equation of motion (to be implemented)
• E. Solutions (to be implemented)
  • E.1. Underdamped case
  • E.2. Critically damped case
  • E.3. Overdamped case
• F. Quality factor and decay time (to be implemented)

iv. References

References for the damped harmonic oscillator include:

• Landau & Lifshitz, Mechanics, page 76, section 25.
• Goldstein, Classical Mechanics, Chapter 2.

A. The input data (placeholder)

The input data for the damped harmonic oscillator will consist of:

• Mass m > 0
• Spring constant k > 0
• Damping coefficient γ ≥ 0

structure ClassicalMechanics.DampedHarmonicOscillator : Type

Placeholder structure for the damped harmonic oscillator. The damped harmonic oscillator is specified by a mass m, a spring constant k, and a damping coefficient γ. All parameters are assumed to be positive (or non-negative for the damping coefficient).

• m : ℝ

  The mass of the oscillator.

• k : ℝ

  The spring constant of the oscillator.

• γ : ℝ

  The damping coefficient of the oscillator.

• m_pos : 0 < self.m
• k_pos : 0 < self.k
• γ_nonneg : 0 ≤ self.γ

@[simp]

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

@[simp]

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

B. The natural angular frequency (placeholder)

The natural angular frequency ω₀ = √(k/m) will be defined here.

noncomputable def ClassicalMechanics.DampedHarmonicOscillator.ω₀ (S : DampedHarmonicOscillator) : ℝ

The natural (undamped) angular frequency of the oscillator, ω₀ = √(k/m).

Equations

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

@[simp]

theorem ClassicalMechanics.DampedHarmonicOscillator.ω₀_pos (S : DampedHarmonicOscillator) : 0 < S.ω₀

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

C. Equation of motion (Tag: DHO03)

The damped harmonic oscillator with mass m, spring constant k, and damping coefficient γ satisfies

m ẍ + γ ẋ + k x = 0,

where x : Time → ℝ is the position as a function of time.

noncomputable def ClassicalMechanics.DampedHarmonicOscillator.EquationOfMotion (S : DampedHarmonicOscillator) (x : Time → ℝ) : Prop

The equation of motion for the damped harmonic oscillator.

A function x : Time → ℝ is a solution if it satisfies

S.m * x¨ + S.γ * ẋ + S.k * x = 0

for all times t.

Equations

• S.EquationOfMotion x = ∀ (t : Time), S.m * Time.deriv (Time.deriv x) t + S.γ * Time.deriv x t + S.k * x t = 0

D. The energies and energy dissipation (Tag: DHO04)

For the damped harmonic oscillator, the mechanical energy is

E(t) = ½ S.m (ẋ(t))^2 + ½ S.k (x(t))^2,

where x : Time → ℝ is the position as a function of time.

If x satisfies the equation of motion

S.m * x¨ + S.γ * ẋ + S.k * x = 0,

then differentiating E with respect to time and substituting the equation of motion yields

dE/dt = - S.γ * (ẋ(t))^2 ≤ 0

Thus the energy is non-increasing in time, and it is strictly decreasing whenever S.γ > 0 and ẋ(t) ≠ 0. In particular, for S.γ > 0 the energy is not conserved, and the energy dissipation rate is proportional to the squared velocity.

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

The kinetic energy of the damped harmonic oscillator.

Equations

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

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

The potential energy of the damped harmonic oscillator.

Equations

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

noncomputable def ClassicalMechanics.DampedHarmonicOscillator.energy (S : DampedHarmonicOscillator) (x : Time → ℝ) : Time → ℝ

Mechanical energy of the damped harmonic oscillator.

Equations

• S.energy x = S.kineticEnergy x + S.potentialEnergy x

noncomputable def ClassicalMechanics.DampedHarmonicOscillator.energyDissipationRate (S : DampedHarmonicOscillator) (x : Time → ℝ) : Time → ℝ

Energy dissipation rate along a trajectory x : Time → ℝ.

if x satisfies S.equationOfMotion x, then

Time.deriv (S.energy x) t = - S.γ * (Time.deriv x t)^2,

so the energy is non-increasing and not conserved when S.γ > 0.

Equations

• S.energyDissipationRate x t = -S.γ * Time.deriv x t ^ 2

E. Damping regimes (placeholder)

The three damping regimes will be defined based on the discriminant γ² - 4mk.

noncomputable def ClassicalMechanics.DampedHarmonicOscillator.discriminant (S : DampedHarmonicOscillator) : ℝ

The discriminant that determines the damping regime.

Equations

• S.discriminant = S.γ ^ 2 - 4 * S.m * S.k

def ClassicalMechanics.DampedHarmonicOscillator.IsUnderdamped (S : DampedHarmonicOscillator) : Prop

The system is underdamped when γ² < 4mk.

Equations

• S.IsUnderdamped = (S.discriminant < 0)

def ClassicalMechanics.DampedHarmonicOscillator.IsCriticallyDamped (S : DampedHarmonicOscillator) : Prop

The system is critically damped when γ² = 4mk.

Equations

• S.IsCriticallyDamped = (S.discriminant = 0)

def ClassicalMechanics.DampedHarmonicOscillator.IsOverdamped (S : DampedHarmonicOscillator) : Prop

The system is overdamped when γ² > 4mk.

Equations

• S.IsOverdamped = (S.discriminant > 0)