Resonant covectors in two degrees of freedom

This file develops the elementary linear-algebra step in Poincaré's nonintegrability argument. At a resonant action, both the unperturbed frequency and the differential of the leading coefficient of a putative first integral annihilate the same nonzero resonance vector. In two dimensions, the two covectors must therefore be linearly dependent.

@[reducible, inline]

abbrev LeanPool.PoincareThreeBody.ActionSpace : Type

The two-dimensional action or frequency space used in the planar problem.

Equations

• LeanPool.PoincareThreeBody.ActionSpace = (Fin 2 → ℝ)

def LeanPool.PoincareThreeBody.dot (u v : ActionSpace) : ℝ

The coordinate dot product on the two-dimensional action space.

Equations

• LeanPool.PoincareThreeBody.dot u v = ∑ i : Fin 2, u i * v i

def LeanPool.PoincareThreeBody.wedge (u v : ActionSpace) : ℝ

The oriented area spanned by two vectors in the action space.

Equations

• LeanPool.PoincareThreeBody.wedge u v = u 0 * v 1 - u 1 * v 0

theorem LeanPool.PoincareThreeBody.dot_eq (u v : ActionSpace) : dot u v = u 0 * v 0 + u 1 * v 1

theorem LeanPool.PoincareThreeBody.wedge_eq_zero_of_resonance {k u v : ActionSpace} (hk : k ≠ 0) (hu : dot k u = 0) (hv : dot k v = 0) : wedge u v = 0

Two covectors annihilating the same nonzero vector in dimension two have zero wedge.

theorem LeanPool.PoincareThreeBody.not_linearIndependent_of_wedge_eq_zero {u v : ActionSpace} (h : wedge u v = 0) : ¬LinearIndependent ℝ ![u, v]

Zero wedge is equivalent to failure of linear independence for two vectors in dimension two.

theorem LeanPool.PoincareThreeBody.not_linearIndependent_of_common_resonance {k frequency differential : ActionSpace} (hk : k ≠ 0) (hfrequency : dot k frequency = 0) (hdifferential : dot k differential = 0) : ¬LinearIndependent ℝ ![frequency, differential]

The resonant linear-algebra obstruction in the form used by the perturbative proof.

theorem LeanPool.PoincareThreeBody.homologicalEquation_obstruction {k frequency differential : ActionSpace} {correction perturbation : ℝ} (hk : k ≠ 0) (hresonance : dot k frequency = 0) (hperturbation : perturbation ≠ 0) (hequation : dot k frequency * correction + dot k differential * perturbation = 0) : ¬LinearIndependent ℝ ![frequency, differential]

A nonzero perturbing Fourier mode turns the first homological equation into the second orthogonality relation needed by the resonant obstruction.

theorem LeanPool.PoincareThreeBody.wedge_eq_zero_of_dense_resonances {X : Type u_1} [TopologicalSpace X] {resonantActions : Set X} (hdense : Dense resonantActions) {frequency differential : X → ActionSpace} (hfrequency : Continuous frequency) (hdifferential : Continuous differential) (hresonant : ∀ x ∈ resonantActions, wedge (frequency x) (differential x) = 0) (x : X) : wedge (frequency x) (differential x) = 0

A continuous wedge that vanishes on a dense family of resonant actions vanishes everywhere.

theorem LeanPool.PoincareThreeBody.denseResonance_obstruction {X : Type u_1} [TopologicalSpace X] {resonantActions : Set X} (hdense : Dense resonantActions) {frequency differential : X → ActionSpace} (hfrequency : Continuous frequency) (hdifferential : Continuous differential) (hresonant : ∀ x ∈ resonantActions, wedge (frequency x) (differential x) = 0) (x : X) : ¬LinearIndependent ℝ ![frequency x, differential x]

Dense resonant obstructions force dependence at every action in the two-dimensional family.