The planar circular restricted three-body Hamiltonian

This file gives the exact definitions occurring in the Poincaré nonintegrability challenge and establishes their elementary structural properties. It deliberately does not import the challenge module: the solution and challenge environments must remain separately exportable for comparator.

@[reducible, inline]

abbrev LeanPool.PoincareThreeBody.PhaseSpace : Type

Planar canonical phase space, ordered as (x, y, pₓ, pᵧ).

Equations

• LeanPool.PoincareThreeBody.PhaseSpace = (Fin 4 → ℝ)

def LeanPool.PoincareThreeBody.firstPrimaryDistanceSq (μ : ℝ) (s : PhaseSpace) : ℝ

Squared distance from the primary of mass μ at (1 - μ, 0).

Equations

• LeanPool.PoincareThreeBody.firstPrimaryDistanceSq μ s = (s 0 - 1 + μ) ^ 2 + s 1 ^ 2

def LeanPool.PoincareThreeBody.secondPrimaryDistanceSq (μ : ℝ) (s : PhaseSpace) : ℝ

Squared distance from the primary of mass 1 - μ at (-μ, 0).

Equations

• LeanPool.PoincareThreeBody.secondPrimaryDistanceSq μ s = (s 0 + μ) ^ 2 + s 1 ^ 2

def LeanPool.PoincareThreeBody.collisionFree : Set (ℝ × PhaseSpace)

The collision-free joint mass-parameter/phase-space domain.

Equations

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

def LeanPool.PoincareThreeBody.parameterDomain (δ : ℝ) : Set (ℝ × PhaseSpace)

The collision-free domain with the mass parameter restricted to |μ| < δ.

Equations

• LeanPool.PoincareThreeBody.parameterDomain δ = {z : ℝ × LeanPool.PoincareThreeBody.PhaseSpace | |z.1| < δ ∧ z ∈ LeanPool.PoincareThreeBody.collisionFree}

noncomputable def LeanPool.PoincareThreeBody.potential (μ : ℝ) (s : PhaseSpace) : ℝ

The Newtonian potential in the rotating frame.

Equations

• LeanPool.PoincareThreeBody.potential μ s = μ / √(LeanPool.PoincareThreeBody.firstPrimaryDistanceSq μ s) + (1 - μ) / √(LeanPool.PoincareThreeBody.secondPrimaryDistanceSq μ s)

noncomputable def LeanPool.PoincareThreeBody.hamiltonian (μ : ℝ) (s : PhaseSpace) : ℝ

The planar circular restricted three-body Hamiltonian in rotating canonical coordinates.

Equations

• LeanPool.PoincareThreeBody.hamiltonian μ s = (s 2 ^ 2 + s 3 ^ 2) / 2 + s 2 * s 1 - s 3 * s 0 - LeanPool.PoincareThreeBody.potential μ s

def LeanPool.PoincareThreeBody.coordinateVector (i : Fin 4) : PhaseSpace

The coordinate basis vector in the concrete phase space.

Equations

• LeanPool.PoincareThreeBody.coordinateVector i j = if j = i then 1 else 0

noncomputable def LeanPool.PoincareThreeBody.poissonBracket (F G : PhaseSpace → ℝ) (s : PhaseSpace) : ℝ

The canonical Poisson bracket in coordinates (x, y, pₓ, pᵧ).

Equations

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

def LeanPool.PoincareThreeBody.IsJointlyAnalytic (δ : ℝ) (F : ℝ → PhaseSpace → ℝ) : Prop

Joint real analyticity in the mass parameter and phase variables.

Equations

• LeanPool.PoincareThreeBody.IsJointlyAnalytic δ F = AnalyticOnNhd ℝ (Function.uncurry F) (LeanPool.PoincareThreeBody.parameterDomain δ)

noncomputable def LeanPool.PoincareThreeBody.IsFirstIntegralFamily (δ : ℝ) (F : ℝ → PhaseSpace → ℝ) : Prop

A first-integral family Poisson-commutes with the Hamiltonian throughout the domain.

Equations

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

noncomputable def LeanPool.PoincareThreeBody.IsIndependentSomewhere (δ : ℝ) (F : ℝ → PhaseSpace → ℝ) : Prop

Functional independence of the phase differentials at some point.

Equations

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

theorem LeanPool.PoincareThreeBody.firstPrimaryDistanceSq_nonneg (μ : ℝ) (s : PhaseSpace) : 0 ≤ firstPrimaryDistanceSq μ s

theorem LeanPool.PoincareThreeBody.secondPrimaryDistanceSq_nonneg (μ : ℝ) (s : PhaseSpace) : 0 ≤ secondPrimaryDistanceSq μ s

theorem LeanPool.PoincareThreeBody.firstPrimaryDistanceSq_pos {μ : ℝ} {s : PhaseSpace} (h : firstPrimaryDistanceSq μ s ≠ 0) : 0 < firstPrimaryDistanceSq μ s

theorem LeanPool.PoincareThreeBody.secondPrimaryDistanceSq_pos {μ : ℝ} {s : PhaseSpace} (h : secondPrimaryDistanceSq μ s ≠ 0) : 0 < secondPrimaryDistanceSq μ s

theorem LeanPool.PoincareThreeBody.mem_collisionFree_iff {μ : ℝ} {s : PhaseSpace} : (μ, s) ∈ collisionFree ↔ firstPrimaryDistanceSq μ s ≠ 0 ∧ secondPrimaryDistanceSq μ s ≠ 0

theorem LeanPool.PoincareThreeBody.mem_parameterDomain_iff {δ μ : ℝ} {s : PhaseSpace} : (μ, s) ∈ parameterDomain δ ↔ |μ| < δ ∧ (μ, s) ∈ collisionFree

@[simp]

theorem LeanPool.PoincareThreeBody.coordinateVector_same (i : Fin 4) : coordinateVector i i = 1

@[simp]

theorem LeanPool.PoincareThreeBody.coordinateVector_apply {i j : Fin 4} (h : j ≠ i) : coordinateVector i j = 0

theorem LeanPool.PoincareThreeBody.poissonBracket_self (F : PhaseSpace → ℝ) (s : PhaseSpace) : poissonBracket F F s = 0

theorem LeanPool.PoincareThreeBody.hamiltonian_isFirstIntegralFamily (δ : ℝ) : IsFirstIntegralFamily δ hamiltonian

theorem LeanPool.PoincareThreeBody.hamiltonian_zero (s : PhaseSpace) : hamiltonian 0 s = (s 2 ^ 2 + s 3 ^ 2) / 2 + s 2 * s 1 - s 3 * s 0 - 1 / √(s 0 ^ 2 + s 1 ^ 2)

theorem LeanPool.PoincareThreeBody.IsFirstIntegralFamily.poissonBracket_zero_at_mass_zero {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} (hδ : 0 < δ) (hF : IsFirstIntegralFamily δ F) {s : PhaseSpace} (hs : (0, s) ∈ collisionFree) : poissonBracket (F 0) (hamiltonian 0) s = 0

theorem LeanPool.PoincareThreeBody.hamiltonian_not_independent (δ : ℝ) : ¬IsIndependentSomewhere δ hamiltonian