The first homological equation on a resonant Kepler orbit

This file restricts the homological equation forced by the exact challenge hypotheses to the true periodic Kepler flow. Its first term becomes a time derivative, so its integral over one resonant period vanishes.

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

The first mass coefficient of a candidate integral, restricted to a resonant Kepler orbit.

Equations

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

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

The remaining forcing term in the first homological equation, restricted to the same orbit.

Equations

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

theorem LeanPool.PoincareThreeBody.continuousAt_poissonBracket_comp {f g : PhaseSpace → ℝ} {orbit : ℝ → PhaseSpace} {time : ℝ} (hf : ContDiffAt ℝ 1 f (orbit time)) (hg : ContDiffAt ℝ 1 g (orbit time)) (horbit : ContinuousAt orbit time) : ContinuousAt (fun (argument : ℝ) => poissonBracket f g (orbit argument)) time

A Poisson bracket of two C¹ observables varies continuously along a continuous phase-space curve.

theorem LeanPool.PoincareThreeBody.IsFirstIntegralFamily.firstHomologicalEquation_on_resonantKeplerOrbit {δ : ℝ} {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) : poissonBracket (parameterCoefficient (Function.uncurry F)) (hamiltonian 0) (orientedResonantKeplerPhasePoint p q eccentricity orientation time) + resonantCandidateForcing F p q eccentricity orientation time = 0

The exact challenge hypotheses imply the explicit first homological equation at every point of an interior resonant Kepler ellipse.

theorem LeanPool.PoincareThreeBody.IsJointlyAnalytic.hasDerivAt_resonantCandidateCorrection {δ : ℝ} {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 (resonantCandidateCorrection F p q eccentricity orientation) (poissonBracket (parameterCoefficient (Function.uncurry F)) (hamiltonian 0) (orientedResonantKeplerPhasePoint p q eccentricity orientation time)) time

The correction term in the resonant homological equation has the expected Poisson bracket as its time derivative.

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

The correction is periodic because it is a scalar observable evaluated on the periodic Kepler phase trajectory.

theorem LeanPool.PoincareThreeBody.continuous_resonantCandidateCorrectionDerivative {δ : ℝ} {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 fun (time : ℝ) => poissonBracket (parameterCoefficient (Function.uncurry F)) (hamiltonian 0) (orientedResonantKeplerPhasePoint p q eccentricity orientation time)

The derivative term in the restricted homological equation is continuous in time.

theorem LeanPool.PoincareThreeBody.continuous_resonantCandidateForcing {δ : ℝ} {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 (resonantCandidateForcing F p q eccentricity orientation)

The forcing term in the restricted homological equation is continuous in time.

theorem LeanPool.PoincareThreeBody.IsFirstIntegralFamily.integral_resonantCandidateForcing_eq_zero_of_intervalIntegrable {δ : ℝ} {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) (hcorrectionIntegrable : IntervalIntegrable (fun (time : ℝ) => poissonBracket (parameterCoefficient (Function.uncurry F)) (hamiltonian 0) (orientedResonantKeplerPhasePoint p q eccentricity orientation time)) MeasureTheory.volume 0 (resonantOrbitPeriod p)) (hforcingIntegrable : IntervalIntegrable (resonantCandidateForcing F p q eccentricity orientation) MeasureTheory.volume 0 (resonantOrbitPeriod p)) : ∫ (time : ℝ) in 0..resonantOrbitPeriod p, resonantCandidateForcing F p q eccentricity orientation time = 0

Averaging the exact first homological equation along a resonant Kepler orbit forces the candidate's perturbative forcing to have zero period integral. The two interval-integrability hypotheses are isolated here so that later analytic estimates can discharge them independently.

theorem LeanPool.PoincareThreeBody.IsFirstIntegralFamily.integral_resonantCandidateForcing_eq_zero {δ : ℝ} {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) : ∫ (time : ℝ) in 0..resonantOrbitPeriod p, resonantCandidateForcing F p q eccentricity orientation time = 0

Every candidate satisfying the exact analytic first-integral hypotheses has zero averaged first-order forcing on every interior resonant Kepler ellipse.