Revision #2380 → #3033 · back to history
modifiedEllipse in polar form7fcef9838324
| Field | From #2380 | To #3033 |
|---|
| note | No definition of an ellipse exists in Mathlib (only convex 'cones' and elliptic curves, neither relevant). | No definition of an ellipse exists in Mathlib (grep for Ellipse returns nothing). |
modifiedEccentricity as coefficient of variation2f3bf1a4b644
| Field | From #2380 | To #3033 |
|---|
| note | No ellipse eccentricity defined; the only 'eccentricity' in Mathlib is graph-theoretic. | No ellipse eccentricity defined; the only 'eccentricity' in Mathlib is graph-theoretic (SimpleGraph/Diam.lean). |
modifiedSecond law from conservation of angular momentum84dfc10400a9
| Field | From #2380 | To #3033 |
|---|
| note | No angular momentum or central-force dynamics formalized in Mathlib. | No angular momentum or central-force dynamics formalized in Mathlib (grep for AngularMomentum/CentralForce returns nothing). |
modifiedThird law derivation from Newton's gravitation (circular case)6e1f8e493bbe
| Field | From #2380 | To #3033 |
|---|
| note | No gravitational/centripetal-force calculus in Mathlib. | No gravitational/centripetal-force calculus in Mathlib (grep for Gravitat returns nothing). |
addedEllipse eccentricity via linear eccentricity and semi-major axiseea31c059acb
addedSecond law is a consequence of the radial nature of the force7508cc62ece9
addedRunge–Lenz O(4) symmetry of the Kepler problembb6026cc67c9
addedAreal velocity equals half the angular momentum per unit mass9f03cd924a55
addedRadial force produces no torque, so angular momentum is conserved77b6b9cad843
addedKepler's third law from equal areas and ellipse area πab167210c4dfa0
addedMean motion n = 2π/P674d075bbdbf
addedSector-area relation between ellipse and auxiliary circle292bfcc9fbd1
addedCartesian coordinates from the eccentric anomaly50354e410f6f
addedHalf-angle tangent identity for true anomaly40cd312af5be