Pass the conjugacy to the limit and construct solutions of the original Hamiltonian equation for every real time.
theorem
KamProject.Arnold1963.Iteration.InitialData.limit_conjugacy_complex
{n : ℕ}
{Ω₀ : Set (ComplexSpace n)}
{δ₁ θ₀ Θ₀ ρ₀ : NNReal}
{κ D : ℝ}
(b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D)
(h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D)
{p : ComplexSpace n}
(hp : p ∈ limitDomain b h)
{q : ComplexSpace n}
{t : ℂ}
(ht : t ∈ lineDomain q (limitFrequency b h p))
:
HasDerivAt (fun (u : ℂ) => limitMap b h (p, q + u • limitFrequency b h p))
(vectorField b h 0 (limitMap b h (p, q + t • limitFrequency b h p))) t
theorem
KamProject.Arnold1963.Iteration.InitialData.real_time_mem_lineDomain
{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)
(t : ℝ)
:
noncomputable def
KamProject.Arnold1963.Iteration.InitialData.orbit
{n : ℕ}
{Ω₀ : Set (ComplexSpace n)}
{δ₁ θ₀ Θ₀ ρ₀ : NNReal}
{κ D : ℝ}
(b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D)
(h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D)
(p q : RealSpace n)
(t : ℝ)
:
The limiting phase transformation applied to uniform rotation with the limiting frequency.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
KamProject.Arnold1963.Iteration.InitialData.orbit_hasDerivAt
{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)
(t : ℝ)
:
HasDerivAt (orbit b h p q) (vectorField b h 0 (orbit b h p q t)) t
theorem
KamProject.Arnold1963.Iteration.InitialData.orbit_mem_initial
{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)
(t : ℝ)
:
theorem
KamProject.Arnold1963.Iteration.InitialData.orbit_initial
{n : ℕ}
{Ω₀ : Set (ComplexSpace n)}
{δ₁ θ₀ Θ₀ ρ₀ : NNReal}
{κ D : ℝ}
(b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D)
(h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D)
(p q : RealSpace n)
: