The projected orbit closure equals the invariant torus, using nonresonant flow density.
theorem
KamProject.Arnold1963.Iteration.InitialData.projected_orbit_closure
{n : ℕ}
{Ω₀ : Set (ComplexSpace n)}
{δ₁ θ₀ Θ₀ ρ₀ : NNReal}
{κ D : ℝ}
(b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D)
(h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D)
{p : RealSpace n}
(hp : p ∈ realSlice (limitDomain b h))
(q : RealSpace n)
:
closure (Set.range fun (t : ℝ) => torusProjection (realPartPhase (orbit b h p q t))) = invariantTorus b h p