Uniqueness of analytic autonomous trajectories, including trajectories from different labels.

theorem KamProject.Arnold1963.eq_of_analytic_autonomous_orbits {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedSpace ℝ E] [CompleteSpace E] {X : E → E} {f g : ℝ → E} (ha : ∀ (t : ℝ), AnalyticAt ℂ X (f t)) (hf : ∀ (t : ℝ), HasDerivAt f (X (f t)) t) (hg : ∀ (t : ℝ), HasDerivAt g (X (g t)) t) (he : f 0 = g 0) : f = g

theorem KamProject.Arnold1963.Iteration.InitialData.orbit_eq_of_initial_eq {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) {p p' : RealSpace n} (hp : p ∈ realSlice (limitDomain b h)) (hp' : p' ∈ realSlice (limitDomain b h)) (q q' : RealSpace n) (he : orbit b h p q 0 = orbit b h p' q' 0) : orbit b h p q = orbit b h p' q'