Increasing cutoffs give a common small-divisor bound for every nonzero integer mode of the limit frequency.

theorem KamProject.Arnold1963.Iteration.indexLength_pos_of_ne_zero {n : ℕ} (k : FourierIndex n) (hk : k ≠ 0) : 0 < indexLength k

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

def KamProject.Arnold1963.Iteration.InitialData.frequencyDomain {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) (s : ℕ) : Set (ComplexSpace n)

The resonance-filtered frequency domain at the specified iteration stage.

Equations

• KamProject.Arnold1963.Iteration.InitialData.frequencyDomain b h s = (KamProject.Arnold1963.Iteration.InitialData.state b h s).ar.domain Ω₀

theorem KamProject.Arnold1963.Iteration.InitialData.frequencyDomain_succ {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) (s : ℕ) : frequencyDomain b h (s + 1) = erosion (nonresonantDomain (frequencyDomain b h s) id (κ * ↑δ₁) (cutoff n δ₁ s)) ((5 + 7 * Iteration.upper Θ₀ δ₁ s) * beta δ₁ s)

theorem KamProject.Arnold1963.Iteration.InitialData.frequencyDomain_antitone {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) : Antitone (frequencyDomain b h)

theorem KamProject.Arnold1963.Iteration.InitialData.limitFrequency_mem {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) {p : ComplexSpace n} (hp : p ∈ limitDomain b h) (s : ℕ) : limitFrequency b h p ∈ frequencyDomain b h s

theorem KamProject.Arnold1963.Iteration.InitialData.limitFrequency_nonresonant {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) {p : ComplexSpace n} (hp : p ∈ limitDomain b h) (k : FourierIndex n) (hk : k ≠ 0) : κ * ↑δ₁ / indexLength k ^ (n + 1) ≤ ‖indexPairing k (limitFrequency b h p)‖

theorem KamProject.Arnold1963.Iteration.InitialData.limitFrequency_no_integer_relation {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) {p : ComplexSpace n} (hp : p ∈ limitDomain b h) (k : FourierIndex n) (hk : k ≠ 0) : indexPairing k (limitFrequency b h p) ≠ 0