Solutions to the classical harmonic oscillator #

The solution for given initial conditions #

structure ClassicalMechanics.HarmonicOscillator.InitialConditions :

The initial conditions for the harmonic oscillator specified by an initial position, and an initial velocity.

x₀ : ℝ
The initial position of the harmonic oscillator.
v₀ : ℝ
The initial velocity of the harmonic oscillator.

Instances For

theorem ClassicalMechanics.HarmonicOscillator.InitialConditions.ext {IC₁ IC₂ : InitialConditions} (h1 : IC₁.x₀ = IC₂.x₀) (h2 : IC₁.v₀ = IC₂.v₀) :

IC₁ = IC₂

source

theorem ClassicalMechanics.HarmonicOscillator.InitialConditions.ext_iff {IC₁ IC₂ : InitialConditions} :

IC₁ = IC₂ ↔ IC₁.x₀ = IC₂.x₀ ∧ IC₁.v₀ = IC₂.v₀

The zero initial condition #

source

def ClassicalMechanics.HarmonicOscillator.zeroIC :

InitialConditions

The zero initial condition.

Equations

ClassicalMechanics.HarmonicOscillator.zeroIC = { x₀ := 0, v₀ := 0 }

Instances For

source

@[simp]

theorem ClassicalMechanics.HarmonicOscillator.x₀_zeroIC :

zeroIC.x₀ = 0

The zero initial condition has zero starting point.

source

@[simp]

theorem ClassicalMechanics.HarmonicOscillator.v₀_zeroIC :

zeroIC.v₀ = 0

The zero initial condition has zero starting velocity.

The solution #

source

noncomputable def ClassicalMechanics.HarmonicOscillator.sol (S : HarmonicOscillator) (IC : InitialConditions) :

Time → ℝ

Given initial conditions, the solution to the classical harmonic oscillator.

Equations

S.sol IC t = IC.x₀ * Real.cos (S.ω * t) + IC.v₀ / S.ω * Real.sin (S.ω * t)

Instances For

source

theorem ClassicalMechanics.HarmonicOscillator.sol_eq (S : HarmonicOscillator) (IC : InitialConditions) :

S.sol IC = fun (t : ℝ) => IC.x₀ * Real.cos (S.ω * t) + IC.v₀ / S.ω * Real.sin (S.ω * t)

source

theorem ClassicalMechanics.HarmonicOscillator.sol_zeroIC (S : HarmonicOscillator) :

S.sol zeroIC = fun (x : Time) => 0

For zero initial conditions, the solution is zero.

source

noncomputable def ClassicalMechanics.HarmonicOscillator.amplitude (S : HarmonicOscillator) (IC : InitialConditions) :

ℝ

Given initial conditions, the amplitude of the classical harmonic oscillator.

Equations

S.amplitude IC = (↑polarCoord (IC.x₀, IC.v₀ / S.ω)).1

Instances For

source

theorem ClassicalMechanics.HarmonicOscillator.amplitude_eq (S : HarmonicOscillator) (IC : InitialConditions) :

S.amplitude IC = √(IC.x₀ ^ 2 + (IC.v₀ / S.ω) ^ 2)

source

@[simp]

theorem ClassicalMechanics.HarmonicOscillator.amplitude_nonneg (S : HarmonicOscillator) (IC : InitialConditions) :

0 ≤ S.amplitude IC

The amplitude of the classical harmonic oscillator is non-negative.

source

theorem ClassicalMechanics.HarmonicOscillator.amplitude_eq_norm (S : HarmonicOscillator) (IC : InitialConditions) :

S.amplitude IC = ‖↑IC.x₀ + -↑IC.v₀ / ↑S.ω * Complex.I ‖

source

theorem ClassicalMechanics.HarmonicOscillator.amplitude_sq (S : HarmonicOscillator) (IC : InitialConditions) :

S.amplitude IC ^ 2 = IC.x₀ ^ 2 + (IC.v₀ / S.ω) ^ 2

source

@[simp]

theorem ClassicalMechanics.HarmonicOscillator.amplitude_zeroIC (S : HarmonicOscillator) :

S.amplitude zeroIC = 0

source

theorem ClassicalMechanics.HarmonicOscillator.amplitude_eq_zero_iff_IC_eq_zeroIC (S : HarmonicOscillator) (IC : InitialConditions) :

S.amplitude IC = 0 ↔ IC = zeroIC

The amplitude is zero if and only if the inital conditions are zero.

source

noncomputable def ClassicalMechanics.HarmonicOscillator.phase (S : HarmonicOscillator) (IC : InitialConditions) :

ℝ

Given initial conditions, the phase of the classical harmonic oscillator.

Equations

S.phase IC = (↑polarCoord (IC.x₀, -IC.v₀ / S.ω)).2

Instances For

source

theorem ClassicalMechanics.HarmonicOscillator.phase_le_pi (S : HarmonicOscillator) (IC : InitialConditions) :

S.phase IC ≤ Real.pi

source

theorem ClassicalMechanics.HarmonicOscillator.neg_pi_lt_phase (S : HarmonicOscillator) (IC : InitialConditions) :

-Real.pi < S.phase IC

source

@[simp]

theorem ClassicalMechanics.HarmonicOscillator.phase_zeroIC (S : HarmonicOscillator) :

S.phase zeroIC = 0

source

theorem ClassicalMechanics.HarmonicOscillator.amplitude_mul_cos_phase (S : HarmonicOscillator) (IC : InitialConditions) :

S.amplitude IC * Real.cos (S.phase IC) = IC.x₀

source

theorem ClassicalMechanics.HarmonicOscillator.amplitude_mul_sin_phase (S : HarmonicOscillator) (IC : InitialConditions) :

S.amplitude IC * Real.sin (S.phase IC) = -IC.v₀ / S.ω

source

theorem ClassicalMechanics.HarmonicOscillator.sol_eq_amplitude_mul_cos_phase (S : HarmonicOscillator) (IC : InitialConditions) :

S.sol IC = fun (t : ℝ) => S.amplitude IC * Real.cos (S.ω * t + S.phase IC)

source

theorem ClassicalMechanics.HarmonicOscillator.abs_sol_le_amplitude (S : HarmonicOscillator) (IC : InitialConditions) (t : ℝ) :

|S.sol IC t| ≤ S.amplitude IC

For any time the position of the harmonic oscillator is less then the amplitude.

source

@[simp]

theorem ClassicalMechanics.HarmonicOscillator.sol_t_zero (S : HarmonicOscillator) (IC : InitialConditions) :

S.sol IC 0 = IC.x₀

For a set of initial conditions IC the position of the solution at time 0 is IC.x₀.

source

theorem ClassicalMechanics.HarmonicOscillator.sol_differentiable (S : HarmonicOscillator) (IC : InitialConditions) :

Differentiable ℝ (S.sol IC)

The solutions are differentiable.

source

theorem ClassicalMechanics.HarmonicOscillator.sol_velocity (S : HarmonicOscillator) (IC : InitialConditions) :

deriv (S.sol IC) = fun (t : ℝ) => -IC.x₀ * S.ω * Real.sin (S.ω * t) + IC.v₀ * Real.cos (S.ω * t)

source

theorem ClassicalMechanics.HarmonicOscillator.sol_velocity_amplitude_phase (S : HarmonicOscillator) (IC : InitialConditions) :

deriv (S.sol IC) = fun (t : ℝ) => -S.amplitude IC * S.ω * Real.sin (S.ω * t + S.phase IC)

source

@[simp]

theorem ClassicalMechanics.HarmonicOscillator.sol_velocity_t_zero (S : HarmonicOscillator) (IC : InitialConditions) :

deriv (S.sol IC) 0 = IC.v₀

source

theorem ClassicalMechanics.HarmonicOscillator.sol_potentialEnergy (S : HarmonicOscillator) (IC : InitialConditions) :

S.potentialEnergy (S.sol IC) = fun (t : ℝ) => 1 / 2 * (S.k * IC.x₀ ^ 2 + S.m * IC.v₀ ^ 2) * Real.cos (S.ω * t + S.phase IC) ^ 2

source

theorem ClassicalMechanics.HarmonicOscillator.sol_kineticEnergy (S : HarmonicOscillator) (IC : InitialConditions) :

S.kineticEnergy (S.sol IC) = fun (t : ℝ) => 1 / 2 * (S.k * IC.x₀ ^ 2 + S.m * IC.v₀ ^ 2) * Real.sin (S.ω * t + S.phase IC) ^ 2

source

theorem ClassicalMechanics.HarmonicOscillator.sol_energy (S : HarmonicOscillator) (IC : InitialConditions) :

S.energy (S.sol IC) = fun (x : Time) => 1 / 2 * (S.m * IC.v₀ ^ 2 + S.k * IC.x₀ ^ 2)

source

theorem ClassicalMechanics.HarmonicOscillator.sol_lagrangian (S : HarmonicOscillator) (IC : InitialConditions) :

S.lagrangian (S.sol IC) = fun (t : ℝ) => -1 / 2 * (S.m * IC.v₀ ^ 2 + S.k * IC.x₀ ^ 2) * Real.cos (2 * (S.ω * t + S.phase IC))

source

theorem ClassicalMechanics.HarmonicOscillator.sol_action (S : HarmonicOscillator) (IC : InitialConditions) (t1 t2 : ℝ) :

∫ (t' : ℝ) in t1..t2, S.lagrangian (S.sol IC) t' = -1 / 2 * (S.m * IC.v₀ ^ 2 + S.k * IC.x₀ ^ 2) * (S.ω⁻¹ * 2⁻¹ * (Real.sin (2 * (S.ω * t2 + S.phase IC)) - Real.sin (2 * (S.ω * t1 + S.phase IC))))

Some semi-formal results #

source

theorem ClassicalMechanics.HarmonicOscillator.sol_equationOfMotion (S : HarmonicOscillator) (IC : InitialConditions) :

EquationOfMotion (S.sol IC)

The solutions for any initial condition solve the equation of motion.

source

theorem ClassicalMechanics.HarmonicOscillator.sol_unique (S : HarmonicOscillator) (IC : InitialConditions) (x : Time → ℝ) :

EquationOfMotion x ∧ x 0 = IC.x₀ ∧ deriv x 0 = IC.v₀ → x = S.sol IC

The solutions 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.

PhysLean Documentation

PhysLean.ClassicalMechanics.HarmonicOscillator.Solution

Solutions to the classical harmonic oscillator #

The solution for given initial conditions #

The zero initial condition #

The solution #

Some semi-formal results #