Prove energy dissipation rate for damped harmonic oscillator#967
Prove energy dissipation rate for damped harmonic oscillator#967JayYarlott wants to merge 11 commits intoleanprover-community:masterfrom
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
| have hddx : Differentiable ℝ (∂ₜ x) := deriv_differentiable_of_contDiff x hx | ||
|
|
||
| -- Break equation apart | ||
| simp only [energy, kineticEnergy, potentialEnergy, Pi.add_def] |
There was a problem hiding this comment.
If you remove Pi.add_def from the simp only do you need it in the rw below?
There was a problem hiding this comment.
The Pi.add_def was being used chronologically between energy and the kineticEnergy because simp only was having a hard time unfolding kineticEnergy and potentialEnergy without it. I cleaned it up a bit in 956245f, just using unfold and rw [energy]
| -- 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)] |
| 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] |
There was a problem hiding this comment.
I think you should be able to replace this have he ... followed by rw with just
rw [energy_dissipation_rate]
| exact hdx | ||
|
|
||
| rw [neg_mul S.γ (∂ₜ x t ^ 2)] | ||
| exact neg_neg_of_pos (mul_pos hγ hp) |
There was a problem hiding this comment.
This might be cleaner as
rw [neg_mul S.γ (∂ₜ x t ^ 2)]
refine neg_neg_of_pos (mul_pos hγ ?_)
rw [sq_pos_iff]
exact hdxor even, if it works,
rw [neg_mul S.γ (∂ₜ x t ^ 2)]
refine neg_neg_of_pos (mul_pos hγ (sq_pos_iff.mp hdx))| 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] |
There was a problem hiding this comment.
You could probably put the have hke and have hpe directly in the rw, so something like
rw [fderiv_add (((hddx t).pow 2).const_mul _) (((hddx t).pow 2).const_mul _)]| 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) |
There was a problem hiding this comment.
Could we use lemma here instead of theorem.
There was a problem hiding this comment.
(and also in the other theorem)
There was a problem hiding this comment.
Absolutely, I'd meant to do that before issuing the pull request.
jstoobysmith
added
t-classical-mechanics
2 participants
Builds on #891 by adding proofs of the energy dissipation rate for a damped harmonic oscillator.