Disjointness of invariant tori from ODE uniqueness, bounded angle corrections, and frequency injectivity within a single chart.
theorem
KamProject.Arnold1963.eq_zero_of_bounded_affine_line
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{u v : E}
{C : ℝ}
(hb : ∀ (t : ℝ), ‖u + t • v‖ ≤ C)
:
theorem
KamProject.Arnold1963.Iteration.InitialData.frequency_eq_of_orbit_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 = orbit b h p' q')
:
theorem
KamProject.Arnold1963.Iteration.InitialData.realLimitMap_injOn
{n : ℕ}
{Ω₀ : Set (ComplexSpace n)}
{δ₁ θ₀ Θ₀ ρ₀ : NNReal}
{κ D : ℝ}
(b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D)
(h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D)
:
Set.InjOn (realLimitMap b h) (realSlice (limitDomain b h) ×ˢ Set.univ)
theorem
KamProject.Arnold1963.Iteration.InitialData.torusLimitMap_injOn
{n : ℕ}
{Ω₀ : Set (ComplexSpace n)}
{δ₁ θ₀ Θ₀ ρ₀ : NNReal}
{κ D : ℝ}
(b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D)
(h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D)
:
Set.InjOn (torusLimitMap b h) (realSlice (limitDomain b h) ×ˢ Set.univ)
def
KamProject.Arnold1963.Iteration.InitialData.invariantTorus
{n : ℕ}
{Ω₀ : Set (ComplexSpace n)}
{δ₁ θ₀ Θ₀ ρ₀ : NNReal}
{κ D : ℝ}
(b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D)
(h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D)
(p : RealSpace n)
:
Set (RealPhaseSpace n)
The image of one retained action label and the full real angle torus.
Equations
Instances For
theorem
KamProject.Arnold1963.Iteration.InitialData.invariantTorus_disjoint
{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))
(hne : p ≠ p')
:
Disjoint (invariantTorus b h p) (invariantTorus b h p')