Documentation

LeanPool.PoincareThreeBody.JointEccentricAnomaly

Joint analyticity of Kepler's equation #

The existing one-variable inverse theorem gives analyticity of the eccentric anomaly in mean anomaly for fixed eccentricity. Poincaré's coefficient argument also needs analytic dependence on eccentricity. We obtain it by applying the analytic inverse-function theorem to the triangular map (e, E) ↦ (e, E - e sin E).

source
noncomputable def LeanPool.PoincareThreeBody.eccentricKeplerMap (parameters : ℝ × ℝ) :
ℝ × ℝ

Kepler's equation while retaining eccentricity as a coordinate.

Equations
Instances For
    source
    noncomputable def LeanPool.PoincareThreeBody.eccentricKeplerMapFDeriv (parameters : ℝ × ℝ) :
    ℝ × ℝ →L[ℝ] ℝ × ℝ

    The derivative of eccentricKeplerMap.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem LeanPool.PoincareThreeBody.hasFDerivAt_eccentricKeplerMap (parameters : ℝ × ℝ) :
      HasFDerivAt eccentricKeplerMap (eccentricKeplerMapFDeriv parameters) parameters
      source
      theorem LeanPool.PoincareThreeBody.analyticAt_eccentricKeplerMap (parameters : ℝ × ℝ) :
      AnalyticAt ℝ eccentricKeplerMap parameters
      source
      theorem LeanPool.PoincareThreeBody.eccentricKeplerMapFDeriv_apply (parameters direction : ℝ × ℝ) :
      (eccentricKeplerMapFDeriv parameters) direction = (direction.1, -Real.sin parameters.2 * direction.1 + (1 - parameters.1 * Real.cos parameters.2) * direction.2)
      source
      theorem LeanPool.PoincareThreeBody.eccentricKeplerMapFDeriv_bijective {parameters : ℝ × ℝ} (hdenominator : 1 - parameters.1 * Real.cos parameters.2 ≠ 0) :
      Function.Bijective ⇑(eccentricKeplerMapFDeriv parameters)
      source
      noncomputable def LeanPool.PoincareThreeBody.jointEccentricAnomaly (parameters : ℝ × ℝ) :
      ℝ × ℝ

      Eccentricity and eccentric anomaly as a joint function of eccentricity and mean anomaly.

      Equations
      Instances For
        source
        theorem LeanPool.PoincareThreeBody.eccentricKeplerMap_jointEccentricAnomaly {parameters : ℝ × ℝ} (heccentricity : 0 ≤ parameters.1) :
        eccentricKeplerMap (jointEccentricAnomaly parameters) = parameters
        source
        theorem LeanPool.PoincareThreeBody.jointEccentricAnomaly_eccentricKeplerMap {parameters : ℝ × ℝ} (heccentricity : 0 ≤ parameters.1) (heccentricityOne : parameters.1 < 1) :
        jointEccentricAnomaly (eccentricKeplerMap parameters) = parameters
        source
        theorem LeanPool.PoincareThreeBody.analyticAt_jointEccentricAnomaly {parameters : ℝ × ℝ} (heccentricity : 0 < parameters.1) (heccentricityOne : parameters.1 < 1) :
        AnalyticAt ℝ jointEccentricAnomaly parameters

        The eccentric anomaly is jointly real analytic in eccentricity and mean anomaly throughout the elliptic range 0 < e < 1.

        source
        theorem LeanPool.PoincareThreeBody.analyticAt_eccentricAnomaly_joint {eccentricity meanAnomaly : ℝ} (heccentricity : 0 < eccentricity) (heccentricityOne : eccentricity < 1) :
        AnalyticAt ℝ (fun (parameters : ℝ × ℝ) => eccentricAnomaly parameters.1 parameters.2) (eccentricity, meanAnomaly)