Explicit decay sequences for the corrected iteration. States are indexed from zero; their small parameters correspond to the next paper step. The recurrence uses the exponent 3 / 2.

noncomputable def KamProject.Arnold1963.Iteration.decay (x : NNReal) (s : ℕ) : NNReal

Superexponential decay with exponent (3/2)^s.

Equations

• KamProject.Arnold1963.Iteration.decay x s = x ^ (3 / 2) ^ s

@[simp]

theorem KamProject.Arnold1963.Iteration.decay_zero (x : NNReal) : decay x 0 = x

theorem KamProject.Arnold1963.Iteration.decay_succ (x : NNReal) (s : ℕ) : decay x (s + 1) = decay x s ^ (3 / 2)

theorem KamProject.Arnold1963.Iteration.decay_pos {x : NNReal} (hx : 0 < x) (s : ℕ) : 0 < decay x s

theorem KamProject.Arnold1963.Iteration.decay_add (x : NNReal) (s t : ℕ) : decay x (s + t) = decay (decay x s) t

theorem KamProject.Arnold1963.Iteration.coe_decay_succ (x : NNReal) (s : ℕ) : ↑(decay x (s + 1)) = ↑(decay x s) * √↑(decay x s)

theorem KamProject.Arnold1963.Iteration.decay_le {x : NNReal} (hx : x ≤ 1) (s : ℕ) : decay x s ≤ x

theorem KamProject.Arnold1963.Iteration.decay_half {x : NNReal} (hx : x ≤ 1 / 4) (s : ℕ) : ↑(decay x (s + 1)) ≤ ↑(decay x s) / 2

theorem KamProject.Arnold1963.Iteration.decay_geometric {x : NNReal} (hx : x ≤ 1 / 4) (s : ℕ) : ↑(decay x s) ≤ ↑x * (1 / 2) ^ s

theorem KamProject.Arnold1963.Iteration.decay_summable {x : NNReal} (hx : x ≤ 1 / 4) : Summable fun (s : ℕ) => ↑(decay x s)

theorem KamProject.Arnold1963.Iteration.decay_tsum_le {x : NNReal} (hx : x ≤ 1 / 4) : ∑' (s : ℕ), ↑(decay x s) ≤ 2 * ↑x

theorem KamProject.Arnold1963.Iteration.decay_sum_le {x : NNReal} (hx : x ≤ 1 / 4) (s : ℕ) : ∑ j ∈ Finset.range s, ↑(decay x j) ≤ 2 * ↑x

theorem KamProject.Arnold1963.Iteration.decay_tail_le {x : NNReal} (hx : x ≤ 1 / 4) (s : ℕ) : ∑' (j : ℕ), ↑(decay x (s + j)) ≤ 2 * ↑(decay x s)

noncomputable def KamProject.Arnold1963.Iteration.delta (δ₁ : NNReal) (s : ℕ) : NNReal

The stage's smallness parameter along the superexponential decay sequence.

Equations

• KamProject.Arnold1963.Iteration.delta δ₁ s = KamProject.Arnold1963.Iteration.decay δ₁ s

noncomputable def KamProject.Arnold1963.Iteration.beta (δ₁ : NNReal) (s : ℕ) : NNReal

The cubic smallness scale used for displacement and action-domain erosion.

Equations

• KamProject.Arnold1963.Iteration.beta δ₁ s = KamProject.Arnold1963.Iteration.delta δ₁ s ^ 3

noncomputable def KamProject.Arnold1963.Iteration.gamma (n : ℕ) (δ₁ : NNReal) (s : ℕ) : NNReal

The stage's strip-loss scale derived from the initial smallness parameter.

Equations

• KamProject.Arnold1963.Iteration.gamma n δ₁ s = KamProject.Arnold1963.Iteration.decay (δ₁ ^ (1 / (4 * ↑n))) s

noncomputable def KamProject.Arnold1963.Iteration.perturbation (n : ℕ) (δ₁ : NNReal) (s : ℕ) : ℝ

The stage's perturbation bound chosen with the iteration exponent.

Equations

• KamProject.Arnold1963.Iteration.perturbation n δ₁ s = ↑(KamProject.Arnold1963.Iteration.delta δ₁ s) ^ KamProject.Arnold1963.iterationExponent n

theorem KamProject.Arnold1963.Iteration.gamma_eq (n : ℕ) (δ₁ : NNReal) (s : ℕ) : gamma n δ₁ s = delta δ₁ s ^ (1 / (4 * ↑n))

theorem KamProject.Arnold1963.Iteration.gamma_pow {n : ℕ} (hn : 0 < n) (δ₁ : NNReal) (s : ℕ) : gamma n δ₁ s ^ (4 * n) = delta δ₁ s

theorem KamProject.Arnold1963.Iteration.gamma_initial_bounds {n : ℕ} (hn : 0 < n) {δ₁ ρ₀ : NNReal} {κ : ℝ} (hδ : ↑δ₁ < threshold2 n κ ↑ρ₀) : ↑(gamma n δ₁ 0) < ↑ρ₀ / 10 ∧ ↑(gamma n δ₁ 0) < 1 / 4

theorem KamProject.Arnold1963.Iteration.delta_initial_lt_quarter {n : ℕ} {θ Θ ρ κ D : ℝ} {δ₁ : NNReal} (hδ : ↑δ₁ < threshold5 n θ Θ ρ κ D) : δ₁ < 1 / 4

theorem KamProject.Arnold1963.Iteration.remainder_eq_next {δ₁ : NNReal} (hδ : 0 < δ₁) (n s : ℕ) : perturbation n δ₁ s ^ 2 / (↑(delta δ₁ s) ^ (2 * stepExponent n) * ↑(beta δ₁ s) ^ 2) = perturbation n δ₁ (s + 1)