Topology of the collision-free parameter domain

A shear u = x + μ makes the two moving primaries into the fixed punctures (0, 0) and (1, 0). In these coordinates the parameter domain is a product of an open mass interval, a twice-punctured plane, and the unrestricted momentum plane. This proves that the full domain is path-connected whenever the mass interval is nonempty.

@[reducible, inline]

abbrev LeanPool.PoincareThreeBody.Plane : Type

A two-dimensional real coordinate plane.

Equations

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

def LeanPool.PoincareThreeBody.parameterCoordinateEquiv : ℝ × PhaseSpace ≃ (ℝ × Plane) × Plane

Coordinates consisting of mass, the sheared position (x + μ, y), and momentum.

Equations

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

noncomputable def LeanPool.PoincareThreeBody.parameterCoordinateHomeomorph : ℝ × PhaseSpace ≃ₜ (ℝ × Plane) × Plane

The shear and coordinate splitting as a homeomorphism.

Equations

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

def LeanPool.PoincareThreeBody.primaryConfigurations : Set Plane

The two primary positions after straightening the moving coordinates.

Equations

• LeanPool.PoincareThreeBody.primaryConfigurations = {![0, 0], ![1, 0]}

def LeanPool.PoincareThreeBody.straightenedParameterDomain (δ : ℝ) : Set ((ℝ × Plane) × Plane)

Product form of the mass-restricted, collision-free domain.

Equations

• LeanPool.PoincareThreeBody.straightenedParameterDomain δ = (Set.Ioo (-δ) δ ×ˢ LeanPool.PoincareThreeBody.primaryConfigurationsᶜ) ×ˢ Set.univ

theorem LeanPool.PoincareThreeBody.parameterCoordinateHomeomorph_preimage_straightenedParameterDomain (δ : ℝ) : ⇑parameterCoordinateHomeomorph ⁻¹' straightenedParameterDomain δ = parameterDomain δ

The original parameter domain is the preimage of its product form under the shear.

theorem LeanPool.PoincareThreeBody.isPathConnected_primaryConfigurations_compl : IsPathConnected primaryConfigurationsᶜ

The plane with the two primary positions removed is path-connected.

theorem LeanPool.PoincareThreeBody.isPathConnected_straightenedParameterDomain {δ : ℝ} (hδ : 0 < δ) : IsPathConnected (straightenedParameterDomain δ)

The straightened parameter domain is path-connected for a positive mass radius.

theorem LeanPool.PoincareThreeBody.isPreconnected_parameterDomain {δ : ℝ} (hδ : 0 < δ) : IsPreconnected (parameterDomain δ)

The collision-free parameter domain in the challenge is preconnected.

def LeanPool.PoincareThreeBody.phaseCoordinateEquiv : PhaseSpace ≃ Plane × Plane

Split a phase point into its position and momentum planes.

Equations

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

noncomputable def LeanPool.PoincareThreeBody.phaseCoordinateHomeomorph : PhaseSpace ≃ₜ Plane × Plane

Position/momentum splitting as a homeomorphism.

Equations

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

def LeanPool.PoincareThreeBody.massZeroCollisionFree : Set PhaseSpace

The mass-zero phase domain, excluding both fixed primary positions.

Equations

• LeanPool.PoincareThreeBody.massZeroCollisionFree = {state : LeanPool.PoincareThreeBody.PhaseSpace | (0, state) ∈ LeanPool.PoincareThreeBody.collisionFree}

theorem LeanPool.PoincareThreeBody.phaseCoordinateHomeomorph_preimage_primaryConfigurations : ⇑phaseCoordinateHomeomorph ⁻¹' primaryConfigurationsᶜ ×ˢ Set.univ = massZeroCollisionFree

The mass-zero collision-free phase domain is a twice-punctured position plane times the unrestricted momentum plane.

theorem LeanPool.PoincareThreeBody.isPathConnected_massZeroCollisionFree : IsPathConnected massZeroCollisionFree

The full mass-zero collision-free phase domain is path-connected.

theorem LeanPool.PoincareThreeBody.isPreconnected_massZeroCollisionFree : IsPreconnected massZeroCollisionFree