Averaging the first homological equation

On a resonant periodic orbit, the first-order correction to a putative first integral is periodic. Integrating its derivative over one period removes that term. A nonzero averaged perturbation then forces the leading differential of the integral to annihilate the resonance vector.

theorem LeanPool.PoincareThreeBody.intervalIntegral_derivative_eq_zero_of_endpoints_eq {correction correctionDerivative : ℝ → ℝ} {period : ℝ} (hderiv : ∀ time ∈ Set.uIcc 0 period, HasDerivAt correction (correctionDerivative time) time) (hintegrable : IntervalIntegrable correctionDerivative MeasureTheory.volume 0 period) (hperiodic : correction period = correction 0) : ∫ (time : ℝ) in 0..period, correctionDerivative time = 0

The derivative of a periodic scalar function has zero integral over a period.

theorem LeanPool.PoincareThreeBody.intervalIntegral_forcing_eq_zero_of_homologicalEquation {correction correctionDerivative forcing : ℝ → ℝ} {period : ℝ} (hderiv : ∀ time ∈ Set.uIcc 0 period, HasDerivAt correction (correctionDerivative time) time) (hcorrectionIntegrable : IntervalIntegrable correctionDerivative MeasureTheory.volume 0 period) (hforcingIntegrable : IntervalIntegrable forcing MeasureTheory.volume 0 period) (hperiodic : correction period = correction 0) (hequation : ∀ time ∈ Set.uIcc 0 period, correctionDerivative time + forcing time = 0) : ∫ (time : ℝ) in 0..period, forcing time = 0

If a first homological equation is a periodic total derivative plus a forcing term, then the forcing has zero average over the period.

theorem LeanPool.PoincareThreeBody.coefficient_eq_zero_of_averaged_homologicalEquation {correction correctionDerivative forcing : ℝ → ℝ} {coefficient period : ℝ} (hderiv : ∀ time ∈ Set.uIcc 0 period, HasDerivAt correction (correctionDerivative time) time) (hcorrectionIntegrable : IntervalIntegrable correctionDerivative MeasureTheory.volume 0 period) (hforcingIntegrable : IntervalIntegrable forcing MeasureTheory.volume 0 period) (hperiodic : correction period = correction 0) (hforcing : ∫ (time : ℝ) in 0..period, forcing time ≠ 0) (hequation : ∀ time ∈ Set.uIcc 0 period, correctionDerivative time + coefficient * forcing time = 0) : coefficient = 0

Averaging a scalar first homological equation over a periodic orbit kills its correction term.

theorem LeanPool.PoincareThreeBody.averagedHomologicalEquation_obstruction {k frequency differential : ActionSpace} {correction correctionDerivative forcing : ℝ → ℝ} {period : ℝ} (hk : k ≠ 0) (hresonance : dot k frequency = 0) (hderiv : ∀ time ∈ Set.uIcc 0 period, HasDerivAt correction (correctionDerivative time) time) (hcorrectionIntegrable : IntervalIntegrable correctionDerivative MeasureTheory.volume 0 period) (hforcingIntegrable : IntervalIntegrable forcing MeasureTheory.volume 0 period) (hperiodic : correction period = correction 0) (hforcing : ∫ (time : ℝ) in 0..period, forcing time ≠ 0) (hequation : ∀ time ∈ Set.uIcc 0 period, correctionDerivative time + dot k differential * forcing time = 0) : ¬LinearIndependent ℝ ![frequency, differential]

A nonzero averaged perturbation on a resonant orbit yields Poincaré's two-dimensional linear-dependence obstruction.