The resonant disturbing average

Rotating the inertial ellipse by an orientation phase produces the phase family on a resonant torus. We define the first-order disturbing function on this family and its average over the common period. Nonconstancy of this average is the concrete perturbative input in Poincaré's argument.

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

A resonant Kepler ellipse with an arbitrary inertial orientation phase.

Equations

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

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

The oriented resonant position embedded in phase space.

Equations

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

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

The first-order disturbing function along an oriented resonant ellipse.

Equations

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

noncomputable def LeanPool.PoincareThreeBody.resonantDisturbingAverage (p q : ℕ) (eccentricity orientation : ℝ) : ℝ

The disturbing function averaged over one common resonant period.

Equations

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

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

Orientation derivative of the disturbing function along a resonant ellipse.

Equations

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

theorem LeanPool.PoincareThreeBody.orientedResonantEllipsePosition_zero_orientation (p q : ℕ) (eccentricity time : ℝ) : orientedResonantEllipsePosition p q eccentricity 0 time = resonantRotatingEllipsePosition p q eccentricity time

theorem LeanPool.PoincareThreeBody.orientedResonantEllipsePosition_eq_fixedRotation (p q : ℕ) (eccentricity orientation time : ℝ) : orientedResonantEllipsePosition p q eccentricity orientation time = positionInRotatingFrame (-orientation) (resonantRotatingEllipsePosition p q eccentricity time)

theorem LeanPool.PoincareThreeBody.analyticAt_orientedResonantEllipsePosition_coordinate (p q : ℕ) {eccentricity orientation time : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) (coordinate : Fin 2) : AnalyticAt ℝ (fun (argument : ℝ) => orientedResonantEllipsePosition p q eccentricity orientation argument coordinate) time

theorem LeanPool.PoincareThreeBody.continuous_orientedResonantEllipsePosition_coordinate (p q : ℕ) {eccentricity : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) (coordinate : Fin 2) : Continuous fun (parameters : ℝ × ℝ) => orientedResonantEllipsePosition p q eccentricity parameters.1 parameters.2 coordinate

theorem LeanPool.PoincareThreeBody.orientedResonantEllipsePosition_sq {p q : ℕ} {eccentricity orientation time : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity ≤ 1) : orientedResonantEllipsePosition p q eccentricity orientation time 0 ^ 2 + orientedResonantEllipsePosition p q eccentricity orientation time 1 ^ 2 = eccentricRadius (resonantFirstAction p q) eccentricity (resonantEccentricAnomaly p q eccentricity time) ^ 2

theorem LeanPool.PoincareThreeBody.continuous_resonantDisturbingOrientationDerivative {p q : ℕ} (hp : 0 < p) (hq : 0 < q) {eccentricity : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) (hapoapsis : resonantFirstAction p q ^ 2 * (1 + eccentricity) < 1) : Continuous fun (parameters : ℝ × ℝ) => resonantDisturbingOrientationDerivative p q eccentricity parameters.1 parameters.2

theorem LeanPool.PoincareThreeBody.hasDerivAt_orientedResonantEllipsePosition_zero_orientation (p q : ℕ) (eccentricity orientation time : ℝ) : HasDerivAt (fun (phase : ℝ) => orientedResonantEllipsePosition p q eccentricity phase time 0) (-orientedResonantEllipsePosition p q eccentricity orientation time 1) orientation

theorem LeanPool.PoincareThreeBody.hasDerivAt_orientedResonantEllipsePosition_one_orientation (p q : ℕ) (eccentricity orientation time : ℝ) : HasDerivAt (fun (phase : ℝ) => orientedResonantEllipsePosition p q eccentricity phase time 1) (orientedResonantEllipsePosition p q eccentricity orientation time 0) orientation

theorem LeanPool.PoincareThreeBody.hasDerivAt_resonantDisturbingFunction_orientation {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 (fun (phase : ℝ) => resonantDisturbingFunction p q eccentricity phase time) (resonantDisturbingOrientationDerivative p q eccentricity orientation time) orientation

Differentiating the disturbing function with respect to the ellipse orientation gives the explicit rotational derivative.

theorem LeanPool.PoincareThreeBody.analyticAt_resonantDisturbingOrientationDerivative {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) : AnalyticAt ℝ (resonantDisturbingOrientationDerivative p q eccentricity orientation) time

theorem LeanPool.PoincareThreeBody.intervalIntegrable_resonantDisturbingOrientationDerivative {p q : ℕ} (hp : 0 < p) (hq : 0 < q) {eccentricity orientation start finish : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) (hapoapsis : resonantFirstAction p q ^ 2 * (1 + eccentricity) < 1) : IntervalIntegrable (resonantDisturbingOrientationDerivative p q eccentricity orientation) MeasureTheory.volume start finish

theorem LeanPool.PoincareThreeBody.analyticAt_resonantDisturbingFunction_time {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) : AnalyticAt ℝ (resonantDisturbingFunction p q eccentricity orientation) time

theorem LeanPool.PoincareThreeBody.intervalIntegrable_resonantDisturbingFunction {p q : ℕ} (hp : 0 < p) (hq : 0 < q) {eccentricity orientation start finish : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) (hapoapsis : resonantFirstAction p q ^ 2 * (1 + eccentricity) < 1) : IntervalIntegrable (resonantDisturbingFunction p q eccentricity orientation) MeasureTheory.volume start finish

theorem LeanPool.PoincareThreeBody.orientedResonantEllipse_primaryDistance_ne_zero_of_apoapsis_lt_one {p q : ℕ} {eccentricity orientation time : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) (hapoapsis : resonantFirstAction p q ^ 2 * (1 + eccentricity) < 1) : (orientedResonantEllipsePosition p q eccentricity orientation time 0 - 1) ^ 2 + orientedResonantEllipsePosition p q eccentricity orientation time 1 ^ 2 ≠ 0

theorem LeanPool.PoincareThreeBody.orientedResonantEllipsePosition_add_orientation_two_pi (p q : ℕ) (eccentricity orientation time : ℝ) : orientedResonantEllipsePosition p q eccentricity (orientation + 2 * Real.pi) time = orientedResonantEllipsePosition p q eccentricity orientation time

theorem LeanPool.PoincareThreeBody.orientedResonantEllipsePosition_add_period {p q : ℕ} (hp : 0 < p) {eccentricity orientation : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) (time : ℝ) : orientedResonantEllipsePosition p q eccentricity orientation (time + resonantOrbitPeriod p) = orientedResonantEllipsePosition p q eccentricity orientation time

theorem LeanPool.PoincareThreeBody.resonantDisturbingFunction_add_orientation_two_pi (p q : ℕ) (eccentricity orientation time : ℝ) : resonantDisturbingFunction p q eccentricity (orientation + 2 * Real.pi) time = resonantDisturbingFunction p q eccentricity orientation time

theorem LeanPool.PoincareThreeBody.resonantDisturbingFunction_add_period {p q : ℕ} (hp : 0 < p) {eccentricity orientation : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) (time : ℝ) : resonantDisturbingFunction p q eccentricity orientation (time + resonantOrbitPeriod p) = resonantDisturbingFunction p q eccentricity orientation time

theorem LeanPool.PoincareThreeBody.resonantDisturbingAverage_add_orientation_two_pi (p q : ℕ) (eccentricity orientation : ℝ) : resonantDisturbingAverage p q eccentricity (orientation + 2 * Real.pi) = resonantDisturbingAverage p q eccentricity orientation

theorem LeanPool.PoincareThreeBody.hasDerivAt_resonantDisturbingAverage {p q : ℕ} (hp : 0 < p) (hq : 0 < q) {eccentricity orientation : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) (hapoapsis : resonantFirstAction p q ^ 2 * (1 + eccentricity) < 1) : HasDerivAt (resonantDisturbingAverage p q eccentricity) (∫ (time : ℝ) in 0..resonantOrbitPeriod p, resonantDisturbingOrientationDerivative p q eccentricity orientation time) orientation

Differentiation under the period integral identifies the derivative of the Poincaré disturbing average with the integral of the explicit orientation forcing.

theorem LeanPool.PoincareThreeBody.deriv_resonantDisturbingAverage {p q : ℕ} (hp : 0 < p) (hq : 0 < q) {eccentricity orientation : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) (hapoapsis : resonantFirstAction p q ^ 2 * (1 + eccentricity) < 1) : deriv (resonantDisturbingAverage p q eccentricity) orientation = ∫ (time : ℝ) in 0..resonantOrbitPeriod p, resonantDisturbingOrientationDerivative p q eccentricity orientation time

theorem LeanPool.PoincareThreeBody.differentiable_resonantDisturbingAverage {p q : ℕ} (hp : 0 < p) (hq : 0 < q) {eccentricity : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) (hapoapsis : resonantFirstAction p q ^ 2 * (1 + eccentricity) < 1) : Differentiable ℝ (resonantDisturbingAverage p q eccentricity)

theorem LeanPool.PoincareThreeBody.exists_deriv_resonantDisturbingAverage_ne_zero_of_values_ne {p q : ℕ} (hp : 0 < p) (hq : 0 < q) {eccentricity phaseA phaseB : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) (hapoapsis : resonantFirstAction p q ^ 2 * (1 + eccentricity) < 1) (hvalues : resonantDisturbingAverage p q eccentricity phaseA ≠ resonantDisturbingAverage p q eccentricity phaseB) : ∃ (orientation : ℝ), deriv (resonantDisturbingAverage p q eccentricity) orientation ≠ 0

Distinct certified values of the Poincaré average imply a nonzero resonant forcing integral at some orientation. This is the interface intended for exact analytic estimates or validated finite computation.

theorem LeanPool.PoincareThreeBody.resonantDisturbingAverage_obstruction {p q : ℕ} (hp : 0 < p) (hq : 0 < q) {differential : ActionSpace} {eccentricity orientation : ℝ} {correction correctionDerivative : ℝ → ℝ} (hderiv : ∀ time ∈ Set.uIcc 0 (resonantOrbitPeriod p), HasDerivAt correction (correctionDerivative time) time) (hcorrectionIntegrable : IntervalIntegrable correctionDerivative MeasureTheory.volume 0 (resonantOrbitPeriod p)) (hforcingIntegrable : IntervalIntegrable (resonantDisturbingOrientationDerivative p q eccentricity orientation) MeasureTheory.volume 0 (resonantOrbitPeriod p)) (hperiodic : correction (resonantOrbitPeriod p) = correction 0) (hforcing : ∫ (time : ℝ) in 0..resonantOrbitPeriod p, resonantDisturbingOrientationDerivative p q eccentricity orientation time ≠ 0) (hequation : ∀ time ∈ Set.uIcc 0 (resonantOrbitPeriod p), correctionDerivative time + dot (resonanceVector p q) differential * resonantDisturbingOrientationDerivative p q eccentricity orientation time = 0) : ¬LinearIndependent ℝ ![delaunayFrequency (resonantFirstAction p q), differential]

The averaged homological obstruction specialized to the explicit resonant disturbing function. The remaining concrete input is nonvanishing of its orientation derivative integral.

theorem LeanPool.PoincareThreeBody.resonantDisturbingAverage_obstruction_of_apoapsis_lt_one {p q : ℕ} (hp : 0 < p) (hq : 0 < q) {differential : ActionSpace} {eccentricity orientation : ℝ} {correction correctionDerivative : ℝ → ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) (hapoapsis : resonantFirstAction p q ^ 2 * (1 + eccentricity) < 1) (hderiv : ∀ time ∈ Set.uIcc 0 (resonantOrbitPeriod p), HasDerivAt correction (correctionDerivative time) time) (hcorrectionIntegrable : IntervalIntegrable correctionDerivative MeasureTheory.volume 0 (resonantOrbitPeriod p)) (hperiodic : correction (resonantOrbitPeriod p) = correction 0) (hforcing : ∫ (time : ℝ) in 0..resonantOrbitPeriod p, resonantDisturbingOrientationDerivative p q eccentricity orientation time ≠ 0) (hequation : ∀ time ∈ Set.uIcc 0 (resonantOrbitPeriod p), correctionDerivative time + dot (resonanceVector p q) differential * resonantDisturbingOrientationDerivative p q eccentricity orientation time = 0) : ¬LinearIndependent ℝ ![delaunayFrequency (resonantFirstAction p q), differential]

Collision-free interior ellipses automatically satisfy the integrability hypothesis in the concrete averaged obstruction.

theorem LeanPool.PoincareThreeBody.resonantDisturbingAverage_deriv_obstruction {p q : ℕ} (hp : 0 < p) (hq : 0 < q) {differential : ActionSpace} {eccentricity orientation : ℝ} {correction correctionDerivative : ℝ → ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) (hapoapsis : resonantFirstAction p q ^ 2 * (1 + eccentricity) < 1) (hderiv : ∀ time ∈ Set.uIcc 0 (resonantOrbitPeriod p), HasDerivAt correction (correctionDerivative time) time) (hcorrectionIntegrable : IntervalIntegrable correctionDerivative MeasureTheory.volume 0 (resonantOrbitPeriod p)) (hperiodic : correction (resonantOrbitPeriod p) = correction 0) (haverageDeriv : deriv (resonantDisturbingAverage p q eccentricity) orientation ≠ 0) (hequation : ∀ time ∈ Set.uIcc 0 (resonantOrbitPeriod p), correctionDerivative time + dot (resonanceVector p q) differential * resonantDisturbingOrientationDerivative p q eccentricity orientation time = 0) : ¬LinearIndependent ℝ ![delaunayFrequency (resonantFirstAction p q), differential]

Equivalent concrete obstruction using nonvanishing of the derivative of the Poincaré disturbing average.