Joint multivariable angle analyticity for each retained action label on a common complex strip. The result makes no ambient analyticity claim in the Cantor action-label variable.

def KamProject.Arnold1963.Iteration.InitialData.commonAngleStrip (n : ℕ) (ρ : NNReal) : Set (ComplexSpace n)

The open angle strip retained uniformly throughout the iteration.

Equations

• KamProject.Arnold1963.Iteration.InitialData.commonAngleStrip n ρ = {q : KamProject.Arnold1963.ComplexSpace n | ‖KamProject.Arnold1963.imagPart q‖ < ↑ρ / 3}

theorem KamProject.Arnold1963.Iteration.InitialData.commonAngleStrip_open {n : ℕ} {ρ₀ : NNReal} : IsOpen (commonAngleStrip n ρ₀)

theorem KamProject.Arnold1963.Iteration.InitialData.angle_mem_limitPhase {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} (hq : q ∈ commonAngleStrip n ρ₀) : (p, q) ∈ limitPhase b h

theorem KamProject.Arnold1963.Iteration.InitialData.angle_uniform {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) {p : ComplexSpace n} (hp : p ∈ limitDomain b h) : TendstoUniformlyOn (fun (s : ℕ) (q : ComplexSpace n) => cumulative b h s (p, q)) (fun (q : ComplexSpace n) => limitMap b h (p, q)) Filter.atTop (commonAngleStrip n ρ₀)

theorem KamProject.Arnold1963.Iteration.InitialData.cumulative_angle_analytic {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) {p : ComplexSpace n} (hp : p ∈ limitDomain b h) (s : ℕ) : AnalyticOnNhd ℂ (fun (q : ComplexSpace n) => cumulative b h s (p, q)) (commonAngleStrip n ρ₀)

theorem KamProject.Arnold1963.Iteration.InitialData.limitMap_angle_scalar_analytic {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) {p : ComplexSpace n} (hp : p ∈ limitDomain b h) (L : ComplexPhaseSpace n →L[ℂ] ℂ) : AnalyticOnNhd ℂ (fun (q : ComplexSpace n) => L (limitMap b h (p, q))) (commonAngleStrip n ρ₀)

theorem KamProject.Arnold1963.Iteration.InitialData.limitMap_angle_analytic {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) {p : ComplexSpace n} (hp : p ∈ limitDomain b h) : AnalyticOnNhd ℂ (fun (q : ComplexSpace n) => limitMap b h (p, q)) (commonAngleStrip n ρ₀)