Uniform domain buffers, transformation estimates, and derivative bounds for the actual states.

theorem KamProject.Arnold1963.Iteration.InitialData.phase_succ {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) (s : ℕ) : phase b h (s + 1) = phaseDomain (state b h s).step.domain (width n ρ₀ δ₁ s - 3 * gamma n δ₁ s)

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

theorem KamProject.Arnold1963.Iteration.InitialData.displacement_lt {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)) : ‖(transformation b h s).toFun z - z‖ < ↑(beta δ₁ s)

theorem KamProject.Arnold1963.Iteration.InitialData.transformation_periodic {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)) (k : FourierIndex n) : (transformation b h s).toFun (phaseShift k z) = phaseShift k ((transformation b h s).toFun z)

theorem KamProject.Arnold1963.Iteration.InitialData.transformation_real {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)) : (transformation b h s).toFun (conjPhase z) = conjPhase ((transformation b h s).toFun z)

theorem KamProject.Arnold1963.Iteration.InitialData.width_gt_third {n : ℕ} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (s : ℕ) : ↑ρ₀ / 3 < ↑(width n ρ₀ δ₁ s)

theorem KamProject.Arnold1963.Iteration.InitialData.remainder_derivative {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)) : ‖fderiv ℂ (state b h (s + 1)).perturbation.toFun z‖ < ↑(delta δ₁ s) * ↑(beta δ₁ (s + 1))

theorem KamProject.Arnold1963.Iteration.InitialData.remainder_coordinate_derivative {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)) (j : Fin n ⊕ Fin n) : ‖(fderiv ℂ (state b h (s + 1)).perturbation.toFun z) (phaseBasis j)‖ < ↑(delta δ₁ s) * ↑(beta δ₁ (s + 1))

theorem KamProject.Arnold1963.Iteration.InitialData.remainder_second_derivative {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)) (j k : Fin n ⊕ Fin n) : ‖((fderiv ℂ (fderiv ℂ (state b h (s + 1)).perturbation.toFun) z) (phaseBasis j)) (phaseBasis k)‖ < ↑(delta δ₁ s)

theorem KamProject.Arnold1963.Iteration.InitialData.frequency_bounds {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) (s : ℕ) {p : ComplexSpace n} (hp : p ∈ actionDomain b h s) (v : ComplexSpace n) : ↑θ₀ / 2 * ‖v‖ ≤ ‖(fderiv ℂ (actionFrequency (state b h s).integrable) p) v‖ ∧ ‖(fderiv ℂ (actionFrequency (state b h s).integrable) p) v‖ ≤ 2 * ↑Θ₀ * ‖v‖

theorem KamProject.Arnold1963.Iteration.InitialData.frequency_displacement {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) (s : ℕ) {p : ComplexSpace n} (hp : p ∈ actionDomain b h (s + 1)) : ‖actionFrequency (state b h (s + 1)).integrable p - actionFrequency (state b h s).integrable p‖ < ↑(beta δ₁ s) * ↑(delta δ₁ s)