Hyperbolic motions in the N-body problem

DefinitionMutual distances#✓fully proved

For a configuration \(x = (x_1, \dots, x_N) \in E^N\) of \(N\) points in a finite-dimensional real inner product space \(E\) and indices \(i, j\), the mutual distance of the \(i\)-th and \(j\)-th points is \(r_{ij}(x) = \lVert x_i - x_j \rVert\).

def r (x : Eᴺ) (i j : Fin N) : ℝ := dist (x i) (x j)

Used by 2

Used bySolutions of the \(N\)-body problem · Configurations without collisions

DefinitionConfigurations without collisions#✓fully proved

A configuration \(x = (x_1, \dots, x_N) \in E^N\) of \(N\) points in a finite-dimensional real inner product space \(E\) is without collisions if \(r_{ij}(x) = \lVert x_i - x_j \rVert \neq 0\) for all \(i \neq j\).

def WithoutCollisions (x : Eᴺ) : Prop := ∀ i j, i ≠ j → r x i j ≠ 0

Uses 1 · Used by 1

Statement usesMutual distances

Used byMaderna–Venturelli theorem on hyperbolic motions

StructureSolutions of the \(N\)-body problem#✓fully proved

Let \(E\) be a finite-dimensional real inner product space, let \(N\) be a natural number, give \(E^N\) the inner product \(\langle u, v \rangle = \sum_i \langle u_i, v_i \rangle\), and let \(m = (m_1, \dots, m_N) \in \mathbb{R}^N\) be masses. Let \(U(y) = \sum_{i < j} m_i m_j \lVert y_i - y_j \rVert^{-1}\) be the Newtonian potential on \(E^N\), and for \(f : E^N \to \mathbb{R}\) let \(\nabla_m f(y) \in E^N\) be the mass-weighted gradient, with components \((\nabla_m f(y))_i = m_i^{-1} (\nabla f(y))_i\), where \(\nabla f\) is the gradient of \(f\). A curve \(x : \mathbb{R} \to E^N\) is a solution of the \(N\)-body problem with masses \(m\) if \(x\) is \(C^2\) on \((0, \infty)\), \(x\) is continuous at \(0\), and \(x''(t) = \nabla_m U(x(t))\) for every \(t > 0\).

By convention \(0^{-1} = 0\) here, so a collision term contributes \(0\) to \(U\) and a zero mass gives a zero component of \(\nabla_m f\). Moreover \(\nabla f(y) = 0\) at every point \(y\) where \(f\) is not differentiable; for instance, a curve that stays at a collision with \(x'' = 0\) can be a solution in this sense.

structure IsNBodySolution (m : ℝᴺ) (x : ℝ → Eᴺ) where
  contDiff : ContDiffOn ℝ 2 x (Ioi 0)
  continuousAt_zero : ContinuousAt x 0
  eq : ∀ t > 0, iteratedDeriv 2 x t = ∇_[m] (U m) (x t)

Uses 1 · Used by 1

Statement usesMutual distances

Used byMaderna–Venturelli theorem on hyperbolic motions

TheoremMaderna–Venturelli theorem on hyperbolic motions#●ready to prove

Let \(E\) be a finite-dimensional real inner product space of dimension at least \(2\), let \(N\) be a natural number, and let \(m = (m_1, \dots, m_N)\) be positive masses. Let \(x_0 \in E^N\), let \(a \in E^N\) be a configuration without collisions with \(\lVert a \rVert_m = 1\), where \(\lVert a \rVert_m = \bigl(\sum_i m_i \lVert a_i \rVert^2\bigr)^{1/2}\), and let \(h > 0\). Then there are a solution \(x : \mathbb{R} \to E^N\) of the \(N\)-body problem with masses \(m\) and a function \(\varepsilon : \mathbb{R} \to E^N\) with \(\lVert \varepsilon(t) \rVert / t \to 0\) as \(t \to \infty\) such that \(x(0) = x_0\), the configuration \(x(t)\) is without collisions for every \(t > 0\), and \(x(t) = \sqrt{2h}\, t\, a + \varepsilon(t)\) for every \(t \ge 0\).

public theorem_wanted theorem_1_1 (hE : 2 ≤ Module.finrank ℝ E) (m : ℝᴺ) (hm : ∀ i, 0 < m i)
    (x₀ a : Eᴺ) (a_nc : WithoutCollisions a) (a_norm : ‖a‖_[m] = 1) (h : ℝ) (h_pos : h > 0) :
    ∃ x : ℝ → Eᴺ, ∃ o : ℝ → Eᴺ, (o =o[atTop] fun t ↦ t) ∧ x 0 = x₀ ∧
      IsNBodySolution m x ∧ (∀ t > 0, WithoutCollisions (x t)) ∧
        ∀ t ≥ 0, x t = (sqrt (2 * h) * t) • a + o t

Sources

• E. Maderna and A. Venturelli, Viscosity solutions and hyperbolic motions: a new PDE method for the N-body problem, Annals of Math, 192 (2) 2020. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge. Problem annals_viscosity_solutions of the lean-eval benchmark.

Uses 2

Statement usesSolutions of the \(N\)-body problem · Configurations without collisions

3 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.