Counting integer lattice shells in the sum-of-absolute-coordinates norm. Natural lengths are proved equal to the public real-valued indexLength. All mode cutoffs are strict.

def KamProject.Arnold1963.latticeLength {n : ℕ} (k : FourierIndex n) : ℕ

The integer-valued sum of absolute Fourier coordinates, used to enumerate shells.

Equations

• KamProject.Arnold1963.latticeLength k = ∑ j : Fin n, (k j).natAbs

theorem KamProject.Arnold1963.indexLength_eq_latticeLength {n : ℕ} (k : FourierIndex n) : indexLength k = ↑(latticeLength k)

theorem KamProject.Arnold1963.natAbs_le_latticeLength {n : ℕ} (k : FourierIndex n) (j : Fin n) : (k j).natAbs ≤ latticeLength k

@[simp]

theorem KamProject.Arnold1963.latticeLength_zero {n : ℕ} : latticeLength 0 = 0

@[simp]

theorem KamProject.Arnold1963.latticeLength_eq_zero {n : ℕ} (k : FourierIndex n) : latticeLength k = 0 ↔ k = 0

theorem KamProject.Arnold1963.latticeLength_cons {n : ℕ} (a : ℤ) (k : FourierIndex n) : latticeLength (Fin.cons a k) = a.natAbs + latticeLength k

def KamProject.Arnold1963.latticeBox (n m : ℕ) : Finset (FourierIndex n)

The finite integer coordinate box containing every shell of the given radius.

Equations

• KamProject.Arnold1963.latticeBox n m = Fintype.piFinset fun (x : Fin n) => Finset.Icc (-↑m) ↑m

def KamProject.Arnold1963.latticeShell (n m : ℕ) : Finset (FourierIndex n)

The finite shell of integer indices with the specified sum of absolute coordinates.

Equations

• KamProject.Arnold1963.latticeShell n m = {k ∈ KamProject.Arnold1963.latticeBox n m | KamProject.Arnold1963.latticeLength k = m}

@[simp]

theorem KamProject.Arnold1963.mem_latticeShell {n m : ℕ} {k : FourierIndex n} : k ∈ latticeShell n m ↔ latticeLength k = m

@[simp]

theorem KamProject.Arnold1963.latticeShell_zero (n : ℕ) : latticeShell n 0 = {0}

theorem KamProject.Arnold1963.card_shell_fiber_le (n m : ℕ) (a : ℤ) : {k ∈ latticeShell (n + 1) m | k 0 = a}.card ≤ (latticeShell n (m - a.natAbs)).card

theorem KamProject.Arnold1963.card_latticeShell_one_le (m : ℕ) : (latticeShell 1 m).card ≤ 2

theorem KamProject.Arnold1963.card_latticeShell_le (n m : ℕ) (hn : 0 < n) (hm : 0 < m) : (latticeShell n m).card ≤ 2 ^ n * m ^ (n - 1)

def KamProject.Arnold1963.nonzeroLatticeBall (n M : ℕ) : Finset (FourierIndex n)

The finite union of nonzero lattice shells through the specified radius.

Equations

• KamProject.Arnold1963.nonzeroLatticeBall n M = (Finset.Icc 1 M).biUnion (KamProject.Arnold1963.latticeShell n)

@[simp]

theorem KamProject.Arnold1963.mem_nonzeroLatticeBall {n M : ℕ} {k : FourierIndex n} : k ∈ nonzeroLatticeBall n M ↔ 0 < latticeLength k ∧ latticeLength k ≤ M

theorem KamProject.Arnold1963.card_nonzeroLatticeBall_le (n M : ℕ) (hn : 0 < n) : (nonzeroLatticeBall n M).card ≤ 2 ^ n * M ^ n

noncomputable def KamProject.Arnold1963.lowModes (n : ℕ) (N : ℝ) : Finset (FourierIndex n)

Nonzero Fourier indices with length strictly below the real cutoff.

Equations

• KamProject.Arnold1963.lowModes n N = KamProject.Arnold1963.nonzeroLatticeBall n (⌈N⌉₊ - 1)

@[simp]

theorem KamProject.Arnold1963.mem_lowModes {n : ℕ} {N : ℝ} {k : FourierIndex n} : k ∈ lowModes n N ↔ 0 < indexLength k ∧ indexLength k < N

noncomputable def KamProject.Arnold1963.fourierModes (n : ℕ) (N : ℝ) : Finset (FourierIndex n)

Fourier modes below the cutoff, including zero when the cutoff is positive.

Equations

• KamProject.Arnold1963.fourierModes n N = if 0 < N then insert 0 (KamProject.Arnold1963.lowModes n N) else ∅

@[simp]

theorem KamProject.Arnold1963.mem_fourierModes {n : ℕ} {N : ℝ} {k : FourierIndex n} : k ∈ fourierModes n N ↔ indexLength k < N

theorem KamProject.Arnold1963.not_mem_fourierModes {n : ℕ} {N : ℝ} {k : FourierIndex n} : k ∉ fourierModes n N ↔ N ≤ indexLength k

theorem KamProject.Arnold1963.fourierModes_eq_insert_lowModes (n : ℕ) {N : ℝ} (hN : 0 < N) : fourierModes n N = insert 0 (lowModes n N)

theorem KamProject.Arnold1963.card_lowModes_le {n : ℕ} {N : ℝ} (hn : 0 < n) (hN : 1 < N) : ↑(lowModes n N).card ≤ 2 ^ n * N ^ n