First and second derivative budgets for the next perturbation.

theorem KamProject.Arnold1963.Iteration.InitialParameters.next_perturbation_power {n : ℕ} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (s : ℕ) : perturbation n δ₁ (s + 1) = ↑(delta δ₁ s) ^ (12 * n + 36)

theorem KamProject.Arnold1963.Iteration.InitialParameters.beta_next_lower {n : ℕ} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (s : ℕ) : ↑(delta δ₁ s) ^ 6 ≤ ↑(beta δ₁ (s + 1))

theorem KamProject.Arnold1963.Iteration.InitialParameters.first_derivative_budget {n : ℕ} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (s : ℕ) : perturbation n δ₁ (s + 1) / ↑(beta δ₁ s) < ↑(delta δ₁ s) * ↑(beta δ₁ (s + 1))

theorem KamProject.Arnold1963.Iteration.InitialParameters.second_derivative_budget {n : ℕ} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (s : ℕ) : 2 * perturbation n δ₁ (s + 1) / ↑(beta δ₁ s) ^ 2 < ↑(delta δ₁ s)