Elliptic Kepler orbits in eccentric anomaly

This file gives the real elliptic Kepler orbit attached to Delaunay action I₁ and eccentricity e. It verifies the radius, radial momentum, and energy formulas directly. The mean anomaly is the first Delaunay angle along the unperturbed flow.

noncomputable def LeanPool.PoincareThreeBody.eccentricRadius (firstAction eccentricity anomaly : ℝ) : ℝ

Radius of an elliptic Kepler orbit as a function of eccentric anomaly.

Equations

• LeanPool.PoincareThreeBody.eccentricRadius firstAction eccentricity anomaly = firstAction ^ 2 * (1 - eccentricity * Real.cos anomaly)

noncomputable def LeanPool.PoincareThreeBody.eccentricRadialMomentum (firstAction eccentricity anomaly : ℝ) : ℝ

Radial momentum of an elliptic Kepler orbit as a function of eccentric anomaly.

Equations

• LeanPool.PoincareThreeBody.eccentricRadialMomentum firstAction eccentricity anomaly = eccentricity * Real.sin anomaly / (firstAction * (1 - eccentricity * Real.cos anomaly))

noncomputable def LeanPool.PoincareThreeBody.eccentricMeanAnomaly (eccentricity anomaly : ℝ) : ℝ

Mean anomaly as a function of eccentric anomaly (Kepler's equation).

Equations

• LeanPool.PoincareThreeBody.eccentricMeanAnomaly eccentricity anomaly = anomaly - eccentricity * Real.sin anomaly

noncomputable def LeanPool.PoincareThreeBody.eccentricKeplerTime (firstAction eccentricity anomaly : ℝ) : ℝ

Physical Kepler time, normalized to vanish with the mean anomaly.

Equations

• LeanPool.PoincareThreeBody.eccentricKeplerTime firstAction eccentricity anomaly = firstAction ^ 3 * LeanPool.PoincareThreeBody.eccentricMeanAnomaly eccentricity anomaly

noncomputable def LeanPool.PoincareThreeBody.eccentricPolarState (firstAction eccentricity anomaly polarAngle : ℝ) : PolarState

A polar phase-space point on the elliptic Kepler orbit. Its angular coordinate is free because the inertial Kepler energy is rotation invariant.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanPool.PoincareThreeBody.one_sub_eccentricity_mul_cos_pos {eccentricity anomaly : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) : 0 < 1 - eccentricity * Real.cos anomaly

theorem LeanPool.PoincareThreeBody.eccentricRadius_pos {firstAction eccentricity anomaly : ℝ} (hfirstAction : firstAction ≠ 0) (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) : 0 < eccentricRadius firstAction eccentricity anomaly

theorem LeanPool.PoincareThreeBody.eccentricRadius_le_apoapsis_bound {firstAction eccentricity anomaly : ℝ} (heccentricity : 0 ≤ eccentricity) : eccentricRadius firstAction eccentricity anomaly ≤ firstAction ^ 2 * (1 + eccentricity)

theorem LeanPool.PoincareThreeBody.hasDerivAt_eccentricMeanAnomaly (eccentricity anomaly : ℝ) : HasDerivAt (eccentricMeanAnomaly eccentricity) (1 - eccentricity * Real.cos anomaly) anomaly

theorem LeanPool.PoincareThreeBody.hasDerivAt_eccentricRadius (firstAction eccentricity anomaly : ℝ) : HasDerivAt (eccentricRadius firstAction eccentricity) (firstAction ^ 2 * eccentricity * Real.sin anomaly) anomaly

theorem LeanPool.PoincareThreeBody.hasDerivAt_eccentricKeplerTime (firstAction eccentricity anomaly : ℝ) : HasDerivAt (eccentricKeplerTime firstAction eccentricity) (firstAction ^ 3 * (1 - eccentricity * Real.cos anomaly)) anomaly

theorem LeanPool.PoincareThreeBody.eccentricRadialMomentum_eq_radiusDeriv_div_timeDeriv {firstAction eccentricity anomaly : ℝ} (hfirstAction : firstAction ≠ 0) (hdenominator : 1 - eccentricity * Real.cos anomaly ≠ 0) : eccentricRadialMomentum firstAction eccentricity anomaly = firstAction ^ 2 * eccentricity * Real.sin anomaly / (firstAction ^ 3 * (1 - eccentricity * Real.cos anomaly))

The radial momentum is dr/dt along the eccentric-anomaly parameterization.

theorem LeanPool.PoincareThreeBody.strictMono_eccentricMeanAnomaly {eccentricity : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) : StrictMono (eccentricMeanAnomaly eccentricity)

theorem LeanPool.PoincareThreeBody.eccentricMeanAnomaly_add_two_pi (eccentricity anomaly : ℝ) : eccentricMeanAnomaly eccentricity (anomaly + 2 * Real.pi) = eccentricMeanAnomaly eccentricity anomaly + 2 * Real.pi

theorem LeanPool.PoincareThreeBody.eccentricMeanAnomaly_add_nat_mul_two_pi (eccentricity anomaly : ℝ) (turns : ℕ) : eccentricMeanAnomaly eccentricity (anomaly + ↑turns * (2 * Real.pi)) = eccentricMeanAnomaly eccentricity anomaly + ↑turns * (2 * Real.pi)

theorem LeanPool.PoincareThreeBody.eccentricMeanAnomaly_lower_bound {eccentricity anomaly : ℝ} (heccentricity : 0 ≤ eccentricity) : anomaly - eccentricity ≤ eccentricMeanAnomaly eccentricity anomaly

theorem LeanPool.PoincareThreeBody.eccentricMeanAnomaly_upper_bound {eccentricity anomaly : ℝ} (heccentricity : 0 ≤ eccentricity) : eccentricMeanAnomaly eccentricity anomaly ≤ anomaly + eccentricity

theorem LeanPool.PoincareThreeBody.continuous_eccentricMeanAnomaly (eccentricity : ℝ) : Continuous (eccentricMeanAnomaly eccentricity)

theorem LeanPool.PoincareThreeBody.analyticAt_eccentricMeanAnomaly (eccentricity anomaly : ℝ) : AnalyticAt ℝ (eccentricMeanAnomaly eccentricity) anomaly

theorem LeanPool.PoincareThreeBody.surjective_eccentricMeanAnomaly {eccentricity : ℝ} (heccentricity : 0 ≤ eccentricity) : Function.Surjective (eccentricMeanAnomaly eccentricity)

theorem LeanPool.PoincareThreeBody.bijective_eccentricMeanAnomaly {eccentricity : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) : Function.Bijective (eccentricMeanAnomaly eccentricity)

noncomputable def LeanPool.PoincareThreeBody.eccentricAnomaly (eccentricity meanAnomaly : ℝ) : ℝ

The unique eccentric anomaly solving Kepler's equation for a given mean anomaly.

Equations

• LeanPool.PoincareThreeBody.eccentricAnomaly eccentricity meanAnomaly = Function.invFun (LeanPool.PoincareThreeBody.eccentricMeanAnomaly eccentricity) meanAnomaly

theorem LeanPool.PoincareThreeBody.eccentricMeanAnomaly_eccentricAnomaly {eccentricity : ℝ} (heccentricity : 0 ≤ eccentricity) (meanAnomaly : ℝ) : eccentricMeanAnomaly eccentricity (eccentricAnomaly eccentricity meanAnomaly) = meanAnomaly

theorem LeanPool.PoincareThreeBody.eccentricAnomaly_eccentricMeanAnomaly {eccentricity : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) (anomaly : ℝ) : eccentricAnomaly eccentricity (eccentricMeanAnomaly eccentricity anomaly) = anomaly

theorem LeanPool.PoincareThreeBody.eccentricAnomaly_add_two_pi {eccentricity meanAnomaly : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) : eccentricAnomaly eccentricity (meanAnomaly + 2 * Real.pi) = eccentricAnomaly eccentricity meanAnomaly + 2 * Real.pi

theorem LeanPool.PoincareThreeBody.eccentricAnomaly_add_nat_mul_two_pi {eccentricity meanAnomaly : ℝ} (turns : ℕ) (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) : eccentricAnomaly eccentricity (meanAnomaly + ↑turns * (2 * Real.pi)) = eccentricAnomaly eccentricity meanAnomaly + ↑turns * (2 * Real.pi)

theorem LeanPool.PoincareThreeBody.continuous_eccentricAnomaly {eccentricity : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) : Continuous (eccentricAnomaly eccentricity)

theorem LeanPool.PoincareThreeBody.hasDerivAt_eccentricAnomaly {eccentricity meanAnomaly : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) : HasDerivAt (eccentricAnomaly eccentricity) (1 / (1 - eccentricity * Real.cos (eccentricAnomaly eccentricity meanAnomaly))) meanAnomaly

theorem LeanPool.PoincareThreeBody.analyticAt_eccentricAnomaly {eccentricity meanAnomaly : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) : AnalyticAt ℝ (eccentricAnomaly eccentricity) meanAnomaly

noncomputable def LeanPool.PoincareThreeBody.delaunayRadius (firstAction eccentricity meanAnomaly : ℝ) : ℝ

Radius expressed as a function of the first Delaunay angle.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanPool.PoincareThreeBody.delaunayRadius_pos {firstAction eccentricity meanAnomaly : ℝ} (hfirstAction : firstAction ≠ 0) (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) : 0 < delaunayRadius firstAction eccentricity meanAnomaly

theorem LeanPool.PoincareThreeBody.delaunayRadius_add_two_pi {firstAction eccentricity meanAnomaly : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) : delaunayRadius firstAction eccentricity (meanAnomaly + 2 * Real.pi) = delaunayRadius firstAction eccentricity meanAnomaly

theorem LeanPool.PoincareThreeBody.delaunayRadius_add_nat_mul_two_pi {firstAction eccentricity meanAnomaly : ℝ} (turns : ℕ) (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) : delaunayRadius firstAction eccentricity (meanAnomaly + ↑turns * (2 * Real.pi)) = delaunayRadius firstAction eccentricity meanAnomaly

theorem LeanPool.PoincareThreeBody.analyticAt_delaunayRadius {firstAction eccentricity meanAnomaly : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) : AnalyticAt ℝ (delaunayRadius firstAction eccentricity) meanAnomaly

theorem LeanPool.PoincareThreeBody.polarKeplerEnergy_eccentricPolarState {firstAction eccentricity anomaly polarAngle : ℝ} (hfirstAction : firstAction ≠ 0) (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) : polarKeplerEnergy (eccentricPolarState firstAction eccentricity anomaly polarAngle) = -1 / (2 * firstAction ^ 2)

The eccentric-anomaly formulas lie on the inertial Kepler energy shell -1 / (2 * I₁²).