Real limit maps, quotient maps, and actual invariant trajectories on the angle torus.

noncomputable def KamProject.Arnold1963.Iteration.InitialData.realLimitMap {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) (x : RealPhaseCover n) : RealPhaseCover n

The real-coordinate restriction of the limiting phase transformation.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def KamProject.Arnold1963.Iteration.InitialData.torusLimitMap {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) (x : RealPhaseSpace n) : RealPhaseSpace n

The limiting phase transformation descended to real angles modulo 2π.

Equations

• One or more equations did not get rendered due to their size.

theorem KamProject.Arnold1963.Iteration.InitialData.realLimitMap_shift {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) {x : RealPhaseCover n} (hx : x.1 ∈ realSlice (limitDomain b h)) (k : FourierIndex n) : realLimitMap b h (realPhaseShift k x) = realPhaseShift k (realLimitMap b h x)

theorem KamProject.Arnold1963.Iteration.InitialData.torusLimitMap_projection {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) {x : RealPhaseCover n} (hx : x.1 ∈ realSlice (limitDomain b h)) : torusLimitMap b h (torusProjection x) = torusProjection (realLimitMap b h x)

theorem KamProject.Arnold1963.Iteration.InitialData.realLimitMap_maps {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) {x : RealPhaseCover n} (hx : x.1 ∈ realSlice (limitDomain b h)) : (realLimitMap b h x).1 ∈ realSlice h.domain

theorem KamProject.Arnold1963.Iteration.InitialData.torusLimitMap_maps {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) : Set.MapsTo (torusLimitMap b h) (realSlice (limitDomain b h) ×ˢ Set.univ) (realSlice h.domain ×ˢ Set.univ)

theorem KamProject.Arnold1963.Iteration.InitialData.orbit_eq_real_angle {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 : ℝ) : orbit b h p q t = limitMap b h (complexifyPhase (p, q + t • realPart (limitFrequency b h (complexify p))))

theorem KamProject.Arnold1963.Iteration.InitialData.orbit_real_value {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 : ℝ) : complexifyPhase (realPartPhase (orbit b h p q t)) = orbit b h p q t

theorem KamProject.Arnold1963.Iteration.InitialData.orbit_mem_torus_image {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 : ℝ) : torusProjection (realPartPhase (orbit b h p q t)) ∈ torusLimitMap b h '' {p} ×ˢ Set.univ