Prove energy dissipation rate for damped harmonic oscillator#967
Conversation
jstoobysmith
left a comment
jstoobysmith
left a comment
There was a problem hiding this comment.
I've added some review comments - I was a bit pedantic, but hopefully they are useful
PhysLean/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean
Outdated
Show resolved
Hide resolved
PhysLean/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean
Outdated
Show resolved
Hide resolved
PhysLean/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean
Outdated
Show resolved
Hide resolved
PhysLean/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean
Outdated
Show resolved
Hide resolved
PhysLean/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean
Outdated
Show resolved
Hide resolved
PhysLean/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean
Outdated
Show resolved
Hide resolved
jstoobysmith
added
t-classical-mechanics
jstoobysmith
left a comment
jstoobysmith
left a comment
There was a problem hiding this comment.
Many thanks, two more quick comments.
| - S.γ * Time.deriv x t := by linarith [h1 t] | ||
|
|
||
| -- Break equation apart | ||
| rw [energy] |
There was a problem hiding this comment.
rw [energy, kineticEnergy, potentialEnergy]?
If this doesn't work then we should likely have theorems kineticEnergy_eq and potentialEnergy_eq which experts the definitional equality of kineticEnergy and potentialEnergy. Using unfold is generally not the best idea, although I acknowledge that it is used throughout this project.
| have hPE := ((hdx t).hasFDerivAt.pow 2).const_mul (1/2 * S.k) | ||
|
|
||
| rw [(hKE.add hPE).fderiv] | ||
|
|
There was a problem hiding this comment.
Could we remove these extra new lines in the proof?
jstoobysmith
left a comment
jstoobysmith
left a comment
There was a problem hiding this comment.
Added a couple more suggested changes, you should just be able to apply these directly. Some are necessary for the linters. This should hopefully be the last round.
PhysLean/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean
Outdated
Show resolved
Hide resolved
PhysLean/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean
Outdated
Show resolved
Hide resolved
PhysLean/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean
Outdated
Show resolved
Hide resolved
PhysLean/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean
Outdated
Show resolved
Hide resolved
Co-authored-by: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com>
Co-authored-by: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com>
Co-authored-by: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com>
Co-authored-by: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com>
jstoobysmith
left a comment
jstoobysmith
left a comment
There was a problem hiding this comment.
Many thanks for this, I've approved and I will merge now.
jstoobysmith
added
ready-to-merge
2 participants
Builds on #891 by adding proofs of the energy dissipation rate for a damped harmonic oscillator.