Supporting results for the analytic Hamiltonian KAM construction.

noncomputable def KamProject.Arnold1963.fundamentalCutoff (γ M : ℝ) : ℝ

The logarithmic Fourier cutoff balancing strip loss and perturbation size.

Equations

• KamProject.Arnold1963.fundamentalCutoff γ M = Real.log (1 / M) / γ

noncomputable def KamProject.Arnold1963.fundamentalRemainderBound (n : ℕ) (M δ β : ℝ) : ℝ

The strict quadratic remainder target used in the fundamental step.

Equations

• KamProject.Arnold1963.fundamentalRemainderBound n M δ β = 1 / 4 * M ^ 2 / (δ ^ (2 * KamProject.Arnold1963.stepExponent n) * β ^ 2)

theorem KamProject.Arnold1963.fundamentalRemainderBound_twice (n : ℕ) (M δ β : ℝ) : fundamentalRemainderBound n (2 * M) δ β = M ^ 2 / (δ ^ (2 * stepExponent n) * β ^ 2)

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

The positive parameters and numerical constraints required by the fundamental step.

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

theorem KamProject.Arnold1963.FundamentalParameters.gamma_pos {n : ℕ} {ρ β δ γ : NNReal} {K M Θ : ℝ} (b : FundamentalParameters n ρ β δ γ K M Θ) : 0 < γ

theorem KamProject.Arnold1963.FundamentalParameters.K_pos {n : ℕ} {ρ β δ γ : NNReal} {K M Θ : ℝ} (b : FundamentalParameters n ρ β δ γ K M Θ) : 0 < K

theorem KamProject.Arnold1963.FundamentalParameters.delta_lt {n : ℕ} {ρ β δ γ : NNReal} {K M Θ : ℝ} (b : FundamentalParameters n ρ β δ γ K M Θ) : ↑δ < 1 / 12

theorem KamProject.Arnold1963.FundamentalParameters.double_delta_le {n : ℕ} {ρ β δ γ : NNReal} {K M Θ : ℝ} (b : FundamentalParameters n ρ β δ γ K M Θ) : δ + δ ≤ ρ

theorem KamProject.Arnold1963.FundamentalParameters.exp_cutoff {n : ℕ} {ρ β δ γ : NNReal} {K M Θ : ℝ} (b : FundamentalParameters n ρ β δ γ K M Θ) : Real.exp (-fundamentalCutoff (↑γ) M * ↑γ) = M

theorem KamProject.Arnold1963.FundamentalParameters.generating_bound_lt {n : ℕ} {ρ β δ γ : NNReal} {K M Θ : ℝ} (b : FundamentalParameters n ρ β δ γ K M Θ) : homologicalBound n M K ↑δ < 2 * constantL5 n * ↑δ ^ 2 * ↑β ^ 2

theorem KamProject.Arnold1963.FundamentalParameters.generating_small {n : ℕ} {ρ β δ γ : NNReal} {K M Θ : ℝ} (b : FundamentalParameters n ρ β δ γ K M Θ) : homologicalBound n M K ↑δ < ↑β ^ 2 / (16 * ↑n)

theorem KamProject.Arnold1963.FundamentalParameters.generating_lt_beta_sq {n : ℕ} {ρ β δ γ : NNReal} {K M Θ : ℝ} (b : FundamentalParameters n ρ β δ γ K M Θ) : homologicalBound n M K ↑δ < ↑β ^ 2

theorem KamProject.Arnold1963.FundamentalParameters.displacement_lt_beta {n : ℕ} {ρ β δ γ : NNReal} {K M Θ : ℝ} (b : FundamentalParameters n ρ β δ γ K M Θ) : homologicalBound n M K ↑δ / ↑β < ↑β

theorem KamProject.Arnold1963.FundamentalParameters.remainder_budget {n : ℕ} {ρ β δ γ : NNReal} {K M Θ : ℝ} (b : FundamentalParameters n ρ β δ γ K M Θ) : 1 / 2 * ↑n ^ 2 * Θ * (homologicalBound n M K ↑δ / ↑δ) ^ 2 + (2 * ↑n / Real.exp 1) ^ n * M ^ 2 / ↑δ ^ (n + 1) + ↑n * M / ↑β * (homologicalBound n M K ↑δ / ↑δ) < fundamentalRemainderBound n M ↑δ ↑β