Initial Commit for Orbital Mechanics

[hannxmarie]

Added vis viva for circular orbit. If I need to put this elsewhere in the file structure please let me know, happy to move. This is first attempt at lean so welcome to feedback - thanks!

[zhikaip]

Welcome! Would you mind changing the title to something more informative? (e.g feat: initial commit for orbital mechanics) (we attempt to follow Mathlib conventions https://leanprover-community.github.io/contribute/commit.html)

I don't think this should sit inside the Lagrangian folder, and probably deserves it's own folder under classical mechanics (will be worth thinking about how you want to build around it). I don't know the physics well enough and @winstonyin can probably comment on this. (Might also want a more specific namespace.)

Finally, I feel like the adjective circular might work better than circle

[hannxmarie]

Thanks for sending, I'll format in that way for any new requests. I'm planning to add some more of the 2 body orbital mechanics equations. Happy to add an Orbital Mechanics folder and rename this file to TwoBody.lean?

[jstoobysmith]

Hi Hannah, nice to see this PR! I think an orbital mechanics folder sounds good. I don't think this is quite TwoBody though, in the sense that you are assuming that one of the bodies is massive and are only considering the motion of the other. Maybe there is a better file name we could use.

[hannxmarie]

Thanks for the feedback! I've added an orbital mechanics folder and named my file visviva for now. Also made a couple edits which means it should ideally pass the workflow now.

[jstoobysmith]

Hi Hannah,

I think there are a couple more changes which could be made here to make things better (again these are all really design choices0:

1. I would define a structure VisViva or something else, which contains the input data: G, M and m (eventually surly you need the mass of both bodies).

2. I would then define a configuration space VisViva.ConfigurationSpace which contains a single field r, which can be in Real or EuclideanSpace Real (Fin 3) or something similar.

3. I would then rename vis_viva_circular to something like speedCircular (no underscores in definition names) and vis_viva_circular_sq to something like speedCircular_sq