Viscosity solutions and hyperbolic motions: a new PDE method for the N-body problem

Problem statement

Notes: Unavailable.

Source: 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 (v1.0.0, e32eb14), AnnalsChallenge/AnnalsOfMathematics/2020-192-2-ViscositySolutions.lean

Informal solution: Unavailable.

theorem declaration uses `sorry`theorem_1_1 (hE : 2 ≤ Module.finrank ℝ E) (m : ℝᴺ) (hm : ∀ i, 0 < m i)
    (x₀ a : Eᴺ) (a_nc : ViscositySolutions.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₀ ∧
      ViscositySolutions.IsNBodySolution m x ∧ (∀ t > 0, ViscositySolutions.WithoutCollisions (x t)) ∧
        ∀ t ≥ 0, x t = (sqrt (2 * h) * t) • a + o t := byE:Type u_1inst✝²:NormedAddCommGroup Einst✝¹:InnerProductSpace ℝ Einst✝:FiniteDimensional ℝ EN:ℕhE:2 ≤ Module.finrank ℝ Em:Fin N → ℝhm:∀ (i : Fin N), 0 < m ix₀:Eᴺa:Eᴺa_nc:WithoutCollisions aa_norm:‖a‖_[m] = 1h:ℝh_pos:h > 0⊢ ∃ x o,
  (o =o[atTop] fun t => t) ∧
    x 0 = x₀ ∧ IsNBodySolution m x ∧ (∀ t > 0, WithoutCollisions (x t)) ∧ ∀ t ≥ 0, x t = (√(2 * h) * t) • a + o t
  sorryAll goals completed! 🐙