Frequency relabeling of the same limit transformation. The unperturbed center is selected through the original inverse frequency chart; action and angle corrections retain their bounds.

theorem KamProject.Arnold1963.Iteration.InitialParameters.torus_displacement_budget {n : ℕ} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) : ↑(beta δ₁ 0) * (2 + (↑θ₀)⁻¹) < κ

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

The limiting action displacement from the corresponding original action center.

Equations

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

theorem KamProject.Arnold1963.Iteration.InitialData.parameterization_eq {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) (p q : ComplexSpace n) : limitMap b h (p, q) = (h.unperturbedCenter (limitFrequency b h p) + actionCorrection b h p q, q + angleCorrection b h p q)

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

theorem KamProject.Arnold1963.Iteration.InitialData.torusCorrections_small {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 ρ₀) : ‖actionCorrection b h p q‖ < κ ∧ ‖angleCorrection b h p q‖ < κ

theorem KamProject.Arnold1963.Iteration.InitialData.torusCorrections_periodic {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 ρ₀) (k : FourierIndex n) : actionCorrection b h p (q + angleShift k) = actionCorrection b h p q ∧ angleCorrection b h p (q + angleShift k) = angleCorrection b h p q

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

The limiting frequencies corresponding to retained real action labels.

Equations

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

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

The real action label associated with a retained limiting frequency.

Equations

• KamProject.Arnold1963.Iteration.InitialData.realFrequencyLabel b h ω = KamProject.Arnold1963.realPart (KamProject.Arnold1963.Iteration.InitialData.frequencyLabel b h ω)

theorem KamProject.Arnold1963.Iteration.InitialData.realFrequencyLabel_spec {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) {ω : ComplexSpace n} (hω : ω ∈ retainedRealFrequencies b h) : realFrequencyLabel b h ω ∈ realSlice (limitDomain b h) ∧ limitFrequency b h (complexify (realFrequencyLabel b h ω)) = ω ∧ complexify (realFrequencyLabel b h ω) = frequencyLabel b h ω

theorem KamProject.Arnold1963.Iteration.InitialData.retainedRealFrequency_real {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) {ω : ComplexSpace n} (hω : ω ∈ retainedRealFrequencies b h) : complexify (realPart ω) = ω

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

theorem KamProject.Arnold1963.Iteration.InitialData.unperturbedCenter_real {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) {p : RealSpace n} (hp : p ∈ realSlice (limitDomain b h)) : complexify (realPart (h.unperturbedCenter (limitFrequency b h (complexify p)))) = h.unperturbedCenter (limitFrequency b h (complexify p))

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

The limiting torus lift expressed in frequency coordinates rather than action labels.

Equations

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

theorem KamProject.Arnold1963.Iteration.InitialData.frequencyParameterization_eq {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) {ω : ComplexSpace n} (hω : ω ∈ retainedRealFrequencies b h) (q : ComplexSpace n) : frequencyParameterization b h ω q = (h.unperturbedCenter ω + actionCorrection b h (frequencyLabel b h ω) q, q + angleCorrection b h (frequencyLabel b h ω) q)