Supporting results for the analytic Hamiltonian KAM construction.

def KamProject.Arnold1963.FiniteNonresonant {n : ℕ} (ω : ComplexSpace n) (K N : ℝ) : Prop

Finite-cutoff lower bounds on all retained nonzero integer frequency pairings.

Equations

• KamProject.Arnold1963.FiniteNonresonant ω K N = ∀ k ∈ KamProject.Arnold1963.lowModes n N, K / KamProject.Arnold1963.indexLength k ^ (n + 1) ≤ ‖KamProject.Arnold1963.indexPairing k ω‖

def KamProject.Arnold1963.nonresonantDomain {n : ℕ} (G : Set (ComplexSpace n)) (ω : ComplexSpace n → ComplexSpace n) (K N : ℝ) : Set (ComplexSpace n)

The action subdomain satisfying the finite-cutoff nonresonance condition.

Equations

• KamProject.Arnold1963.nonresonantDomain G ω K N = {p : KamProject.Arnold1963.ComplexSpace n | p ∈ G ∧ KamProject.Arnold1963.FiniteNonresonant (ω p) K N}

theorem KamProject.Arnold1963.FiniteNonresonant.ne_zero {n : ℕ} {ω : ComplexSpace n} {K N : ℝ} (h : FiniteNonresonant ω K N) (hK : 0 < K) {k : FourierIndex n} (hk : k ∈ lowModes n N) : indexPairing k ω ≠ 0

@[simp]

theorem KamProject.Arnold1963.indexLength_neg {n : ℕ} (k : FourierIndex n) : indexLength (-k) = indexLength k

theorem KamProject.Arnold1963.neg_mem_lowModes {n : ℕ} {k : FourierIndex n} {N : ℝ} : -k ∈ lowModes n N ↔ k ∈ lowModes n N

theorem KamProject.Arnold1963.indexPairing_conj {n : ℕ} (k : FourierIndex n) (z : ComplexSpace n) : indexPairing k (conjVec z) = star (indexPairing k z)

@[simp]

theorem KamProject.Arnold1963.indexPairing_neg {n : ℕ} (k : FourierIndex n) (z : ComplexSpace n) : indexPairing (-k) z = -indexPairing k z

theorem KamProject.Arnold1963.FiniteNonresonant.conj {n : ℕ} {ω : ComplexSpace n} {K N : ℝ} (h : FiniteNonresonant ω K N) : FiniteNonresonant (conjVec ω) K N

theorem KamProject.Arnold1963.nonresonantDomain_conj {n : ℕ} {G : Set (ComplexSpace n)} {ω : ComplexSpace n → ComplexSpace n} {K N : ℝ} (hG : ConjInvariant G) (hω : ∀ p ∈ G, ω (conjVec p) = conjVec (ω p)) : ConjInvariant (nonresonantDomain G ω K N)

theorem KamProject.Arnold1963.analyticAt_indexPairing {n : ℕ} (k : FourierIndex n) (z : ComplexSpace n) : AnalyticAt ℂ (indexPairing k) z