Intersecting tori from different charts coincide by uniqueness of the original Hamiltonian trajectory and density of its orbit. The global family removes duplicate sets, retaining distinct branches that can have the same frequency.
theorem
KamProject.Arnold1963.FiniteLocalization.tori_eq_of_intersection
{n : ℕ}
{H₀ : ComplexSpace n → ℂ}
{ambient : Set (ComplexSpace n)}
{ρ : NNReal}
{κ : ℝ}
(L : FiniteLocalization n H₀ ambient ρ κ)
(f : AnalyticPhaseFunction n ambient ρ)
(hf : f.uniformNorm ≤ L.threshold)
(c d : ↥L.patches)
{p p' : RealSpace n}
(hp : p ∈ realSlice (Iteration.InitialData.limitDomain ⋯ (L.data f hf c)))
(hp' : p' ∈ realSlice (Iteration.InitialData.limitDomain ⋯ (L.data f hf d)))
{z : RealPhaseSpace n}
(hz : z ∈ Iteration.InitialData.invariantTorus ⋯ (L.data f hf c) p)
(hz' : z ∈ Iteration.InitialData.invariantTorus ⋯ (L.data f hf d) p')
:
Iteration.InitialData.invariantTorus ⋯ (L.data f hf c) p = Iteration.InitialData.invariantTorus ⋯ (L.data f hf d) p'
def
KamProject.Arnold1963.FiniteLocalization.tori
{n : ℕ}
{H₀ : ComplexSpace n → ℂ}
{ambient : Set (ComplexSpace n)}
{ρ : NNReal}
{κ : ℝ}
(L : FiniteLocalization n H₀ ambient ρ κ)
(f : AnalyticPhaseFunction n ambient ρ)
(hf : f.uniformNorm ≤ L.threshold)
:
Set (Set (RealPhaseSpace n))
The invariant torus sets realized by all retained labels in the finite patch collection.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
KamProject.Arnold1963.FiniteLocalization.tori_pairwise_disjoint
{n : ℕ}
{H₀ : ComplexSpace n → ℂ}
{ambient : Set (ComplexSpace n)}
{ρ : NNReal}
{κ : ℝ}
(L : FiniteLocalization n H₀ ambient ρ κ)
(f : AnalyticPhaseFunction n ambient ρ)
(hf : f.uniformNorm ≤ L.threshold)
:
theorem
KamProject.Arnold1963.FiniteLocalization.goodSet_eq_sUnion_tori
{n : ℕ}
{H₀ : ComplexSpace n → ℂ}
{ambient : Set (ComplexSpace n)}
{ρ : NNReal}
{κ : ℝ}
(L : FiniteLocalization n H₀ ambient ρ κ)
(f : AnalyticPhaseFunction n ambient ρ)
(hf : f.uniformNorm ≤ L.threshold)
: