The resonant action form of the first homological obstruction

This file connects the exact first homological equation to the derivative of Poincaré's resonant disturbing average. The bridge is the pointwise factorization of the leading differential through the physical Delaunay action map.

noncomputable def LeanPool.PoincareThreeBody.resonantPerturbationActionPoisson (p q : ℕ) (eccentricity orientation time : ℝ) : ActionSpace

The perturbation's two Poisson brackets with the physical actions along a resonant ellipse.

Equations

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

theorem LeanPool.PoincareThreeBody.hasDerivAt_orientedResonantKeplerPhasePoint_orientation {p q : ℕ} (hp : 0 < p) (hq : 0 < q) (eccentricity orientation time : ℝ) : HasDerivAt (fun (phase : ℝ) => orientedResonantKeplerPhasePoint p q eccentricity phase time) (angularActionVectorField (orientedResonantKeplerPhasePoint p q eccentricity orientation time)) orientation

Varying the inertial orientation at fixed time follows the angular-action Hamiltonian vector field on the full resonant phase trajectory.

theorem LeanPool.PoincareThreeBody.differentiableAt_firstMassPerturbation_orientedResonantKeplerPhasePoint {p q : ℕ} (hp : 0 < p) (hq : 0 < q) {eccentricity orientation time : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) (hapoapsis : resonantFirstAction p q ^ 2 * (1 + eccentricity) < 1) : DifferentiableAt ℝ firstMassPerturbation (orientedResonantKeplerPhasePoint p q eccentricity orientation time)

The first mass perturbation is differentiable at every collision-free point of an interior resonant ellipse.

theorem LeanPool.PoincareThreeBody.resonantPerturbationActionPoisson_one {p q : ℕ} (hp : 0 < p) (hq : 0 < q) {eccentricity orientation time : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) (hapoapsis : resonantFirstAction p q ^ 2 * (1 + eccentricity) < 1) : resonantPerturbationActionPoisson p q eccentricity orientation time 1 = resonantDisturbingOrientationDerivative p q eccentricity orientation time

The angular component of the perturbation action vector is the explicit orientation derivative used in the disturbing average.

theorem LeanPool.PoincareThreeBody.hasDerivAt_resonantDisturbingFunction_time_actionPoisson {p q : ℕ} (hp : 0 < p) (hq : 0 < q) {eccentricity orientation time : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) (hapoapsis : resonantFirstAction p q ^ 2 * (1 + eccentricity) < 1) : HasDerivAt (resonantDisturbingFunction p q eccentricity orientation) (dot (delaunayFrequency (resonantFirstAction p q)) (resonantPerturbationActionPoisson p q eccentricity orientation time)) time

Along the unperturbed resonant flow, the time derivative of the disturbing function is the Kepler frequency contracted with the perturbation action Poisson vector.

theorem LeanPool.PoincareThreeBody.IsFirstIntegralFamily.resonantCandidateForcing_eq_neg_dot_actionPoisson {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} (hδ : 0 < δ) (hanalytic : IsJointlyAnalytic δ F) (hfirstIntegral : IsFirstIntegralFamily δ F) {p q : ℕ} (hp : 0 < p) (hq : 0 < q) {eccentricity orientation time : ℝ} (heccentricity : 0 < eccentricity) (heccentricityOne : eccentricity < 1) (hapoapsis : resonantFirstAction p q ^ 2 * (1 + eccentricity) < 1) : resonantCandidateForcing F p q eccentricity orientation time = -dot (leadingActionDifferential F ![resonantFirstAction p q, angularActionFromEccentricity (resonantFirstAction p q) eccentricity]) (resonantPerturbationActionPoisson p q eccentricity orientation time)

The candidate forcing is the negative contraction of its leading action differential with the perturbation action Poisson vector.

noncomputable def LeanPool.PoincareThreeBody.resonantLeadingActionDifferential (F : ℝ → PhaseSpace → ℝ) (p q : ℕ) (eccentricity : ℝ) : ActionSpace

The leading action differential at the actions carried by a resonant eccentric ellipse.

Equations

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

noncomputable def LeanPool.PoincareThreeBody.resonantCombinedCorrection (F : ℝ → PhaseSpace → ℝ) (p q : ℕ) (eccentricity orientation time : ℝ) : ℝ

The correction whose derivative isolates the resonant orientation forcing.

Equations

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

noncomputable def LeanPool.PoincareThreeBody.resonantCombinedCorrectionDerivative (F : ℝ → PhaseSpace → ℝ) (p q : ℕ) (eccentricity orientation time : ℝ) : ℝ

Displayed derivative of the combined resonant correction.

Equations

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

theorem LeanPool.PoincareThreeBody.IsJointlyAnalytic.hasDerivAt_resonantCombinedCorrection {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} (hδ : 0 < δ) (hanalytic : IsJointlyAnalytic δ F) {p q : ℕ} (hp : 0 < p) (hq : 0 < q) {eccentricity orientation time : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) (hapoapsis : resonantFirstAction p q ^ 2 * (1 + eccentricity) < 1) : HasDerivAt (resonantCombinedCorrection F p q eccentricity orientation) (resonantCombinedCorrectionDerivative F p q eccentricity orientation time) time

The combined correction has the displayed derivative.

theorem LeanPool.PoincareThreeBody.continuous_resonantCombinedCorrectionDerivative {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} (hδ : 0 < δ) (hanalytic : IsJointlyAnalytic δ F) {p q : ℕ} (hp : 0 < p) (hq : 0 < q) {eccentricity orientation : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) (hapoapsis : resonantFirstAction p q ^ 2 * (1 + eccentricity) < 1) : Continuous (resonantCombinedCorrectionDerivative F p q eccentricity orientation)

The derivative of the combined correction is continuous, hence interval integrable.

theorem LeanPool.PoincareThreeBody.resonantCombinedCorrection_periodic (F : ℝ → PhaseSpace → ℝ) {p q : ℕ} (hp : 0 < p) {eccentricity orientation : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) : resonantCombinedCorrection F p q eccentricity orientation (resonantOrbitPeriod p) = resonantCombinedCorrection F p q eccentricity orientation 0

The combined correction inherits the common resonant period.

theorem LeanPool.PoincareThreeBody.IsFirstIntegralFamily.resonantCombinedHomologicalEquation {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} (hδ : 0 < δ) (hanalytic : IsJointlyAnalytic δ F) (hfirstIntegral : IsFirstIntegralFamily δ F) {p q : ℕ} (hp : 0 < p) (hq : 0 < q) {eccentricity orientation time : ℝ} (heccentricity : 0 < eccentricity) (heccentricityOne : eccentricity < 1) (hapoapsis : resonantFirstAction p q ^ 2 * (1 + eccentricity) < 1) : resonantCombinedCorrectionDerivative F p q eccentricity orientation time + dot (resonanceVector p q) (resonantLeadingActionDifferential F p q eccentricity) * resonantDisturbingOrientationDerivative p q eccentricity orientation time = 0

The exact homological equation, after combining its time-derivative part with the perturbation time derivative, has coefficient k · d f₀ multiplying the orientation forcing.

theorem LeanPool.PoincareThreeBody.IsFirstIntegralFamily.resonantLeadingDifferential_orthogonal {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} (hδ : 0 < δ) (hanalytic : IsJointlyAnalytic δ F) (hfirstIntegral : IsFirstIntegralFamily δ F) {p q : ℕ} (hp : 0 < p) (hq : 0 < q) {eccentricity orientation : ℝ} (heccentricity : 0 < eccentricity) (heccentricityOne : eccentricity < 1) (hapoapsis : resonantFirstAction p q ^ 2 * (1 + eccentricity) < 1) (haverageDeriv : deriv (resonantDisturbingAverage p q eccentricity) orientation ≠ 0) : dot (resonanceVector p q) (resonantLeadingActionDifferential F p q eccentricity) = 0

A nonzero derivative of Poincaré's disturbing average forces the leading action differential to annihilate the integer resonance vector.

theorem LeanPool.PoincareThreeBody.IsFirstIntegralFamily.resonantLeadingDifferential_obstruction {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} (hδ : 0 < δ) (hanalytic : IsJointlyAnalytic δ F) (hfirstIntegral : IsFirstIntegralFamily δ F) {p q : ℕ} (hp : 0 < p) (hq : 0 < q) {eccentricity orientation : ℝ} (heccentricity : 0 < eccentricity) (heccentricityOne : eccentricity < 1) (hapoapsis : resonantFirstAction p q ^ 2 * (1 + eccentricity) < 1) (haverageDeriv : deriv (resonantDisturbingAverage p q eccentricity) orientation ≠ 0) : ¬LinearIndependent ℝ ![delaunayFrequency (resonantFirstAction p q), resonantLeadingActionDifferential F p q eccentricity]

A nonzero derivative of Poincaré's disturbing average forces dependence of the Hamiltonian and leading-integral differentials at that resonant action.