Classical Harmonic Oscillator

Stream: PhysLean

[Lode Vermeulen]

I have been looking at trying to use the new variational calculus API on the harmonic oscillator (like we discussed here - I think it makes sense to give this potential its own topic). I have been trying to formalize the EquationOfMotion definition like the following:

noncomputable def EquationOfMotion (xₜ : Time → Space 1) : Prop :=
  ∀ t, (eulerLagrangeOp (lagrangian S) xₜ) t = 0

But this does not quite work due to

Application type mismatch: In the application
  eulerLagrangeOp S.lagrangian
the argument
  S.lagrangian
has type
  (Time → Space 1) → Time → ℝ : Type
but is expected to have type
  Time → Space 1 → Space 1 → ℝ : Type

Which makes sense. I have been able to write it like

noncomputable def lagrangian' : Time → Space 1 → Space 1 → ℝ :=
  fun (t : Time) (q : Space 1) (q_dot : Space 1) =>
    (1 / (2 : ℝ)) * S.m * ⟪q_dot, q_dot⟫_ℝ - (1 / (2 : ℝ)) * S.k * ⟪q, q⟫_ℝ

noncomputable def EquationOfMotion' (xₜ : Time → Space 1) : Prop :=
  ∀ t, (eulerLagrangeOp (lagrangian' S) xₜ) t = 0

Which I expect we can turn the former into somehow, I'm just not sure how. Does anyone have any ideas?

[Joseph Tooby-Smith]

One approach might be to consider lagrangian' as the fundamental object, and derive lagrangian from that. I think it is true that there are various mathematical formulations of classical mechanics in which this is the correct direction (e.g. the jet bundle approach), but I can't speak for every formulation.

[Joseph Tooby-Smith]

(Huh, so I think it would be good to move the relevant messages from that thread to this one - but I don't get the option for these specific messages, I do for others :().

[Joseph Tooby-Smith]

I made an implementation of this (that is setting up and solving the variational calculus problem) here: PhysLean#737 - getting rid of some sorryful results but creating others.

[Lode Vermeulen]

Nice! That actually doesn't look too bad

[Joseph Tooby-Smith]

Ideally I think the amplitude etc. should be done in the way @ZhiKai Pong suggests here: #PhysLean > Mini projects @ 💬, but didn't get round to doing that - hence the sorryful results.

[Joseph Tooby-Smith]

I updated this PR with some Hamilton mechanics. I also massively restructured the file and added a lot more documentation. I created this issue PhysLean#738 regarding the docs, where there is also a pdf which shows them as they would appear on the website.

[Jard]

I am working on the proof for trajectory_velocity_eq_zero_iff; I got quite far quite fast (I just have some annoying arithmetic to do), so I expect to be able to file a pull request by probably Monday at the latest.

[Joseph Tooby-Smith]

Awesome! This sounds great @Jard :).

[Jard]

I actually just managed to finish the proof! I'm getting ready to merge it, however I did notice that there was an assumption in the problem statement that not both initial conditions could be 0, and this assumption went unused. It would be an extremely boring harmonic oscillator, but it would be one nonetheless. Can I remove the assumption or should I leave it in?

[Joseph Tooby-Smith]

Nice! Do you mean the assumption, (hx : IC.x₀ ≠ 0 ∨ IC.v₀ ≠ 0)? If you didn't use this, this is great, and yes it can be removed :)! I only included it as I couldn't see a way to prove this without it

[Jard]

Yes, that's the one I mean! I ended up proving it through energy conservation

[Joseph Tooby-Smith]

Cool, this makes sense! I think there is then a similar lemma one could prove in a similar way - that is, one could find the speed of the particle as it passes through zero.

[Jard]

I have my thesis deadline soon, but I'll have a look after! It's been so much fun, I definitely plan to continue with lean4 after my thesis.

If I did it correctly (it's my first time), I just made the pull request

[Joseph Tooby-Smith]

Good luck with your thesis! I made a comment there regarding linters, but I am more than happy to take care of this - just let me know :).

[Jard]

Thanks! I got it; am working on the linters now