Actual Hamiltonian vector fields at each stage, their conjugacies, and vanishing error bounds.

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

The Hamiltonian vector field at the specified iteration stage.

Equations

• KamProject.Arnold1963.Iteration.InitialData.vectorField b h s = KamProject.Arnold1963.hamiltonianVectorField (KamProject.Arnold1963.Iteration.InitialData.hamiltonian b h s)

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

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

theorem KamProject.Arnold1963.Iteration.InitialData.vectorField_split {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) (s : ℕ) {z : ComplexPhaseSpace n} (hz : z ∈ phase b h s) : vectorField b h s z = (0, frequency b h s z.1) + hamiltonianVectorField (state b h s).perturbation.toFun z

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

theorem KamProject.Arnold1963.Iteration.InitialData.vectorField_limit_error {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) (s : ℕ) {z : ComplexPhaseSpace n} (hz : z ∈ limitPhase b h) : ‖vectorField b h (s + 1) z - (0, limitFrequency b h z.1)‖ < ↑(beta δ₁ (s + 1))

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