From 17e4a82994f096922df25d180831c4e6a7215d83 Mon Sep 17 00:00:00 2001 From: JayYarlott <98546364+JayYarlott@users.noreply.github.com> Date: Wed, 25 Feb 2026 03:10:53 -0500 Subject: [PATCH 01/11] theorems for enery dissipation rates and lack of conservation of energy --- .../DampedHarmonicOscillator/Basic.lean | 53 +++++++++++++++++++ 1 file changed, 53 insertions(+) diff --git a/PhysLean/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean b/PhysLean/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean index 24c4a98df..8cb3ab50e 100644 --- a/PhysLean/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean +++ b/PhysLean/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean @@ -63,6 +63,8 @@ namespace ClassicalMechanics open Real open Space open InnerProductSpace +open ContDiff +open Time TODO "DHO01" "Define the DampedHarmonicOscillator structure with mass m, spring constant k, and damping coefficient γ." @@ -205,6 +207,57 @@ 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 + + +theorem 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 + -- Have our Equation of Motion + have heom := h1 t + -- Rearrange for substitution + have heom' : S.m * Time.deriv (Time.deriv x) t + S.k * x t = + - S.γ * Time.deriv x t := by linarith + -- Work with fderivs + rw [Time.deriv_eq] + + -- Nice to have for later + have hdx : Differentiable ℝ x := hx.differentiable (by norm_num) + have hddx : Differentiable ℝ (∂ₜ x) := deriv_differentiable_of_contDiff x hx + + -- Break equation apart + simp only [energy, kineticEnergy, potentialEnergy, Pi.add_def] + rw [← Pi.add_def] + + have hke : DifferentiableAt ℝ (fun i => (1/2 : ℝ) * S.m * ∂ₜ x i ^ 2) t := ((hddx t).pow 2).const_mul _ + have hpe : DifferentiableAt ℝ (fun i => 1 / 2 * S.k * x i ^ 2) t := ((hdx t).pow 2).const_mul _ + -- Separate energy derivative into potential and kinetic + rw [fderiv_add hke hpe] + -- Perform chain derivatives and move constants + rw [fderiv_const_mul (a := fun i => ∂ₜ x i ^ 2) ((hddx t).pow 2)] + rw [fderiv_const_mul (a := fun i => x i ^ 2) ((hdx t).pow 2)] + rw [fderiv_pow 2 (hddx t)] + rw [fderiv_pow 2 (hdx t)] + + norm_num + rw [← Time.deriv, ← Time.deriv] + linear_combination (Time.deriv x t) * heom' + +theorem 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 + have he : Time.deriv (energy S x) t = - S.γ * (Time.deriv x t)^2 := + energy_dissipation_rate S x h1 hx + rw [he] + + have hp : 0 < ∂ₜ x t ^ 2 := by + rw [sq_pos_iff] + exact hdx + + rw [neg_mul S.γ (∂ₜ x t ^ 2)] + exact neg_neg_of_pos (mul_pos hγ hp) + + /-! ## E. Damping regimes (placeholder) From 76a1d8923aa45a37a608b74021fac3b75f76ee48 Mon Sep 17 00:00:00 2001 From: JayYarlott <98546364+JayYarlott@users.noreply.github.com> Date: Mon, 2 Mar 2026 19:00:03 -0500 Subject: [PATCH 02/11] linting fixes --- .../DampedHarmonicOscillator/Basic.lean | 27 ++++++++++--------- 1 file changed, 14 insertions(+), 13 deletions(-) diff --git a/PhysLean/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean b/PhysLean/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean index 8cb3ab50e..c9b1c869b 100644 --- a/PhysLean/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean +++ b/PhysLean/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean @@ -207,29 +207,30 @@ 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 -/ theorem 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 + (hx : ContDiff ℝ ∞ x) : + Time.deriv (energy S x) t = - S.γ * (Time.deriv x t)^2 := by -- Have our Equation of Motion have heom := h1 t -- Rearrange for substitution have heom' : S.m * Time.deriv (Time.deriv x) t + S.k * x t = - - S.γ * Time.deriv x t := by linarith + - S.γ * Time.deriv x t := by linarith -- Work with fderivs rw [Time.deriv_eq] -- Nice to have for later - have hdx : Differentiable ℝ x := hx.differentiable (by norm_num) - have hddx : Differentiable ℝ (∂ₜ x) := deriv_differentiable_of_contDiff x hx + have hdx : Differentiable ℝ x := hx.differentiable (by norm_num) + have hddx : Differentiable ℝ (∂ₜ x) := deriv_differentiable_of_contDiff x hx -- Break equation apart simp only [energy, kineticEnergy, potentialEnergy, Pi.add_def] rw [← Pi.add_def] - have hke : DifferentiableAt ℝ (fun i => (1/2 : ℝ) * S.m * ∂ₜ x i ^ 2) t := ((hddx t).pow 2).const_mul _ - have hpe : DifferentiableAt ℝ (fun i => 1 / 2 * S.k * x i ^ 2) t := ((hdx t).pow 2).const_mul _ + have hke : DifferentiableAt ℝ (fun i => (1/2 : ℝ) * S.m * ∂ₜ x i ^ 2) t := + ((hddx t).pow 2).const_mul _ + have hpe : DifferentiableAt ℝ (fun i => 1 / 2 * S.k * x i ^ 2) t := + ((hdx t).pow 2).const_mul _ -- Separate energy derivative into potential and kinetic rw [fderiv_add hke hpe] -- Perform chain derivatives and move constants @@ -243,9 +244,10 @@ theorem energy_dissipation_rate (x: Time → ℝ) (h1 : S.EquationOfMotion x) linear_combination (Time.deriv x t) * heom' theorem 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 + (hx : ContDiff ℝ ∞ x) + (hdx : Time.deriv x t ≠ 0) + (hγ : S.γ > 0) : + Time.deriv (energy S x) t < 0 := by have he : Time.deriv (energy S x) t = - S.γ * (Time.deriv x t)^2 := energy_dissipation_rate S x h1 hx rw [he] @@ -257,7 +259,6 @@ theorem energy_not_conserved (x: Time → ℝ) (h1 : S.EquationOfMotion x) rw [neg_mul S.γ (∂ₜ x t ^ 2)] exact neg_neg_of_pos (mul_pos hγ hp) - /-! ## E. Damping regimes (placeholder) From 0f72746d02069ca99a73998159baf696a80ead51 Mon Sep 17 00:00:00 2001 From: JayYarlott <98546364+JayYarlott@users.noreply.github.com> Date: Mon, 2 Mar 2026 19:26:57 -0500 Subject: [PATCH 03/11] Clean up todos --- .../ClassicalMechanics/DampedHarmonicOscillator/Basic.lean | 5 ----- 1 file changed, 5 deletions(-) diff --git a/PhysLean/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean b/PhysLean/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean index c9b1c869b..91e35e815 100644 --- a/PhysLean/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean +++ b/PhysLean/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean @@ -66,11 +66,6 @@ open InnerProductSpace open ContDiff open Time -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." - TODO "DHO05" "Derive solutions for the underdamped case (oscillatory with exponential decay)." TODO "DHO06" "Derive solutions for the critically damped case (fastest non-oscillatory return)." From 84fae7522ef492b614e5aa0597955dfedbc2b2af Mon Sep 17 00:00:00 2001 From: JayYarlott <98546364+JayYarlott@users.noreply.github.com> Date: Mon, 2 Mar 2026 19:30:11 -0500 Subject: [PATCH 04/11] Clean up unused namespaces --- PhysLean/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/PhysLean/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean b/PhysLean/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean index 91e35e815..99b39dfab 100644 --- a/PhysLean/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean +++ b/PhysLean/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean @@ -61,8 +61,6 @@ References for the damped harmonic oscillator include: namespace ClassicalMechanics open Real -open Space -open InnerProductSpace open ContDiff open Time From bf4e588a8bee3290f1c772c149177d6522e076df Mon Sep 17 00:00:00 2001 From: JayYarlott <98546364+JayYarlott@users.noreply.github.com> Date: Tue, 3 Mar 2026 01:26:05 -0500 Subject: [PATCH 05/11] replace `theorem` with `lemma` --- .../ClassicalMechanics/DampedHarmonicOscillator/Basic.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/PhysLean/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean b/PhysLean/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean index 99b39dfab..ed513affc 100644 --- a/PhysLean/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean +++ b/PhysLean/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean @@ -201,7 +201,7 @@ noncomputable def energyDissipationRate (x : Time → ℝ) : Time → ℝ := fun t => - S.γ * (Time.deriv x t)^2 /-- Derives the energy dissipation rate from the equation of motion -/ -theorem energy_dissipation_rate (x: Time → ℝ) (h1 : S.EquationOfMotion x) +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 -- Have our Equation of Motion @@ -236,7 +236,7 @@ theorem energy_dissipation_rate (x: Time → ℝ) (h1 : S.EquationOfMotion x) rw [← Time.deriv, ← Time.deriv] linear_combination (Time.deriv x t) * heom' -theorem energy_not_conserved (x: Time → ℝ) (h1 : S.EquationOfMotion x) +lemma energy_not_conserved (x: Time → ℝ) (h1 : S.EquationOfMotion x) (hx : ContDiff ℝ ∞ x) (hdx : Time.deriv x t ≠ 0) (hγ : S.γ > 0) : From 956245f6482ae202308d3d27111b354ec77b0e83 Mon Sep 17 00:00:00 2001 From: JayYarlott <98546364+JayYarlott@users.noreply.github.com> Date: Tue, 3 Mar 2026 01:27:47 -0500 Subject: [PATCH 06/11] Clearer unfolding of energy defs --- .../ClassicalMechanics/DampedHarmonicOscillator/Basic.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/PhysLean/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean b/PhysLean/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean index ed513affc..95e2645df 100644 --- a/PhysLean/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean +++ b/PhysLean/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean @@ -217,8 +217,8 @@ lemma energy_dissipation_rate (x: Time → ℝ) (h1 : S.EquationOfMotion x) have hddx : Differentiable ℝ (∂ₜ x) := deriv_differentiable_of_contDiff x hx -- Break equation apart - simp only [energy, kineticEnergy, potentialEnergy, Pi.add_def] - rw [← Pi.add_def] + rw [energy] + unfold kineticEnergy potentialEnergy have hke : DifferentiableAt ℝ (fun i => (1/2 : ℝ) * S.m * ∂ₜ x i ^ 2) t := ((hddx t).pow 2).const_mul _ From f343468512366a93cf3bb7a460daba9ded9bd67f Mon Sep 17 00:00:00 2001 From: JayYarlott <98546364+JayYarlott@users.noreply.github.com> Date: Tue, 3 Mar 2026 01:29:00 -0500 Subject: [PATCH 07/11] Fold fderiv_add continuity hypotheses into rewrite --- .../DampedHarmonicOscillator/Basic.lean | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/PhysLean/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean b/PhysLean/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean index 95e2645df..af24958ee 100644 --- a/PhysLean/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean +++ b/PhysLean/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean @@ -220,12 +220,10 @@ lemma energy_dissipation_rate (x: Time → ℝ) (h1 : S.EquationOfMotion x) rw [energy] unfold kineticEnergy potentialEnergy - have hke : DifferentiableAt ℝ (fun i => (1/2 : ℝ) * S.m * ∂ₜ x i ^ 2) t := - ((hddx t).pow 2).const_mul _ - have hpe : DifferentiableAt ℝ (fun i => 1 / 2 * S.k * x i ^ 2) t := - ((hdx t).pow 2).const_mul _ -- Separate energy derivative into potential and kinetic - rw [fderiv_add hke hpe] + rw [fderiv_add (f := fun i => (1/2 : ℝ) * S.m * ∂ₜ x i ^ 2) + (g := fun i => (1/2 : ℝ) * S.k * x i ^ 2) + (((hddx t).pow 2).const_mul _) (((hdx t).pow 2).const_mul _)] -- Perform chain derivatives and move constants rw [fderiv_const_mul (a := fun i => ∂ₜ x i ^ 2) ((hddx t).pow 2)] rw [fderiv_const_mul (a := fun i => x i ^ 2) ((hdx t).pow 2)] From 31158d4138ca401a48651c9a519216f2dc2e47ca Mon Sep 17 00:00:00 2001 From: JayYarlott <98546364+JayYarlott@users.noreply.github.com> Date: Tue, 3 Mar 2026 01:34:22 -0500 Subject: [PATCH 08/11] Combine simpler rewrites --- .../DampedHarmonicOscillator/Basic.lean | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/PhysLean/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean b/PhysLean/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean index af24958ee..599402733 100644 --- a/PhysLean/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean +++ b/PhysLean/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean @@ -220,15 +220,14 @@ lemma energy_dissipation_rate (x: Time → ℝ) (h1 : S.EquationOfMotion x) rw [energy] unfold kineticEnergy potentialEnergy - -- Separate energy derivative into potential and kinetic + -- Break additive terms out of derivative rw [fderiv_add (f := fun i => (1/2 : ℝ) * S.m * ∂ₜ x i ^ 2) (g := fun i => (1/2 : ℝ) * S.k * x i ^ 2) (((hddx t).pow 2).const_mul _) (((hdx t).pow 2).const_mul _)] - -- Perform chain derivatives and move constants - rw [fderiv_const_mul (a := fun i => ∂ₜ x i ^ 2) ((hddx t).pow 2)] - rw [fderiv_const_mul (a := fun i => x i ^ 2) ((hdx t).pow 2)] - rw [fderiv_pow 2 (hddx t)] - rw [fderiv_pow 2 (hdx t)] + -- Perform the derivative + rw [fderiv_const_mul (a := fun i => ∂ₜ x i ^ 2) ((hddx t).pow 2), + fderiv_const_mul (a := fun i => x i ^ 2) ((hdx t).pow 2), + fderiv_pow 2 (hddx t), fderiv_pow 2 (hdx t)] norm_num rw [← Time.deriv, ← Time.deriv] From eeaaaaf257b4e62d2fa878262eff93cd591cd56e Mon Sep 17 00:00:00 2001 From: JayYarlott <98546364+JayYarlott@users.noreply.github.com> Date: Tue, 3 Mar 2026 01:36:49 -0500 Subject: [PATCH 09/11] Condense energy_not_conserved --- .../DampedHarmonicOscillator/Basic.lean | 10 ++-------- 1 file changed, 2 insertions(+), 8 deletions(-) diff --git a/PhysLean/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean b/PhysLean/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean index 599402733..6fcf95aca 100644 --- a/PhysLean/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean +++ b/PhysLean/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean @@ -238,16 +238,10 @@ lemma energy_not_conserved (x: Time → ℝ) (h1 : S.EquationOfMotion x) (hdx : Time.deriv x t ≠ 0) (hγ : S.γ > 0) : Time.deriv (energy S x) t < 0 := by - have he : Time.deriv (energy S x) t = - S.γ * (Time.deriv x t)^2 := - energy_dissipation_rate S x h1 hx - rw [he] - - have hp : 0 < ∂ₜ x t ^ 2 := by - rw [sq_pos_iff] - exact hdx + rw [energy_dissipation_rate S x h1 hx] rw [neg_mul S.γ (∂ₜ x t ^ 2)] - exact neg_neg_of_pos (mul_pos hγ hp) + refine neg_neg_of_pos (mul_pos hγ (sq_pos_iff.mpr hdx)) /-! From cadc96cf0e01a37b7412e93e13f8e61495007965 Mon Sep 17 00:00:00 2001 From: JayYarlott <98546364+JayYarlott@users.noreply.github.com> Date: Tue, 3 Mar 2026 02:51:14 -0500 Subject: [PATCH 10/11] remove fderiv rewrites --- .../DampedHarmonicOscillator/Basic.lean | 13 ++++--------- 1 file changed, 4 insertions(+), 9 deletions(-) diff --git a/PhysLean/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean b/PhysLean/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean index 6fcf95aca..efd3988e3 100644 --- a/PhysLean/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean +++ b/PhysLean/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean @@ -212,7 +212,6 @@ lemma energy_dissipation_rate (x: Time → ℝ) (h1 : S.EquationOfMotion x) -- Work with fderivs rw [Time.deriv_eq] - -- Nice to have for later have hdx : Differentiable ℝ x := hx.differentiable (by norm_num) have hddx : Differentiable ℝ (∂ₜ x) := deriv_differentiable_of_contDiff x hx @@ -220,14 +219,10 @@ lemma energy_dissipation_rate (x: Time → ℝ) (h1 : S.EquationOfMotion x) rw [energy] unfold kineticEnergy potentialEnergy - -- Break additive terms out of derivative - rw [fderiv_add (f := fun i => (1/2 : ℝ) * S.m * ∂ₜ x i ^ 2) - (g := fun i => (1/2 : ℝ) * S.k * x i ^ 2) - (((hddx t).pow 2).const_mul _) (((hdx t).pow 2).const_mul _)] - -- Perform the derivative - rw [fderiv_const_mul (a := fun i => ∂ₜ x i ^ 2) ((hddx t).pow 2), - fderiv_const_mul (a := fun i => x i ^ 2) ((hdx t).pow 2), - fderiv_pow 2 (hddx t), fderiv_pow 2 (hdx t)] + 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] From c2ce03d59f17fb3dd4d7d7aad252efd808663aff Mon Sep 17 00:00:00 2001 From: JayYarlott <98546364+JayYarlott@users.noreply.github.com> Date: Tue, 3 Mar 2026 03:00:18 -0500 Subject: [PATCH 11/11] move statements around --- .../DampedHarmonicOscillator/Basic.lean | 16 +++++++--------- 1 file changed, 7 insertions(+), 9 deletions(-) diff --git a/PhysLean/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean b/PhysLean/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean index efd3988e3..33c78fb39 100644 --- a/PhysLean/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean +++ b/PhysLean/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean @@ -204,21 +204,19 @@ noncomputable def energyDissipationRate (x : Time → ℝ) : Time → ℝ := 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 - -- Have our Equation of Motion - have heom := h1 t - -- Rearrange for substitution - have heom' : S.m * Time.deriv (Time.deriv x) t + S.k * x t = - - S.γ * Time.deriv x t := by linarith - -- Work with fderivs - rw [Time.deriv_eq] - have hdx : Differentiable ℝ x := hx.differentiable (by norm_num) - have hddx : Differentiable ℝ (∂ₜ x) := deriv_differentiable_of_contDiff x hx + -- 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)