Strictly increasing Fourier cutoffs from the actual perturbation and angle-loss sequences.

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

The Fourier cutoff selected from the stage's strip loss and perturbation bound.

Equations

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

noncomputable def KamProject.Arnold1963.Iteration.previousCutoff (n : ℕ) (δ₁ : NNReal) : ℕ → ℝ

The preceding Fourier cutoff, initialized to one before the first step.

Equations

• KamProject.Arnold1963.Iteration.previousCutoff n δ₁ 0 = 1
• KamProject.Arnold1963.Iteration.previousCutoff n δ₁ s.succ = KamProject.Arnold1963.Iteration.cutoff n δ₁ s

theorem KamProject.Arnold1963.Iteration.InitialParameters.perturbation_step_pos {n : ℕ} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (s : ℕ) : 0 < perturbation n δ₁ s

theorem KamProject.Arnold1963.Iteration.InitialParameters.perturbation_le_delta {n : ℕ} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (s : ℕ) : perturbation n δ₁ s ≤ ↑(delta δ₁ s)

theorem KamProject.Arnold1963.Iteration.InitialParameters.cutoff_numerator_gt_half {n : ℕ} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (s : ℕ) : 1 / 2 < Real.log (1 / (2 * perturbation n δ₁ s))

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

theorem KamProject.Arnold1963.Iteration.InitialParameters.cutoff_strictMono {n : ℕ} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) : StrictMono (cutoff n δ₁)

theorem KamProject.Arnold1963.Iteration.InitialParameters.previousCutoff_strictMono {n : ℕ} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) : StrictMono (previousCutoff n δ₁)

theorem KamProject.Arnold1963.Iteration.InitialParameters.previousCutoff_ge_one {n : ℕ} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (s : ℕ) : 1 ≤ previousCutoff n δ₁ s

theorem KamProject.Arnold1963.Iteration.InitialParameters.cutoff_step_le {n : ℕ} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (s : ℕ) : previousCutoff n δ₁ s ≤ cutoff n δ₁ s