Prove energy dissipation rate for damped harmonic oscillator

PhysLean/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean

@@ -61,13 +61,8 @@ References for the damped harmonic oscillator include:
 
 namespace ClassicalMechanics
 open Real
-open Space
-open InnerProductSpace
-
-TODO "DHO01" "Define the DampedHarmonicOscillator structure with mass m, spring constant k,
-  and damping coefficient γ."
-
-TODO "DHO04" "Prove that energy is not conserved and derive the energy dissipation rate."
+open ContDiff
+open Time
 
 TODO "DHO05" "Derive solutions for the underdamped case (oscillatory with exponential decay)."
 
@@ -205,6 +200,42 @@ so the energy is non-increasing and not conserved when `S.γ > 0`. -/
 noncomputable def energyDissipationRate (x : Time → ℝ) : Time → ℝ :=
   fun t => - S.γ * (Time.deriv x t)^2
 
+/-- Derives the energy dissipation rate from the equation of motion -/
+lemma energy_dissipation_rate (x: Time → ℝ) (h1 : S.EquationOfMotion x)
+    (hx : ContDiff ℝ ∞ x) :
+    Time.deriv (energy S x) t = - S.γ * (Time.deriv x t)^2 := by
+
+  -- Rearrange Equation of Motion
+  have heom' : S.m * Time.deriv (Time.deriv x) t + S.k * x t =
+              - S.γ * Time.deriv x t := by linarith [h1 t]
+
+  -- Break equation apart
+  rw [energy]
+  unfold kineticEnergy potentialEnergy
+
+  rw [Time.deriv_eq]
+
+  have hdx : Differentiable ℝ x := hx.differentiable (by norm_num)
+  have hddx : Differentiable ℝ (∂ₜ x) := deriv_differentiable_of_contDiff x hx
+  have hKE := ((hddx t).hasFDerivAt.pow 2).const_mul (1/2 * S.m)
+  have hPE := ((hdx t).hasFDerivAt.pow 2).const_mul (1/2 * S.k)
+
+  rw [(hKE.add hPE).fderiv]
+
+  norm_num
+  rw [← Time.deriv, ← Time.deriv]
+  linear_combination (Time.deriv x t) * heom'
+
+lemma energy_not_conserved (x: Time → ℝ) (h1 : S.EquationOfMotion x)
+    (hx : ContDiff ℝ ∞ x)
+    (hdx : Time.deriv x t ≠ 0)
+    (hγ : S.γ > 0) :
+    Time.deriv (energy S x) t < 0 := by
+
+  rw [energy_dissipation_rate S x h1 hx]
+  rw [neg_mul S.γ (∂ₜ x t ^ 2)]
+  refine neg_neg_of_pos (mul_pos hγ (sq_pos_iff.mpr hdx))
+
 /-!
 
 ## E. Damping regimes (placeholder)