Uniform convergence of actual cumulative transformations on their common domain, with periodicity, real compatibility, and displacement estimates.

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

The telescoping limit of the cumulative phase transformations.

Equations

• KamProject.Arnold1963.Iteration.InitialData.limitMap b h = KamProject.Arnold1963.Convergence.sequenceLimit (KamProject.Arnold1963.Iteration.InitialData.cumulative b h)

theorem KamProject.Arnold1963.Iteration.InitialData.cumulative_uniform {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) : TendstoUniformlyOn (cumulative b h) (limitMap b h) Filter.atTop (limitPhase b h)

theorem KamProject.Arnold1963.Iteration.InitialData.limitMap_tail {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) {z : ComplexPhaseSpace n} (hz : z ∈ limitPhase b h) (s : ℕ) : ‖limitMap b h z - cumulative b h s z‖ ≤ ∑' (j : ℕ), 2 ^ (j + s) * ↑(beta δ₁ (j + s))

theorem KamProject.Arnold1963.Iteration.InitialData.limitMap_displacement {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) {z : ComplexPhaseSpace n} (hz : z ∈ limitPhase b h) : ‖limitMap b h z - z‖ < 2 * ↑(beta δ₁ 0)

theorem KamProject.Arnold1963.Iteration.InitialData.limitMap_continuous {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) : ContinuousOn (limitMap b h) (limitPhase b h)

theorem KamProject.Arnold1963.Iteration.InitialData.limitMap_maps {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) : Set.MapsTo (limitMap b h) (limitPhase b h) (phase b h 0)

theorem KamProject.Arnold1963.Iteration.InitialData.limitMap_periodic {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) {z : ComplexPhaseSpace n} (hz : z ∈ limitPhase b h) (k : FourierIndex n) : limitMap b h (phaseShift k z) = phaseShift k (limitMap b h z)

theorem KamProject.Arnold1963.Iteration.InitialData.limitMap_real {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) {z : ComplexPhaseSpace n} (hz : z ∈ limitPhase b h) : limitMap b h (conjPhase z) = conjPhase (limitMap b h z)

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