Supporting results for the analytic Hamiltonian KAM construction.

structure KamProject.Arnold1963.IterationParameters (n : ℕ) (ρ β δ γ θ Θ : NNReal) (K M : ℝ) : Prop

The positive parameters and smallness inequalities required for an inductive KAM step.

• dimension_pos : 0 < n
• beta_pos : 0 < β
• delta_pos : 0 < δ
• lower_pos : 0 < θ
• lower_lt_one : θ < 1
• upper_gt_one : 1 < Θ
• delta_small : ↑δ < threshold1 n ↑θ ↑Θ
• angle_loss : 10 * ↑δ < 2 * ↑γ
• angle_width : 3 * ↑γ < ↑ρ
• width_le_one : ρ ≤ 1
• action_loss : 3 * ↑β < 2 * ↑δ
• divisor_margin : 2 * ↑β < K
• divisor_le_one : K ≤ 1
• perturbation_pos : 0 < M
• perturbation_small : M < ↑δ ^ stepExponent n * K * ↑β ^ 2
• cutoff_gt_one : 1 < fundamentalCutoff (↑γ) (2 * M)

theorem KamProject.Arnold1963.IterationParameters.fundamental {n : ℕ} {ρ β δ γ θ Θ : NNReal} {K M : ℝ} (b : IterationParameters n ρ β δ γ θ Θ K M) : FundamentalParameters n ρ β δ γ K (2 * M) (2 * ↑Θ)

theorem KamProject.Arnold1963.IterationParameters.delta_lt_one {n : ℕ} {ρ β δ γ θ Θ : NNReal} {K M : ℝ} (b : IterationParameters n ρ β δ γ θ Θ K M) : δ < 1

theorem KamProject.Arnold1963.IterationParameters.beta_lt_gamma {n : ℕ} {ρ β δ γ θ Θ : NNReal} {K M : ℝ} (b : IterationParameters n ρ β δ γ θ Θ K M) : β < γ

theorem KamProject.Arnold1963.IterationParameters.lower_le_upper {n : ℕ} {ρ β δ γ θ Θ : NNReal} {K M : ℝ} (b : IterationParameters n ρ β δ γ θ Θ K M) : θ ≤ Θ

theorem KamProject.Arnold1963.IterationParameters.mean_gradient_small {n : ℕ} {ρ β δ γ θ Θ : NNReal} {K M : ℝ} (b : IterationParameters n ρ β δ γ θ Θ K M) : M / ↑β < ↑β * ↑δ

theorem KamProject.Arnold1963.IterationParameters.mean_hessian_small {n : ℕ} {ρ β δ γ θ Θ : NNReal} {K M : ℝ} (b : IterationParameters n ρ β δ γ θ Θ K M) : 2 * ↑n * M / ↑β ^ 2 < ↑δ * ↑θ