Supporting results for the analytic Hamiltonian KAM construction.

theorem KamProject.Arnold1963.frequencyLossRadius_three (Θ β : NNReal) : frequencyLossRadius Θ β (3 * β) = (5 + 7 * Θ) * β

theorem KamProject.Arnold1963.frequencyMeasureRadius_three (Θ β : NNReal) : frequencyLossRadius Θ β (3 * β) + β = (6 + 7 * Θ) * β

theorem KamProject.Arnold1963.neighborhood_subset_erosion_neighborhood {n : ℕ} (S : Set (ComplexSpace n)) (r t : NNReal) : closedBallNeighborhood S r ⊆ erosion (closedBallNeighborhood S (r + t)) t

theorem KamProject.Arnold1963.neighborhood_conj {n : ℕ} {S : Set (ComplexSpace n)} (hS : ConjInvariant S) (r : NNReal) : ConjInvariant (closedBallNeighborhood S r)

def KamProject.Arnold1963.FrequencyChangeInput.iterationDomain {n : ℕ} {A g Δ : ComplexSpace n → ComplexSpace n} {G Ω : Set (ComplexSpace n)} {β κ θ Θ : NNReal} (h : FrequencyChangeInput A g Δ G Ω β κ θ Θ) (K N : ℝ) : Set (ComplexSpace n)

The corrected action domain retained after finite resonance removal and erosion.

Equations

• h.iterationDomain K N = h.innerDomain (KamProject.Arnold1963.nonresonantDomain Ω id K N) (3 * β)

def KamProject.Arnold1963.FrequencyChangeInput.iterationE {n : ℕ} {A g Δ : ComplexSpace n → ComplexSpace n} {G Ω : Set (ComplexSpace n)} {β κ θ Θ : NNReal} (h : FrequencyChangeInput A g Δ G Ω β κ θ Θ) (K N : ℝ) : Set (ComplexSpace n)

A closed-ball neighborhood of the retained inductive action domain.

Equations

• h.iterationE K N = KamProject.Arnold1963.closedBallNeighborhood (h.iterationDomain K N) (3 * β)

theorem KamProject.Arnold1963.FrequencyChangeInput.iterationChart {n : ℕ} {A g Δ : ComplexSpace n → ComplexSpace n} {G Ω : Set (ComplexSpace n)} {β κ θ Θ : NNReal} (h : FrequencyChangeInput A g Δ G Ω β κ θ Θ) (K N : ℝ) : AnalyticFrequencyChart (fun (p : ComplexSpace n) => A p + Δ p) h.newInverse (h.iterationDomain K N) (erosion (nonresonantDomain Ω id K N) ((5 + 7 * Θ) * β))

theorem KamProject.Arnold1963.FrequencyChangeInput.iterationE_subset {n : ℕ} {A g Δ : ComplexSpace n → ComplexSpace n} {G Ω : Set (ComplexSpace n)} {β κ θ Θ : NNReal} (h : FrequencyChangeInput A g Δ G Ω β κ θ Θ) (K N : ℝ) : h.iterationE K N ⊆ erosion G β

theorem KamProject.Arnold1963.FrequencyChangeInput.iteration_derivative_bounds {n : ℕ} {A g Δ : ComplexSpace n → ComplexSpace n} {G Ω : Set (ComplexSpace n)} {β κ θ Θ : NNReal} (h : FrequencyChangeInput A g Δ G Ω β κ θ Θ) (K N : ℝ) {p : ComplexSpace n} (hp : p ∈ h.iterationDomain K N) (v : ComplexSpace n) : ↑θ * (1 - ↑κ) * ‖v‖ ≤ ‖(fderiv ℂ (fun (x : ComplexSpace n) => A x + Δ x) p) v‖ ∧ ‖(fderiv ℂ (fun (x : ComplexSpace n) => A x + Δ x) p) v‖ ≤ ↑Θ * (1 + ↑κ) * ‖v‖

theorem KamProject.Arnold1963.FrequencyChangeInput.iterationE_nonresonant {n : ℕ} {A g Δ : ComplexSpace n → ComplexSpace n} {G Ω : Set (ComplexSpace n)} {β κ θ Θ : NNReal} (h : FrequencyChangeInput A g Δ G Ω β κ θ Θ) (K N : ℝ) {p : ComplexSpace n} (hp : p ∈ h.iterationE K N) : FiniteNonresonant (A p + Δ p) K N

theorem KamProject.Arnold1963.FrequencyChangeInput.iterationE_compact {n : ℕ} {A g Δ : ComplexSpace n → ComplexSpace n} {G Ω : Set (ComplexSpace n)} {β κ θ Θ : NNReal} (h : FrequencyChangeInput A g Δ G Ω β κ θ Θ) (K N : ℝ) : IsCompact (h.iterationE K N)

theorem KamProject.Arnold1963.FrequencyChangeInput.iterationE_conj {n : ℕ} {A g Δ : ComplexSpace n → ComplexSpace n} {G Ω : Set (ComplexSpace n)} {β κ θ Θ : NNReal} (h : FrequencyChangeInput A g Δ G Ω β κ θ Θ) (K N : ℝ) : ConjInvariant (h.iterationE K N)

theorem KamProject.Arnold1963.FrequencyChangeInput.iteration_target_buffer {n : ℕ} {A g Δ : ComplexSpace n → ComplexSpace n} {G Ω : Set (ComplexSpace n)} {β κ θ Θ : NNReal} (h : FrequencyChangeInput A g Δ G Ω β κ θ Θ) (K N : ℝ) : closedBallNeighborhood (h.iterationDomain K N) β ⊆ erosion (h.iterationE K N) (β + β)

theorem KamProject.Arnold1963.FrequencyChangeInput.iteration_measure {n : ℕ} {A g Δ : ComplexSpace n → ComplexSpace n} {G Ω : Set (ComplexSpace n)} {β κ θ Θ : NNReal} (h : FrequencyChangeInput A g Δ G Ω β κ θ Θ) (K N : ℝ) : realVolume (G \ h.iterationDomain K N) ≤ ENNReal.ofReal ((↑θ)⁻¹ ^ n) * realVolume (Ω \ erosion (nonresonantDomain Ω id K N) ((6 + 7 * Θ) * β))

theorem KamProject.Arnold1963.FrequencyChangeInput.fundamentalInput {n : ℕ} {A g Δ : ComplexSpace n → ComplexSpace n} {G Ω : Set (ComplexSpace n)} {β κ θ Θ : NNReal} (h : FrequencyChangeInput A g Δ G Ω β κ θ Θ) {ρ δ γ : NNReal} {K M T : ℝ} {Hbar : ComplexSpace n → ℂ} {f : AnalyticPhaseFunction n (erosion G β) ρ} (hi : IntegrableData Hbar (erosion G β) T) (hfreq : ∀ p ∈ erosion G β, actionFrequency Hbar p = A p + Δ p) (hb : FundamentalParameters n ρ β δ γ K (2 * M) T) (hf : f.uniformNorm ≤ 2 * M) (hzero : ∀ p ∈ erosion G β, f.angleAverage p = 0) : FundamentalInput Hbar f

theorem KamProject.Arnold1963.frequency_iteration_next_chart {n : ℕ} {K N₀ N : ℝ} {A g Δ : ComplexSpace n → ComplexSpace n} {G Ωbase : Set (ComplexSpace n)} {β κ θ Θ : NNReal} (s : ResonanceDomainState n K N₀) (h : FrequencyChangeInput A g Δ G (s.domain Ωbase) β κ θ Θ) (hK : 0 < K) (hNN : N₀ ≤ N) : AnalyticFrequencyChart (fun (p : ComplexSpace n) => A p + Δ p) h.newInverse (h.iterationDomain K N) ((s.next hK hNN ((5 + 7 * Θ) * β)).domain Ωbase)

theorem KamProject.Arnold1963.frequency_iteration_measure_budget {n : ℕ} {K N₀ N D : ℝ} {A g Δ : ComplexSpace n → ComplexSpace n} {G Ωbase : Set (ComplexSpace n)} {β κ θ Θ : NNReal} (s : ResonanceDomainState n K N₀) (h : FrequencyChangeInput A g Δ G (s.domain Ωbase) β κ θ Θ) (hD : TypeD Ωbase D) (hn : 0 < n) (hK : 0 < K) (hN₀ : 1 ≤ N₀) (hN : 1 < N) (hNN : N₀ ≤ N) : realVolume (G \ h.iterationDomain K N) ≤ ENNReal.ofReal ((↑θ)⁻¹ ^ n) * (ENNReal.ofReal (resonanceLossConstant n * D * (K * newShellBudget N₀ N + ↑((6 + 7 * Θ) * β) * N ^ n)) * realVolume Ωbase)