The single-step resonance loss combines new shells with erosion layers of existing tubes.

def KamProject.Arnold1963.resonanceLossConstant (n : ℕ) : ℝ

The dimension-dependent coefficient bounding the measure of resonant shells.

Equations

• KamProject.Arnold1963.resonanceLossConstant n = ↑n * 2 ^ (n + 2)

theorem KamProject.Arnold1963.resonanceLossConstant_nonneg (n : ℕ) : 0 ≤ resonanceLossConstant n

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

theorem KamProject.Arnold1963.ResonanceDomainState.erosion_loss {n : ℕ} {K N D : ℝ} {Ω : Set (ComplexSpace n)} (s : ResonanceDomainState n K N) (h : TypeD Ω D) (hn : 0 < n) (hN : 1 < N) (d : NNReal) : realVolume (s.domain Ω \ erosion (s.domain Ω) d) ≤ ENNReal.ofReal (resonanceLossConstant n * D * ↑d * N ^ n) * realVolume Ω

theorem KamProject.Arnold1963.newShellBudget_nonneg (N₀ N₁ : ℝ) : 0 ≤ newShellBudget N₀ N₁

theorem KamProject.Arnold1963.TypeD.ar_loss_le {n : ℕ} {K N₀ N₁ D : ℝ} {Ω : Set (ComplexSpace n)} (h : TypeD Ω D) (s : ResonanceDomainState n K N₀) (hn : 0 < n) (hK : 0 < K) (hN₀ : 1 ≤ N₀) (hN₁ : 1 < N₁) (hNN : N₀ ≤ N₁) (d : NNReal) : realVolume (s.domain Ω \ erosion (nonresonantDomain (s.domain Ω) id K N₁) d) ≤ ENNReal.ofReal (resonanceLossConstant n * D * (K * newShellBudget N₀ N₁ + ↑d * N₁ ^ n)) * realVolume Ω