Constants and positive thresholds for the corrected analytic iteration. The iteration exponent is 8 * n + 24. Explicit identities verify the exponent balance in the remainder recurrence.

def KamProject.Arnold1963.arithmeticExponent (n : ℕ) : ℕ

The small-divisor exponent used for arithmetic resonance bounds.

Equations

• KamProject.Arnold1963.arithmeticExponent n = n + 1

def KamProject.Arnold1963.homologicalExponent (n : ℕ) : ℕ

The dimension-dependent exponent in the homological equation estimates.

Equations

• KamProject.Arnold1963.homologicalExponent n = 2 * n + 1

def KamProject.Arnold1963.stepExponent (n : ℕ) : ℕ

The exponent governing the nonlinear remainder bound of one KAM step.

Equations

• KamProject.Arnold1963.stepExponent n = 2 * n + 3

def KamProject.Arnold1963.iterationExponent (n : ℕ) : ℕ

The initial perturbation exponent chosen to sustain the full iteration.

Equations

• KamProject.Arnold1963.iterationExponent n = 8 * n + 24

noncomputable def KamProject.Arnold1963.constantL0 (n : ℕ) : ℝ

The exponential coefficient used in dimension-dependent KAM estimates.

Equations

• KamProject.Arnold1963.constantL0 n = ((↑n + 1) / Real.exp 1) ^ (n + 1)

noncomputable def KamProject.Arnold1963.constantL5 (n : ℕ) : ℝ

The dimension-dependent coefficient used to bound the homological solution.

Equations

• KamProject.Arnold1963.constantL5 n = 4 ^ n * KamProject.Arnold1963.constantL0 n

noncomputable def KamProject.Arnold1963.constantL2 (n : ℕ) : ℝ

The numerical coefficient entering the first smallness threshold.

Equations

• KamProject.Arnold1963.constantL2 n = 16 * ↑n * KamProject.Arnold1963.constantL5 n

noncomputable def KamProject.Arnold1963.constantL3 (n : ℕ) : ℝ

The numerical coefficient entering the quadratic remainder estimate.

Equations

• KamProject.Arnold1963.constantL3 n = 1 / 2 * ↑n ^ 2 * KamProject.Arnold1963.constantL5 n ^ 2

noncomputable def KamProject.Arnold1963.constantL4 (n : ℕ) : ℝ

The exponential tail coefficient entering the Fourier remainder estimate.

Equations

• KamProject.Arnold1963.constantL4 n = 2 * (2 * ↑n / Real.exp 1) ^ n

noncomputable def KamProject.Arnold1963.threshold0 (n : ℕ) (Θ : ℝ) : ℝ

The common smallness bound for the fundamental step's numerical estimates.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def KamProject.Arnold1963.threshold1 (n : ℕ) (θ Θ : ℝ) : ℝ

The fundamental smallness bound adjusted for frequency-chart derivative bounds.

Equations

• KamProject.Arnold1963.threshold1 n θ Θ = min (KamProject.Arnold1963.threshold0 n (2 * Θ)) (θ / (2 * ↑n))

noncomputable def KamProject.Arnold1963.threshold2 (n : ℕ) (κ ρ : ℝ) : ℝ

The smallness bound controlling strip widths and the requested measure tolerance.

Equations

• KamProject.Arnold1963.threshold2 n κ ρ = min ((10 ^ (4 * n))⁻¹ * ρ ^ (4 * n)) (min (4 ^ (4 * n))⁻¹ κ)

noncomputable def KamProject.Arnold1963.threshold3 (n : ℕ) (θ Θ κ D : ℝ) : ℝ

The smallness bound controlling frequency-domain losses and their measure budget.

Equations

• KamProject.Arnold1963.threshold3 n θ Θ κ D = min (Real.exp (2 * ↑n) / (32 * ↑n ^ 2 + 100 * ↑n) ^ (2 * n)) (min (1 / (6 + 14 * Θ)) ((4 ^ (n + 2))⁻¹ * κ * θ ^ n / (Θ ^ n * D * ↑n)))

noncomputable def KamProject.Arnold1963.threshold4 (κ θ : ℝ) : ℝ

The smallness bound balancing the measure tolerance with the lower derivative bound.

Equations

• KamProject.Arnold1963.threshold4 κ θ = κ / (2 + θ⁻¹)

noncomputable def KamProject.Arnold1963.threshold5 (n : ℕ) (θ Θ ρ κ D : ℝ) : ℝ

The common initial smallness bound combining all iteration constraints.

Equations

• One or more equations did not get rendered due to their size.

theorem KamProject.Arnold1963.constants_pos {n : ℕ} (hn : 0 < n) : 0 < constantL0 n ∧ 0 < constantL5 n ∧ 0 < constantL2 n ∧ 0 < constantL3 n ∧ 0 < constantL4 n

theorem KamProject.Arnold1963.threshold0_pos {n : ℕ} (hn : 0 < n) {Θ : ℝ} (hΘ : 0 < Θ) : 0 < threshold0 n Θ

theorem KamProject.Arnold1963.threshold1_pos {n : ℕ} (hn : 0 < n) {θ Θ : ℝ} (hθ : 0 < θ) (hΘ : 0 < Θ) : 0 < threshold1 n θ Θ

theorem KamProject.Arnold1963.threshold0_bounds {n : ℕ} {Θ δ : ℝ} (h : δ < threshold0 n Θ) : δ < 1 / 12 ∧ δ < (constantL2 n)⁻¹ ∧ δ < (constantL3 n)⁻¹ * Θ⁻¹ ∧ δ < (constantL4 n)⁻¹

theorem KamProject.Arnold1963.threshold0_budget_conditions {n : ℕ} (hn : 0 < n) {Θ δ : ℝ} (hΘ : 0 < Θ) (hδ : δ < threshold0 n Θ) : δ < 1 / 12 ∧ δ * constantL2 n < 1 ∧ δ * (constantL3 n * Θ) < 1 ∧ δ * constantL4 n < 1

theorem KamProject.Arnold1963.threshold1_bounds {n : ℕ} {θ Θ δ : ℝ} (h : δ < threshold1 n θ Θ) : δ < threshold0 n (2 * Θ) ∧ δ < θ / (2 * ↑n)

theorem KamProject.Arnold1963.threshold5_bounds {n : ℕ} {θ Θ ρ κ D δ : ℝ} (h : δ < threshold5 n θ Θ ρ κ D) : δ < threshold1 n (θ / 2) (2 * Θ) ∧ δ < threshold2 n κ ρ ∧ δ < threshold3 n θ Θ κ D ∧ δ < threshold4 κ θ

theorem KamProject.Arnold1963.threshold2_pos (n : ℕ) {κ ρ : ℝ} (hκ : 0 < κ) (hρ : 0 < ρ) : 0 < threshold2 n κ ρ

theorem KamProject.Arnold1963.threshold3_pos {n : ℕ} (hn : 0 < n) {θ Θ κ D : ℝ} (hθ : 0 < θ) (hΘ : 0 < Θ) (hκ : 0 < κ) (hD : 0 < D) : 0 < threshold3 n θ Θ κ D

theorem KamProject.Arnold1963.threshold4_pos {κ θ : ℝ} (hκ : 0 < κ) (hθ : 0 < θ) : 0 < threshold4 κ θ

theorem KamProject.Arnold1963.threshold5_pos {n : ℕ} (hn : 0 < n) {θ Θ ρ κ D : ℝ} (hθ : 0 < θ) (hΘ : 0 < Θ) (hρ : 0 < ρ) (hκ : 0 < κ) (hD : 0 < D) : 0 < threshold5 n θ Θ ρ κ D

noncomputable def KamProject.Arnold1963.initialPerturbationThreshold (n : ℕ) (θ Θ ρ κ D : ℝ) : ℝ

The perturbation threshold obtained from the initial smallness bound and iteration exponent.

Equations

• KamProject.Arnold1963.initialPerturbationThreshold n θ Θ ρ κ D = (KamProject.Arnold1963.threshold5 n θ Θ ρ κ D / 2) ^ KamProject.Arnold1963.iterationExponent n

theorem KamProject.Arnold1963.initialPerturbationThreshold_pos {n : ℕ} (hn : 0 < n) {θ Θ ρ κ D : ℝ} (hθ : 0 < θ) (hΘ : 0 < Θ) (hρ : 0 < ρ) (hκ : 0 < κ) (hD : 0 < D) : 0 < initialPerturbationThreshold n θ Θ ρ κ D

theorem KamProject.Arnold1963.strengthened_budget_two_mul (M δ β : ℝ) (n : ℕ) : 1 / 4 * (2 * M) ^ 2 / (δ ^ (2 * stepExponent n) * β ^ 2) = M ^ 2 / (δ ^ (2 * stepExponent n) * β ^ 2)

theorem KamProject.Arnold1963.budget_exponent_identity (n : ℕ) : 2 * iterationExponent n = 2 * stepExponent n + 6 + (12 * n + 36)

theorem KamProject.Arnold1963.budget_step_eq {δ : ℝ} (hδ : 0 < δ) (n : ℕ) : (δ ^ iterationExponent n) ^ 2 / (δ ^ (2 * stepExponent n) * (δ ^ 3) ^ 2) = δ ^ (12 * n + 36)