Measure estimates for newly excluded lattice shells, using the strict mode cutoff. Previously excluded shells are charged once.

def KamProject.Arnold1963.resonanceSet {n : ℕ} (Ω : Set (ComplexSpace n)) (K : ℝ) (k : FourierIndex n) : Set (ComplexSpace n)

The frequencies where a given Fourier pairing violates the prescribed small-divisor bound.

Equations

• KamProject.Arnold1963.resonanceSet Ω K k = Ω ∩ {ω : KamProject.Arnold1963.ComplexSpace n | ‖KamProject.Arnold1963.indexPairing k ω‖ < K / KamProject.Arnold1963.indexLength k ^ (n + 1)}

def KamProject.Arnold1963.resonantShell {n : ℕ} (Ω : Set (ComplexSpace n)) (K : ℝ) (m : ℕ) : Set (ComplexSpace n)

The union of resonances associated with one lattice shell.

Equations

• KamProject.Arnold1963.resonantShell Ω K m = ⋃ k ∈ KamProject.Arnold1963.latticeShell n m, KamProject.Arnold1963.resonanceSet Ω K k

noncomputable def KamProject.Arnold1963.newShells (N₀ N₁ : ℝ) : Finset ℕ

The integer shell radii introduced when the real Fourier cutoff increases.

Equations

• KamProject.Arnold1963.newShells N₀ N₁ = Finset.Ico ⌈N₀⌉₊ ⌈N₁⌉₊

noncomputable def KamProject.Arnold1963.newShellBudget (N₀ N₁ : ℝ) : ℝ

The reciprocal-square sum budgeting the newly introduced resonance shells.

Equations

• KamProject.Arnold1963.newShellBudget N₀ N₁ = ∑ m ∈ KamProject.Arnold1963.newShells N₀ N₁, 1 / ↑m ^ 2

theorem KamProject.Arnold1963.FiniteNonresonant.mono_cutoff {n : ℕ} {ω : ComplexSpace n} {K N₀ N₁ : ℝ} (h : FiniteNonresonant ω K N₁) (hN : N₀ ≤ N₁) : FiniteNonresonant ω K N₀

theorem KamProject.Arnold1963.isClosed_finiteNonresonant {n : ℕ} (K N : ℝ) : IsClosed {ω : ComplexSpace n | FiniteNonresonant ω K N}

theorem KamProject.Arnold1963.isCompact_nonresonant_frequency_domain {n : ℕ} {Ω : Set (ComplexSpace n)} (hΩ : IsCompact Ω) (K N : ℝ) : IsCompact (nonresonantDomain Ω id K N)

theorem KamProject.Arnold1963.nonresonant_on_erosion {n : ℕ} {Ω : Set (ComplexSpace n)} {K N : ℝ} (d : NNReal) {ω : ComplexSpace n} (hω : ω ∈ erosion (nonresonantDomain Ω id K N) d) : FiniteNonresonant ω K N

theorem KamProject.Arnold1963.mem_newShells {N₀ N₁ : ℝ} {m : ℕ} : m ∈ newShells N₀ N₁ ↔ N₀ ≤ ↑m ∧ ↑m < N₁

theorem KamProject.Arnold1963.nonresonant_removed_subset_new_shells {n : ℕ} {Ω E : Set (ComplexSpace n)} {K N₀ N₁ : ℝ} (hE : E ⊆ Ω) (hold : ∀ ω ∈ E, FiniteNonresonant ω K N₀) : E \ nonresonantDomain E id K N₁ ⊆ ⋃ m ∈ newShells N₀ N₁, resonantShell Ω K m

theorem KamProject.Arnold1963.TypeD.resonance_le {n : ℕ} {Ω : Set (ComplexSpace n)} {D K : ℝ} (d : TypeD Ω D) (hK : 0 ≤ K) {k : FourierIndex n} (hk : 0 < latticeLength k) : realVolume (resonanceSet Ω K k) ≤ ENNReal.ofReal (2 * D * ↑n * K / indexLength k ^ (n + 1)) * realVolume Ω

theorem KamProject.Arnold1963.TypeD.resonantShell_le {n m : ℕ} {Ω : Set (ComplexSpace n)} {D K : ℝ} (d : TypeD Ω D) (hn : 0 < n) (hm : 0 < m) (hK : 0 ≤ K) : realVolume (resonantShell Ω K m) ≤ ENNReal.ofReal (2 ^ (n + 1) * ↑n * D * K / ↑m ^ 2) * realVolume Ω

theorem KamProject.Arnold1963.TypeD.new_resonance_loss_le {n : ℕ} {Ω E : Set (ComplexSpace n)} {D K N₀ N₁ : ℝ} (d : TypeD Ω D) (hn : 0 < n) (hK : 0 ≤ K) (hN₀ : 1 ≤ N₀) (hE : E ⊆ Ω) (hold : ∀ ω ∈ E, FiniteNonresonant ω K N₀) : realVolume (E \ nonresonantDomain E id K N₁) ≤ ENNReal.ofReal (2 ^ (n + 1) * ↑n * D * K * newShellBudget N₀ N₁) * realVolume Ω