Convergence on a cylindrical end from uniform convergence of loops up to phase

import Definitions.Def_FiniteEnergyPlane_Asymptotics

namespace FiniteEnergyPlane

open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal Real

/-- Convergence on the cylindrical end from `C⁰` convergence of the loops up to phase. Let `u` be a
finite-energy curve on `D \ {0}` and suppose that, as `r → 0⁺`, the loops
`t ↦ proj H (u (r e^{-2πit}))` become uniformly `ε`-close to some phase shift
`t ↦ x(σTt + c')` of the Reeb orbit `P` (the phase `c'` may depend on `r`). Then `a = endA` and
`w = endW` are smooth on some `(s₀, ∞) × ℝ`, all derivatives of order `≥ 1` of `a(s, t) - σTs`
tend to `0` uniformly, and for every `m` and `ε > 0`, for all large `s` there is a phase `c'`
with `D^j (w - x(σT · + c'))(s, t)` of norm `≤ ε` for all `j ≤ m` and all `t`. -/
theorem cylEnd_tendsto_of_loops_tendstoUnif_mod_phase {n : ℕ} (H : V n → ℝ)
    (hH : IsStrictlyStarShapedLevel H) (J : V n → V n →L[ℝ] V n)
    (hJ : IsCompatibleXiStructure H J) (u : ℂ → V n)
    (hu : IsFiniteEnergyCurve H J (ball 0 1 \ {0}) u) (P : ReebOrbit H) (σ : ℝ)
    (hσ : σ = 1 ∨ σ = -1)
    (hloop : ∀ ε : ℝ, 0 < ε → ∀ᶠ r in 𝓝[>] (0 : ℝ), ∃ c' : ℝ, ∀ t : ℝ,
      ‖loopInS H u (cwLoop 0 r) t - P.x (σ * P.T * t + c')‖ ≤ ε) :
    (∃ s₀ : ℝ, ContDiffOn ℝ ∞ (endA H u cylEnd) (Set.Ioi s₀ ×ˢ Set.univ) ∧
        ContDiffOn ℝ ∞ (endW H u cylEnd) (Set.Ioi s₀ ×ˢ Set.univ)) ∧
      (∀ m : ℕ, 1 ≤ m → ∀ ε > 0, ∃ s₁ : ℝ, ∀ s ≥ s₁, ∀ t : ℝ,
        ‖iteratedFDeriv ℝ m (fun p : ℝ × ℝ => endA H u cylEnd p - σ * P.T * p.1) (s, t)‖ ≤ ε) ∧
      ∀ m : ℕ, ∀ ε > 0, ∃ s₁ : ℝ, ∀ s ≥ s₁, ∃ c' : ℝ, ∀ j ≤ m, ∀ t : ℝ,
        ‖iteratedFDeriv ℝ j
          (fun p : ℝ × ℝ => endW H u cylEnd p - P.x (σ * P.T * p.2 + c')) (s, t)‖ ≤ ε := by
  sorry

end FiniteEnergyPlane