Uniform estimates for cutoff growth relative to decay of the small parameter.

noncomputable def KamProject.Arnold1963.Iteration.cutoffConstant (n : ℕ) : ℝ

The dimension-dependent coefficient used to bound the iteration's Fourier cutoffs.

Equations

• KamProject.Arnold1963.Iteration.cutoffConstant n = 4 * ↑n * (↑(KamProject.Arnold1963.iterationExponent n) + 1) / Real.exp 1

theorem KamProject.Arnold1963.Iteration.InitialParameters.cutoff_bound {n : ℕ} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (s : ℕ) : cutoff n δ₁ s < cutoffConstant n / ↑(gamma n δ₁ s) ^ 2

theorem KamProject.Arnold1963.Iteration.InitialParameters.delta_cutoffConstant_small {n : ℕ} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (s : ℕ) : ↑(delta δ₁ s) * cutoffConstant n ^ (2 * n) < 1

theorem KamProject.Arnold1963.Iteration.InitialParameters.cutoff_budget {n : ℕ} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (s : ℕ) : ↑(delta δ₁ s) * cutoff n δ₁ s ^ n < 1