The Classical Harmonic Oscillator

The solution for given initial conditions

structure ClassicalMechanics.HarmonicOscillator.InitialConditions : Type

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.

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

The zero initial condition

def ClassicalMechanics.HarmonicOscillator.zeroIC : InitialConditions

The zero initial condition.

Equations

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

@[simp]

theorem ClassicalMechanics.HarmonicOscillator.x₀_zeroIC : zeroIC.x₀ = 0

@[simp]

theorem ClassicalMechanics.HarmonicOscillator.v₀_zeroIC : zeroIC.v₀ = 0

The solution

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

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)

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)

theorem ClassicalMechanics.HarmonicOscillator.sol_zeroIC (S : HarmonicOscillator) : S.sol zeroIC = fun (x : ℝ) => 0

For zero initial conditions, the solution is zero.

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

theorem ClassicalMechanics.HarmonicOscillator.amplitude_eq (S : HarmonicOscillator) (IC : InitialConditions) : S.amplitude IC = √(IC.x₀ ^ 2 + (IC.v₀ / S.ω) ^ 2)

@[simp]

theorem ClassicalMechanics.HarmonicOscillator.amplitude_nonneg (S : HarmonicOscillator) (IC : InitialConditions) : 0 ≤ S.amplitude IC

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

theorem ClassicalMechanics.HarmonicOscillator.amplitude_eq_norm (S : HarmonicOscillator) (IC : InitialConditions) : S.amplitude IC = ‖↑IC.x₀ + -↑IC.v₀ / ↑S.ω * Complex.I‖

theorem ClassicalMechanics.HarmonicOscillator.amplitude_sq (S : HarmonicOscillator) (IC : InitialConditions) : S.amplitude IC ^ 2 = IC.x₀ ^ 2 + (IC.v₀ / S.ω) ^ 2

@[simp]

theorem ClassicalMechanics.HarmonicOscillator.amplitude_zeroIC (S : HarmonicOscillator) : S.amplitude zeroIC = 0

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.

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

theorem ClassicalMechanics.HarmonicOscillator.phase_le_pi (S : HarmonicOscillator) (IC : InitialConditions) : S.phase IC ≤ Real.pi

theorem ClassicalMechanics.HarmonicOscillator.neg_pi_lt_phase (S : HarmonicOscillator) (IC : InitialConditions) : -Real.pi < S.phase IC

@[simp]

theorem ClassicalMechanics.HarmonicOscillator.phase_zeroIC (S : HarmonicOscillator) : S.phase zeroIC = 0

theorem ClassicalMechanics.HarmonicOscillator.amplitude_mul_cos_phase (S : HarmonicOscillator) (IC : InitialConditions) : S.amplitude IC * Real.cos (S.phase IC) = IC.x₀

theorem ClassicalMechanics.HarmonicOscillator.amplitude_mul_sin_phase (S : HarmonicOscillator) (IC : InitialConditions) : S.amplitude IC * Real.sin (S.phase IC) = -IC.v₀ / S.ω

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)

theorem ClassicalMechanics.HarmonicOscillator.abs_sol_le_amplitude (S : HarmonicOscillator) (IC : InitialConditions) (t : ℝ) : |S.sol IC t| ≤ S.amplitude IC

@[simp]

theorem ClassicalMechanics.HarmonicOscillator.sol_t_zero (S : HarmonicOscillator) (IC : InitialConditions) : S.sol IC 0 = IC.x₀

theorem ClassicalMechanics.HarmonicOscillator.sol_differentiable (S : HarmonicOscillator) (IC : InitialConditions) : Differentiable ℝ (S.sol IC)

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)

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)

@[simp]

theorem ClassicalMechanics.HarmonicOscillator.sol_velocity_t_zero (S : HarmonicOscillator) (IC : InitialConditions) : deriv (S.sol IC) 0 = IC.v₀

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

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

theorem ClassicalMechanics.HarmonicOscillator.sol_energy (S : HarmonicOscillator) (IC : InitialConditions) : S.energy (S.sol IC) = fun (x : ℝ) => 1 / 2 * (S.m * IC.v₀ ^ 2 + S.k * IC.x₀ ^ 2)

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))

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))))