Cumulative transformation estimates. Mean-value arguments first establish segment containment in the relevant domain.

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

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

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

The intersection of all phase domains in the iteration.

Equations

• KamProject.Arnold1963.Iteration.InitialData.limitPhase b h = ⋂ (s : ℕ), KamProject.Arnold1963.Iteration.InitialData.phase b h s

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

theorem KamProject.Arnold1963.Iteration.InitialData.commonPhase_subset {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) : phaseDomain (limitDomain b h) (ρ₀ / 3) ⊆ limitPhase b h

theorem KamProject.Arnold1963.Iteration.InitialData.cumulative_analytic {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) (s : ℕ) : AnalyticOnNhd ℂ (cumulative b h s) (phase b h s)

theorem KamProject.Arnold1963.Iteration.InitialData.cumulative_derivative {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) (s : ℕ) (z : ComplexPhaseSpace n) : z ∈ phase b h s → ‖fderiv ℂ (cumulative b h s) z‖ ≤ 2 ^ s

theorem KamProject.Arnold1963.Iteration.InitialData.cumulative_canonical {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) (s : ℕ) : CanonicalOn (cumulative b h s) (phase b h s)

theorem KamProject.Arnold1963.Iteration.InitialData.cumulative_injOn {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) (s : ℕ) : Set.InjOn (cumulative b h s) (phase b h s)

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

theorem KamProject.Arnold1963.Iteration.InitialData.cumulative_periodic {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) (s : ℕ) (z : ComplexPhaseSpace n) : z ∈ phase b h s → ∀ (k : FourierIndex n), cumulative b h s (phaseShift k z) = phaseShift k (cumulative b h s z)

theorem KamProject.Arnold1963.Iteration.InitialData.cumulative_real {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) (s : ℕ) (z : ComplexPhaseSpace n) : z ∈ phase b h s → cumulative b h s (conjPhase z) = conjPhase (cumulative b h s z)

theorem KamProject.Arnold1963.Iteration.InitialData.limitPhase_shift {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) : phaseShift k z ∈ limitPhase b h

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