Finite-tube representations of iterated frequency domains. Each integer direction retains one threshold, avoiding repeated tube counts as the cutoff grows and the domain is eroded.

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

An integer Fourier covector regarded as a real coordinate vector.

Equations

• KamProject.Arnold1963.integerCovector k j = ↑(k j)

@[simp]

theorem KamProject.Arnold1963.integerCovector_length {n : ℕ} (k : FourierIndex n) : covectorLength (integerCovector k) = indexLength k

@[simp]

theorem KamProject.Arnold1963.integerCovector_pairing {n : ℕ} (k : FourierIndex n) (z : ComplexSpace n) : realCovectorPairing (integerCovector k) z = indexPairing k z

structure KamProject.Arnold1963.ResonanceDomainState (n : ℕ) (K N : ℝ) : Type

Accumulated geometric erosion and resonance exclusions for a finite Fourier cutoff.

• radius : NNReal

  The accumulated erosion radius of the ambient frequency domain.

• width : FourierIndex n → ℝ

  The exclusion width assigned to each Fourier index.

• width_pos (k : FourierIndex n) : k ∈ lowModes n N → 0 < self.width k
• width_lower (k : FourierIndex n) : k ∈ lowModes n N → K / indexLength k ^ (n + 1) ≤ self.width k

def KamProject.Arnold1963.ResonanceDomainState.domain {n : ℕ} {K N : ℝ} (s : ResonanceDomainState n K N) (Ω : Set (ComplexSpace n)) : Set (ComplexSpace n)

The frequency domain satisfying the state's erosion and finite resonance constraints.

Equations

• One or more equations did not get rendered due to their size.

theorem KamProject.Arnold1963.ResonanceDomainState.mem_domain {n : ℕ} {K N : ℝ} (s : ResonanceDomainState n K N) {Ω : Set (ComplexSpace n)} {z : ComplexSpace n} : z ∈ s.domain Ω ↔ z ∈ erosion Ω s.radius ∧ ∀ k ∈ lowModes n N, s.width k ≤ ‖indexPairing k z‖

theorem KamProject.Arnold1963.ResonanceDomainState.subset {n : ℕ} {K N : ℝ} (s : ResonanceDomainState n K N) (Ω : Set (ComplexSpace n)) : s.domain Ω ⊆ Ω

theorem KamProject.Arnold1963.ResonanceDomainState.nonresonant {n : ℕ} {K N : ℝ} (s : ResonanceDomainState n K N) {Ω : Set (ComplexSpace n)} {z : ComplexSpace n} (hz : z ∈ s.domain Ω) : FiniteNonresonant z K N

theorem KamProject.Arnold1963.ResonanceDomainState.compact {n : ℕ} {K N : ℝ} (s : ResonanceDomainState n K N) {Ω : Set (ComplexSpace n)} (hc : IsCompact Ω) : IsCompact (s.domain Ω)

theorem KamProject.Arnold1963.ResonanceDomainState.conj {n : ℕ} {K N : ℝ} (s : ResonanceDomainState n K N) {Ω : Set (ComplexSpace n)} (hj : ConjInvariant Ω) : ConjInvariant (s.domain Ω)

def KamProject.Arnold1963.ResonanceDomainState.erode {n : ℕ} {K N : ℝ} (s : ResonanceDomainState n K N) (d : NNReal) : ResonanceDomainState n K N

Increasing geometric erosion and widening each resonance exclusion accordingly.

Equations

• s.erode d = { radius := s.radius + d, width := fun (k : KamProject.Arnold1963.FourierIndex n) => s.width k + ↑d * KamProject.Arnold1963.indexLength k, width_pos := ⋯, width_lower := ⋯ }

theorem KamProject.Arnold1963.ResonanceDomainState.erode_domain {n : ℕ} {K N : ℝ} (s : ResonanceDomainState n K N) (Ω : Set (ComplexSpace n)) (d : NNReal) : (s.erode d).domain Ω = erosion (s.domain Ω) d

noncomputable def KamProject.Arnold1963.ResonanceDomainState.cut {n : ℕ} {K N : ℝ} (s : ResonanceDomainState n K N) {N' : ℝ} (hK : 0 < K) (_hNN : N ≤ N') : ResonanceDomainState n K N'

Extending the Fourier cutoff while preserving old exclusions and initializing new ones.

Equations

• One or more equations did not get rendered due to their size.

theorem KamProject.Arnold1963.ResonanceDomainState.cut_domain {n : ℕ} {K N : ℝ} (s : ResonanceDomainState n K N) {N' : ℝ} (hK : 0 < K) (hNN : N ≤ N') (Ω : Set (ComplexSpace n)) : (s.cut hK hNN).domain Ω = nonresonantDomain (s.domain Ω) id K N'

noncomputable def KamProject.Arnold1963.ResonanceDomainState.next {n : ℕ} {K N : ℝ} (s : ResonanceDomainState n K N) {N' : ℝ} (hK : 0 < K) (hNN : N ≤ N') (d : NNReal) : ResonanceDomainState n K N'

The next resonance state after extending the cutoff and applying geometric erosion.

Equations

• s.next hK hNN d = (s.cut hK hNN).erode d

theorem KamProject.Arnold1963.ResonanceDomainState.next_domain {n : ℕ} {K N : ℝ} (s : ResonanceDomainState n K N) {N' : ℝ} (hK : 0 < K) (hNN : N ≤ N') (d : NNReal) (Ω : Set (ComplexSpace n)) : (s.next hK hNN d).domain Ω = erosion (nonresonantDomain (s.domain Ω) id K N') d

def KamProject.Arnold1963.ResonanceDomainState.initial (n : ℕ) (K : ℝ) : ResonanceDomainState n K 1

The initial resonance state at cutoff one, with no nonzero modes to exclude.

Equations

• KamProject.Arnold1963.ResonanceDomainState.initial n K = { radius := 0, width := fun (x : KamProject.Arnold1963.FourierIndex n) => 1, width_pos := ⋯, width_lower := ⋯ }

theorem KamProject.Arnold1963.ResonanceDomainState.initial_domain (n : ℕ) (K : ℝ) (Ω : Set (ComplexSpace n)) : (initial n K).domain Ω = Ω