Imports
/-
Copyright (c) 2026 Florian Wiesner. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Giuseppe Sorge, Florian Wiesner
-/
module
public import Physlib.ClassicalMechanics.DampedHarmonicOscillator.Basic
public import Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
public import Mathlib.Analysis.ODE.ExistUniqueSolutions to the damped harmonic oscillator
i. Overview
In this module we define the solution to the damped harmonic oscillator for given initial conditions and prove that it satisfies the equation of motion. The solution selects the appropriate closed form from the sign of the discriminant: trigonometric for the underdamped case, polynomial for the critically damped case, and hyperbolic for the overdamped case.
ii. Key results
InitialConditions is a structure for the initial position and velocity.
trajectory selects the appropriate regime-specific trajectory from the sign of the
discriminant.
trajectory_equationOfMotion_of_underdamped,
trajectory_equationOfMotion_of_criticallyDamped, and
trajectory_equationOfMotion_of_overdamped prove the selected trajectory satisfies the
equation of motion in each damping regime.
trajectory_equationOfMotion proves that the selected trajectory satisfies the equation
of motion.
equationOfMotion_unique proves that two smooth solutions with the same initial data agree, and
trajectories_unique proves that the selected trajectory is the unique solution with the given
initial conditions.
iii. Table of contents
A. The initial conditions
B. Trajectories associated with the initial conditions
B.1. Regime-specific base trajectories
B.2. The selected trajectory
B.3. Shared calculus lemmas
B.4. Derivatives of the base trajectories
C. Trajectories and equation of motion
C.1. The selected trajectory satisfies the equation of motion
C.2. Uniqueness of the solutions
iv. References
References for the damped harmonic oscillator include:
Landau & Lifshitz, Mechanics, page 76, section 25.
Goldstein, Classical Mechanics, Chapter 2.
@[expose] public sectionA. The initial conditions
We define the type of initial conditions for the damped harmonic oscillator. The initial
conditions are the position and velocity at time 0.
The initial conditions for the damped harmonic oscillator, specified by an initial position and an initial velocity.
The initial position of the damped harmonic oscillator.
The initial velocity of the damped harmonic oscillator.
@[ext]
structure InitialConditions where x₀ : EuclideanSpace ℝ (Fin 1) v₀ : EuclideanSpace ℝ (Fin 1)B. Trajectories associated with the initial conditions
For each damping regime, we give an explicit formula for the trajectory with the specified initial conditions.
B.1. Regime-specific base trajectories
B.2. The selected trajectory
In the underdamped regime, the selected trajectory uses the trigonometric base.
lemma trajectory_eq_of_underdamped (IC : InitialConditions) (hS : S.IsUnderdamped) :
S.trajectory IC =
fun t : Time => exp (-S.decayRate * t) • S.underdampedBase IC t := S:DampedHarmonicOscillatorIC:InitialConditionshS:S.IsUnderdamped⊢ S.trajectory IC = fun t => rexp (-S.decayRate * t.val) • S.underdampedBase IC t
classical
All goals completed! 🐙In the critically damped regime, the selected trajectory uses the polynomial base.
S:DampedHarmonicOscillatorIC:InitialConditionshS:S.IsCriticallyDampedhnotUnder:¬S.IsUnderdamped⊢ S.trajectory IC = fun t => rexp (-S.decayRate * t.val) • S.criticallyDampedBase IC t
All goals completed! 🐙In the overdamped regime, the selected trajectory uses the hyperbolic base.
S:DampedHarmonicOscillatorIC:InitialConditionshS:0 < S.discriminanthnotUnder:¬S.IsUnderdampedhnotCritical:¬S.IsCriticallyDamped⊢ S.trajectory IC = fun t => rexp (-S.decayRate * t.val) • S.overdampedBase IC t
All goals completed! 🐙The selected trajectory is smooth.
S:DampedHarmonicOscillatorIC:InitialConditionshS:S.IsOverdamped⊢ ContDiff ℝ ∞ fun t => rexp (-S.decayRate * t.val) • S.overdampedBase IC t
S:DampedHarmonicOscillatorIC:InitialConditionshS:S.IsOverdamped⊢ ContDiff ℝ ∞ fun t =>
rexp (-S.decayRate * t.val) •
(Real.cosh (S.angularFrequency * t.val) • IC.x₀ +
(Real.sinh (S.angularFrequency * t.val) / S.angularFrequency) • (IC.v₀ + S.decayRate • IC.x₀))
All goals completed! 🐙
The selected trajectory has initial position IC.x₀.
S:DampedHarmonicOscillatorIC:InitialConditionshS:S.IsOverdamped⊢ (fun t => rexp (-S.decayRate * t.val) • S.overdampedBase IC t) 0 = IC.x₀
All goals completed! 🐙B.3. Shared calculus lemmas
The three solution formulas all have the form exp (-a * t) • y t. The following private
lemmas compute the first and second derivatives of that expression and package the common
equation-of-motion argument.
a:ℝy:Time → EuclideanSpace ℝ (Fin 1)hy:Differentiable ℝ yt:Time⊢ rexp (-a * t.val) • ∂ₜ y t + (rexp (-a * t.val) * (-a * 1 + t.val * -0 1)) • y t =
rexp (-a * t.val) • (∂ₜ y t - a • y t)
a:ℝy:Time → EuclideanSpace ℝ (Fin 1)hy:Differentiable ℝ yt:Time⊢ rexp (-(a * t.val)) • ∂ₜ y t + -((rexp (-(a * t.val)) * a) • y t) =
rexp (-(a * t.val)) • ∂ₜ y t - (rexp (-(a * t.val)) * a) • y t
All goals completed! 🐙a:ℝμ:ℝy:Time → EuclideanSpace ℝ (Fin 1)hy:Differentiable ℝ yhdy:Differentiable ℝ (∂ₜ y)hy'':∂ₜ (∂ₜ y) = fun t => μ • y tt:Timehy''_t:(fderiv ℝ (∂ₜ y) t) 1 = μ • y t⊢ rexp (-a * t.val) • (μ • y t - a • ∂ₜ y t) + (rexp (-a * t.val) * (-a * 1 + t.val * -0 1)) • (∂ₜ y t - a • y t) =
rexp (-a * t.val) • (μ • y t - (2 * a) • ∂ₜ y t + a ^ 2 • y t)
a:ℝμ:ℝy:Time → EuclideanSpace ℝ (Fin 1)hy:Differentiable ℝ yhdy:Differentiable ℝ (∂ₜ y)hy'':∂ₜ (∂ₜ y) = fun t => μ • y tt:Timehy''_t:(fderiv ℝ (∂ₜ y) t) 1 = μ • y t⊢ (rexp (-(a * t.val)) * μ) • y t - (rexp (-(a * t.val)) * a) • ∂ₜ y t +
(-((rexp (-(a * t.val)) * a) • ∂ₜ y t) + (rexp (-(a * t.val)) * a * a) • y t) =
(rexp (-(a * t.val)) * μ) • y t - (rexp (-(a * t.val)) * (2 * a)) • ∂ₜ y t + (rexp (-(a * t.val)) * a ^ 2) • y t
All goals completed! 🐙S:DampedHarmonicOscillatora:ℝμ:ℝy:Time → EuclideanSpace ℝ (Fin 1)hy:Differentiable ℝ yhdy:Differentiable ℝ (∂ₜ y)hy'':∂ₜ (∂ₜ y) = fun t => μ • y thγ:S.γ = 2 * S.m * ahk:S.k = S.m * (a ^ 2 - μ)t:Time⊢ S.m • (fun t => rexp (-a * t.val) • (μ • y t - (2 * a) • ∂ₜ y t + a ^ 2 • y t)) t +
(2 * S.m * a) • (fun t => rexp (-a * t.val) • (∂ₜ y t - a • y t)) t +
(S.m * (a ^ 2 - μ)) • (fun t => rexp (-a * t.val) • y t) t =
0
S:DampedHarmonicOscillatora:ℝμ:ℝy:Time → EuclideanSpace ℝ (Fin 1)hy:Differentiable ℝ yhdy:Differentiable ℝ (∂ₜ y)hy'':∂ₜ (∂ₜ y) = fun t => μ • y thγ:S.γ = 2 * S.m * ahk:S.k = S.m * (a ^ 2 - μ)t:Time⊢ (S.m * (rexp (-(a * t.val)) * μ)) • y t - (S.m * (rexp (-(a * t.val)) * (2 * a))) • ∂ₜ y t +
(S.m * (rexp (-(a * t.val)) * a ^ 2)) • y t +
((2 * S.m * a * rexp (-(a * t.val))) • ∂ₜ y t - (2 * S.m * a * (rexp (-(a * t.val)) * a)) • y t) +
(S.m * (a ^ 2 - μ) * rexp (-(a * t.val))) • y t =
0
All goals completed! 🐙B.4. Derivatives of the base trajectories
The remaining private lemmas compute the velocity and acceleration of the trigonometric, polynomial, and hyperbolic base trajectories before the exponential decay factor is applied.
S:DampedHarmonicOscillatorIC:InitialConditionst:Time⊢ (0 t + (fderiv ℝ val t).smulRight (IC.v₀ + S.decayRate • IC.x₀)) 1 = IC.v₀ + S.decayRate • IC.x₀
All goals completed! 🐙S:DampedHarmonicOscillatorIC:InitialConditions⊢ (∂ₜ fun x => IC.v₀ + S.decayRate • IC.x₀) = fun x => 0
S:DampedHarmonicOscillatorIC:InitialConditionst:Time⊢ ∂ₜ (fun x => IC.v₀ + S.decayRate • IC.x₀) t = 0
All goals completed! 🐙S:DampedHarmonicOscillatorIC:InitialConditionshS:S.IsUnderdampedhΩ:S.angularFrequency ≠ 0t:Timefderiv_comp_val_eq_deriv:∀ (g : ℝ → ℝ), DifferentiableAt ℝ g t.val → (fderiv ℝ (fun s => g s.val) t) 1 = _root_.deriv g t.val⊢ _root_.deriv (fun s => Real.cos (S.angularFrequency * s)) t.val • IC.x₀ +
_root_.deriv (fun s => Real.sin (S.angularFrequency * s) / S.angularFrequency) t.val •
(IC.v₀ + S.decayRate • IC.x₀) =
(-S.angularFrequency * Real.sin (S.angularFrequency * t.val)) • IC.x₀ +
Real.cos (S.angularFrequency * t.val) • (IC.v₀ + S.decayRate • IC.x₀)
All goals completed! 🐙S:DampedHarmonicOscillatorIC:InitialConditionshS:S.IsUnderdampedhΩ:S.angularFrequency ≠ 0t:Timefderiv_comp_val_eq_deriv:∀ (g : ℝ → ℝ), DifferentiableAt ℝ g t.val → (fderiv ℝ (fun s => g s.val) t) 1 = _root_.deriv g t.val⊢ _root_.deriv (fun s => -S.angularFrequency * Real.sin (S.angularFrequency * s)) t.val • IC.x₀ +
_root_.deriv (fun s => Real.cos (S.angularFrequency * s)) t.val • (IC.v₀ + S.decayRate • IC.x₀) =
-S.angularFrequency ^ 2 •
(Real.cos (S.angularFrequency * t.val) • IC.x₀ +
(Real.sin (S.angularFrequency * t.val) / S.angularFrequency) • (IC.v₀ + S.decayRate • IC.x₀))
S:DampedHarmonicOscillatorIC:InitialConditionshS:S.IsUnderdampedhΩ:S.angularFrequency ≠ 0t:Timefderiv_comp_val_eq_deriv:∀ (g : ℝ → ℝ), DifferentiableAt ℝ g t.val → (fderiv ℝ (fun s => g s.val) t) 1 = _root_.deriv g t.val⊢ -((S.angularFrequency * (S.angularFrequency * Real.cos (t.val * S.angularFrequency))) • IC.x₀) +
(-((S.angularFrequency * Real.sin (t.val * S.angularFrequency)) • IC.v₀) +
-((S.angularFrequency * Real.sin (t.val * S.angularFrequency) * S.decayRate) • IC.x₀)) =
-((S.angularFrequency ^ 2 * Real.cos (t.val * S.angularFrequency)) • IC.x₀) +
(-((S.angularFrequency ^ 2 * (Real.sin (t.val * S.angularFrequency) / S.angularFrequency)) • IC.v₀) +
-((S.angularFrequency ^ 2 * (Real.sin (t.val * S.angularFrequency) / S.angularFrequency * S.decayRate)) • IC.x₀))
All goals completed! 🐙S:DampedHarmonicOscillatorIC:InitialConditionshS:S.IsOverdampedhΩ:S.angularFrequency ≠ 0t:Timefderiv_comp_val_eq_deriv:∀ (g : ℝ → ℝ), DifferentiableAt ℝ g t.val → (fderiv ℝ (fun s => g s.val) t) 1 = _root_.deriv g t.val⊢ _root_.deriv (fun s => Real.cosh (S.angularFrequency * s)) t.val • IC.x₀ +
_root_.deriv (fun s => Real.sinh (S.angularFrequency * s) / S.angularFrequency) t.val •
(IC.v₀ + S.decayRate • IC.x₀) =
(S.angularFrequency * Real.sinh (S.angularFrequency * t.val)) • IC.x₀ +
Real.cosh (S.angularFrequency * t.val) • (IC.v₀ + S.decayRate • IC.x₀)
All goals completed! 🐙S:DampedHarmonicOscillatorIC:InitialConditionshS:S.IsOverdampedhΩ:S.angularFrequency ≠ 0t:Timefderiv_comp_val_eq_deriv:∀ (g : ℝ → ℝ), DifferentiableAt ℝ g t.val → (fderiv ℝ (fun s => g s.val) t) 1 = _root_.deriv g t.val⊢ _root_.deriv (fun s => S.angularFrequency * Real.sinh (S.angularFrequency * s)) t.val • IC.x₀ +
_root_.deriv (fun s => Real.cosh (S.angularFrequency * s)) t.val • (IC.v₀ + S.decayRate • IC.x₀) =
S.angularFrequency ^ 2 •
(Real.cosh (S.angularFrequency * t.val) • IC.x₀ +
(Real.sinh (S.angularFrequency * t.val) / S.angularFrequency) • (IC.v₀ + S.decayRate • IC.x₀))
S:DampedHarmonicOscillatorIC:InitialConditionshS:S.IsOverdampedhΩ:S.angularFrequency ≠ 0t:Timefderiv_comp_val_eq_deriv:∀ (g : ℝ → ℝ), DifferentiableAt ℝ g t.val → (fderiv ℝ (fun s => g s.val) t) 1 = _root_.deriv g t.val⊢ (S.angularFrequency * (S.angularFrequency * Real.cosh (t.val * S.angularFrequency))) • IC.x₀ +
((S.angularFrequency * Real.sinh (t.val * S.angularFrequency)) • IC.v₀ +
(S.angularFrequency * Real.sinh (t.val * S.angularFrequency) * S.decayRate) • IC.x₀) =
(S.angularFrequency ^ 2 * Real.cosh (t.val * S.angularFrequency)) • IC.x₀ +
((S.angularFrequency ^ 2 * (Real.sinh (t.val * S.angularFrequency) / S.angularFrequency)) • IC.v₀ +
(S.angularFrequency ^ 2 * (Real.sinh (t.val * S.angularFrequency) / S.angularFrequency * S.decayRate)) • IC.x₀)
All goals completed! 🐙
The selected trajectory has initial velocity IC.v₀.
S:DampedHarmonicOscillatorIC:InitialConditionshS:S.IsOverdamped⊢ (fun t =>
rexp (-S.decayRate * t.val) •
((fun t =>
(S.angularFrequency * Real.sinh (S.angularFrequency * t.val)) • IC.x₀ +
Real.cosh (S.angularFrequency * t.val) • (IC.v₀ + S.decayRate • IC.x₀))
t -
S.decayRate • S.overdampedBase IC t))
0 =
IC.v₀
All goals completed! 🐙C. Trajectories and equation of motion
The regime-specific trajectories satisfy the equation of motion for the damped harmonic oscillator.
C.1. The selected trajectory satisfies the equation of motion
In the critically damped regime, the selected trajectory satisfies the damped equation of motion.
S:DampedHarmonicOscillatorIC:InitialConditionshS:S.IsCriticallyDampedhγ:S.γ = 2 * S.m * S.decayRatehk:S.k = S.m * (S.decayRate ^ 2 - 0)⊢ Differentiable ℝ fun x => IC.v₀ + S.decayRate • IC.x₀
All goals completed! 🐙) ?_ hγ hk
All goals completed! 🐙In the underdamped regime, the selected trajectory satisfies the damped equation of motion.
S:DampedHarmonicOscillatorIC:InitialConditionshS:S.IsUnderdampedhγ:S.γ = 2 * S.m * S.decayRatehk:S.k = S.m * (S.decayRate ^ 2 - -S.angularFrequency ^ 2)⊢ Differentiable ℝ fun t =>
(-S.angularFrequency * Real.sin (S.angularFrequency * t.val)) • IC.x₀ +
Real.cos (S.angularFrequency * t.val) • (IC.v₀ + S.decayRate • IC.x₀)
All goals completed! 🐙In the overdamped regime, the selected trajectory satisfies the damped equation of motion.
S:DampedHarmonicOscillatorIC:InitialConditionshS:S.IsOverdampedhγ:S.γ = 2 * S.m * S.decayRatehk:S.k = S.m * (S.decayRate ^ 2 - S.angularFrequency ^ 2)⊢ Differentiable ℝ fun t =>
(S.angularFrequency * Real.sinh (S.angularFrequency * t.val)) • IC.x₀ +
Real.cosh (S.angularFrequency * t.val) • (IC.v₀ + S.decayRate • IC.x₀)
All goals completed! 🐙The selected trajectory satisfies the damped equation of motion.
lemma trajectory_equationOfMotion (IC : InitialConditions) :
S.EquationOfMotion (S.trajectory IC) := S:DampedHarmonicOscillatorIC:InitialConditions⊢ S.EquationOfMotion (S.trajectory IC)
S:DampedHarmonicOscillatorIC:InitialConditionshS:S.IsUnderdamped⊢ S.EquationOfMotion (S.trajectory IC)S:DampedHarmonicOscillatorIC:InitialConditionshS:S.IsCriticallyDamped⊢ S.EquationOfMotion (S.trajectory IC)S:DampedHarmonicOscillatorIC:InitialConditionshS:S.IsOverdamped⊢ S.EquationOfMotion (S.trajectory IC)
S:DampedHarmonicOscillatorIC:InitialConditionshS:S.IsUnderdamped⊢ S.EquationOfMotion (S.trajectory IC) All goals completed! 🐙
S:DampedHarmonicOscillatorIC:InitialConditionshS:S.IsCriticallyDamped⊢ S.EquationOfMotion (S.trajectory IC) All goals completed! 🐙
S:DampedHarmonicOscillatorIC:InitialConditionshS:S.IsOverdamped⊢ S.EquationOfMotion (S.trajectory IC) All goals completed! 🐙C.2. Uniqueness of the solutions
Unlike the undamped oscillator, the mechanical energy is not conserved along a damped solution, so
uniqueness cannot be read off from a conserved positive-definite energy. Instead we reduce the
second-order equation of motion m ẍ + γ ẋ + k x = 0 to the first-order linear system
(x, ẋ)' = (ẋ, (1/m)(-k x - γ ẋ)) on the phase space and invoke the global
ODE-uniqueness theorem ODE_solution_unique_univ (the right-hand side is a continuous
linear map, hence Lipschitz).
The phase-space vector field of the damped oscillator, sending (x, ẋ) to
(ẋ, -(k/m) x - (γ/m) ẋ), as a continuous linear map on E × E.
private noncomputable def phaseVectorField :
EuclideanSpace ℝ (Fin 1) × EuclideanSpace ℝ (Fin 1) →L[ℝ]
EuclideanSpace ℝ (Fin 1) × EuclideanSpace ℝ (Fin 1) :=
(ContinuousLinearMap.snd ℝ (EuclideanSpace ℝ (Fin 1)) (EuclideanSpace ℝ (Fin 1))).prod
((-(S.m⁻¹ * S.k)) •
ContinuousLinearMap.fst ℝ (EuclideanSpace ℝ (Fin 1)) (EuclideanSpace ℝ (Fin 1)) +
(-(S.m⁻¹ * S.γ)) •
ContinuousLinearMap.snd ℝ (EuclideanSpace ℝ (Fin 1)) (EuclideanSpace ℝ (Fin 1)))private lemma phaseVectorField_apply (a b : EuclideanSpace ℝ (Fin 1)) :
S.phaseVectorField (a, b) = (b, (-(S.m⁻¹ * S.k)) • a + (-(S.m⁻¹ * S.γ)) • b) := S:DampedHarmonicOscillatora:EuclideanSpace ℝ (Fin 1)b:EuclideanSpace ℝ (Fin 1)⊢ S.phaseVectorField (a, b) = (b, -(S.m⁻¹ * S.k) • a + -(S.m⁻¹ * S.γ) • b)
All goals completed! 🐙All goals completed! 🐙
Bridge from the time derivative to HasDerivAt for a curve reparametrised through the
canonical ℝ ≃L[ℝ] Time equivalence.
private lemma hasDerivAt_comp_toRealCLE_symm (w : Time → EuclideanSpace ℝ (Fin 1)) (τ : ℝ)
(hw : DifferentiableAt ℝ w (Time.toRealCLE.symm τ)) :
HasDerivAt (fun τ : ℝ => w (Time.toRealCLE.symm τ))
(∂ₜ w (Time.toRealCLE.symm τ)) τ := w:Time → EuclideanSpace ℝ (Fin 1)τ:ℝhw:DifferentiableAt ℝ w (toRealCLE.symm τ)⊢ HasDerivAt (fun τ => w (toRealCLE.symm τ)) (∂ₜ w (toRealCLE.symm τ)) τ
All goals completed! 🐙
The phase curve τ ↦ (z t, ẋ t) (with t = toRealCLE.symm τ) of a smooth solution z
solves the first-order phase-space ODE with vector field phaseVectorField.
S:DampedHarmonicOscillatorz:Time → EuclideanSpace ℝ (Fin 1)hz:ContDiff ℝ ∞ zhEOM:S.EquationOfMotion zτ:ℝ⊢ HasDerivAt (fun τ => (z (toRealCLE.symm τ), ∂ₜ z (toRealCLE.symm τ)))
(∂ₜ z (toRealCLE.symm τ), ∂ₜ (∂ₜ z) (toRealCLE.symm τ)) τ
exact (hasDerivAt_comp_toRealCLE_symm z τ (hz.differentiable (S:DampedHarmonicOscillatorz:Time → EuclideanSpace ℝ (Fin 1)hz:ContDiff ℝ ∞ zhEOM:S.EquationOfMotion zτ:ℝ⊢ ∞ ≠ 0 All goals completed! 🐙) _)).prodMk
(hasDerivAt_comp_toRealCLE_symm (∂ₜ z) τ (deriv_differentiable_of_contDiff z hz _))Any two smooth solutions of the damped equation of motion with the same initial position and velocity are equal.
S:DampedHarmonicOscillatorx:Time → EuclideanSpace ℝ (Fin 1)y:Time → EuclideanSpace ℝ (Fin 1)hx:ContDiff ℝ ∞ xhy:ContDiff ℝ ∞ yhEOMx:S.EquationOfMotion xhEOMy:S.EquationOfMotion yh0:x 0 = y 0hv0:∂ₜ x 0 = ∂ₜ y 0hIC:(fun τ => (x (toRealCLE.symm τ), ∂ₜ x (toRealCLE.symm τ))) 0 =
(fun τ => (y (toRealCLE.symm τ), ∂ₜ y (toRealCLE.symm τ))) 0⊢ x = y
S:DampedHarmonicOscillatorx:Time → EuclideanSpace ℝ (Fin 1)y:Time → EuclideanSpace ℝ (Fin 1)hx:ContDiff ℝ ∞ xhy:ContDiff ℝ ∞ yhEOMx:S.EquationOfMotion xhEOMy:S.EquationOfMotion yh0:x 0 = y 0hv0:∂ₜ x 0 = ∂ₜ y 0hIC:(fun τ => (x (toRealCLE.symm τ), ∂ₜ x (toRealCLE.symm τ))) 0 =
(fun τ => (y (toRealCLE.symm τ), ∂ₜ y (toRealCLE.symm τ))) 0hEq:(fun τ => (x (toRealCLE.symm τ), ∂ₜ x (toRealCLE.symm τ))) = fun τ => (y (toRealCLE.symm τ), ∂ₜ y (toRealCLE.symm τ))⊢ x = y
S:DampedHarmonicOscillatorx:Time → EuclideanSpace ℝ (Fin 1)y:Time → EuclideanSpace ℝ (Fin 1)hx:ContDiff ℝ ∞ xhy:ContDiff ℝ ∞ yhEOMx:S.EquationOfMotion xhEOMy:S.EquationOfMotion yh0:x 0 = y 0hv0:∂ₜ x 0 = ∂ₜ y 0hIC:(fun τ => (x (toRealCLE.symm τ), ∂ₜ x (toRealCLE.symm τ))) 0 =
(fun τ => (y (toRealCLE.symm τ), ∂ₜ y (toRealCLE.symm τ))) 0hEq:(fun τ => (x (toRealCLE.symm τ), ∂ₜ x (toRealCLE.symm τ))) = fun τ => (y (toRealCLE.symm τ), ∂ₜ y (toRealCLE.symm τ))t:Time⊢ x t = y t
S:DampedHarmonicOscillatorx:Time → EuclideanSpace ℝ (Fin 1)y:Time → EuclideanSpace ℝ (Fin 1)hx:ContDiff ℝ ∞ xhy:ContDiff ℝ ∞ yhEOMx:S.EquationOfMotion xhEOMy:S.EquationOfMotion yh0:x 0 = y 0hv0:∂ₜ x 0 = ∂ₜ y 0hIC:(fun τ => (x (toRealCLE.symm τ), ∂ₜ x (toRealCLE.symm τ))) 0 =
(fun τ => (y (toRealCLE.symm τ), ∂ₜ y (toRealCLE.symm τ))) 0hEq:(fun τ => (x (toRealCLE.symm τ), ∂ₜ x (toRealCLE.symm τ))) = fun τ => (y (toRealCLE.symm τ), ∂ₜ y (toRealCLE.symm τ))t:Timeh1:(x (toRealCLE.symm (toRealCLE t)), ∂ₜ x (toRealCLE.symm (toRealCLE t))) =
(y (toRealCLE.symm (toRealCLE t)), ∂ₜ y (toRealCLE.symm (toRealCLE t)))⊢ x t = y t
S:DampedHarmonicOscillatorx:Time → EuclideanSpace ℝ (Fin 1)y:Time → EuclideanSpace ℝ (Fin 1)hx:ContDiff ℝ ∞ xhy:ContDiff ℝ ∞ yhEOMx:S.EquationOfMotion xhEOMy:S.EquationOfMotion yh0:x 0 = y 0hv0:∂ₜ x 0 = ∂ₜ y 0hIC:(fun τ => (x (toRealCLE.symm τ), ∂ₜ x (toRealCLE.symm τ))) 0 =
(fun τ => (y (toRealCLE.symm τ), ∂ₜ y (toRealCLE.symm τ))) 0hEq:(fun τ => (x (toRealCLE.symm τ), ∂ₜ x (toRealCLE.symm τ))) = fun τ => (y (toRealCLE.symm τ), ∂ₜ y (toRealCLE.symm τ))t:Timeh1:(x t, ∂ₜ x t) = (y t, ∂ₜ y t)⊢ x t = y t
All goals completed! 🐙The selected trajectory is the unique smooth solution of the damped equation of motion with the given initial conditions.
All goals completed! 🐙