Uniform positive derivative and angle-width bounds for all stages of the iteration.

noncomputable def KamProject.Arnold1963.Iteration.lower (θ₀ δ₁ : NNReal) (s : ℕ) : NNReal

The lower frequency-derivative bound after the accumulated multiplicative losses.

Equations

• KamProject.Arnold1963.Iteration.lower θ₀ δ₁ s = θ₀ * ∏ j ∈ Finset.range s, (1 - KamProject.Arnold1963.Iteration.delta δ₁ j)

noncomputable def KamProject.Arnold1963.Iteration.upper (Θ₀ δ₁ : NNReal) (s : ℕ) : NNReal

The upper frequency-derivative bound after the accumulated multiplicative growth.

Equations

• KamProject.Arnold1963.Iteration.upper Θ₀ δ₁ s = Θ₀ * ∏ j ∈ Finset.range s, (1 + KamProject.Arnold1963.Iteration.delta δ₁ j)

noncomputable def KamProject.Arnold1963.Iteration.width (n : ℕ) (ρ₀ δ₁ : NNReal) (s : ℕ) : NNReal

The remaining angle-strip width after all preceding strip losses.

Equations

• KamProject.Arnold1963.Iteration.width n ρ₀ δ₁ s = ρ₀ - 3 * ∑ j ∈ Finset.range s, KamProject.Arnold1963.Iteration.gamma n δ₁ j

@[simp]

theorem KamProject.Arnold1963.Iteration.lower_zero (θ₀ δ₁ : NNReal) : lower θ₀ δ₁ 0 = θ₀

@[simp]

theorem KamProject.Arnold1963.Iteration.upper_zero (Θ₀ δ₁ : NNReal) : upper Θ₀ δ₁ 0 = Θ₀

@[simp]

theorem KamProject.Arnold1963.Iteration.width_zero (n : ℕ) (ρ₀ δ₁ : NNReal) : width n ρ₀ δ₁ 0 = ρ₀

theorem KamProject.Arnold1963.Iteration.lower_succ (θ₀ δ₁ : NNReal) (s : ℕ) : lower θ₀ δ₁ (s + 1) = lower θ₀ δ₁ s * (1 - delta δ₁ s)

theorem KamProject.Arnold1963.Iteration.upper_succ (Θ₀ δ₁ : NNReal) (s : ℕ) : upper Θ₀ δ₁ (s + 1) = upper Θ₀ δ₁ s * (1 + delta δ₁ s)

theorem KamProject.Arnold1963.Iteration.width_succ (n : ℕ) (ρ₀ δ₁ : NNReal) (s : ℕ) : width n ρ₀ δ₁ (s + 1) = width n ρ₀ δ₁ s - 3 * gamma n δ₁ s

theorem KamProject.Arnold1963.Iteration.lower_gt_half {θ₀ δ₁ : NNReal} (hθ : 0 < θ₀) (hδ : δ₁ < 1 / 4) (s : ℕ) : ↑θ₀ / 2 < ↑(lower θ₀ δ₁ s)

theorem KamProject.Arnold1963.Iteration.upper_lt_twice {Θ₀ δ₁ : NNReal} (hΘ : 0 < Θ₀) (hδ : δ₁ < 1 / 4) (s : ℕ) : ↑(upper Θ₀ δ₁ s) < 2 * ↑Θ₀

theorem KamProject.Arnold1963.Iteration.width_gt_two_fifths {n : ℕ} {ρ₀ δ₁ : NNReal} (hγ : gamma n δ₁ 0 ≤ 1 / 4) (hρ : ↑(gamma n δ₁ 0) < ↑ρ₀ / 10) (s : ℕ) : 2 * ↑ρ₀ / 5 < ↑(width n ρ₀ δ₁ s)

theorem KamProject.Arnold1963.Iteration.uniform_bounds_of_threshold {n : ℕ} (hn : 0 < n) {θ₀ Θ₀ ρ₀ δ₁ : NNReal} {κ D : ℝ} (hθ : 0 < θ₀) (hΘ : 0 < Θ₀) (hδ : ↑δ₁ < threshold5 n (↑θ₀) (↑Θ₀) (↑ρ₀) κ D) (s : ℕ) : ↑θ₀ / 2 < ↑(lower θ₀ δ₁ s) ∧ ↑(upper Θ₀ δ₁ s) < 2 * ↑Θ₀ ∧ 2 * ↑ρ₀ / 5 < ↑(width n ρ₀ δ₁ s) ∧ 3 * ↑(gamma n δ₁ s) < ↑(width n ρ₀ δ₁ s)