Supporting results for the analytic Hamiltonian KAM construction.

def KamProject.Arnold1963.IterationInput.newDomain {n : ℕ} {G Ω : Set (ComplexSpace n)} {ρ β δ γ θ Θ : NNReal} {K M : ℝ} {a : ComplexSpace n → ℂ} {f : AnalyticPhaseFunction n G ρ} {g : ComplexSpace n → ComplexSpace n} (i : IterationInput a f g β δ γ θ Θ K M) : Set (ComplexSpace n)

The action domain retained by corrected frequency inversion and finite resonance removal.

Equations

• i.newDomain = ⋯.iterationDomain K (KamProject.Arnold1963.fundamentalCutoff (↑γ) (2 * M))

def KamProject.Arnold1963.IterationInput.wideDomain {n : ℕ} {G Ω : Set (ComplexSpace n)} {ρ β δ γ θ Θ : NNReal} {K M : ℝ} {a : ComplexSpace n → ℂ} {f : AnalyticPhaseFunction n G ρ} {g : ComplexSpace n → ComplexSpace n} (i : IterationInput a f g β δ γ θ Θ K M) : Set (ComplexSpace n)

The wider action domain used before the final inductive restriction.

Equations

• i.wideDomain = KamProject.Arnold1963.erosion (⋯.iterationE K (KamProject.Arnold1963.fundamentalCutoff (↑γ) (2 * M))) (β + β)

theorem KamProject.Arnold1963.IterationInput.newDomain_subset {n : ℕ} {G Ω : Set (ComplexSpace n)} {ρ β δ γ θ Θ : NNReal} {K M : ℝ} {a : ComplexSpace n → ℂ} {f : AnalyticPhaseFunction n G ρ} {g : ComplexSpace n → ComplexSpace n} (i : IterationInput a f g β δ γ θ Θ K M) : i.newDomain ⊆ erosion G β

theorem KamProject.Arnold1963.IterationInput.newChart {n : ℕ} {G Ω : Set (ComplexSpace n)} {ρ β δ γ θ Θ : NNReal} {K M : ℝ} {a : ComplexSpace n → ℂ} {f : AnalyticPhaseFunction n G ρ} {g : ComplexSpace n → ComplexSpace n} (i : IterationInput a f g β δ γ θ Θ K M) : AnalyticFrequencyChart (actionFrequency i.newIntegrable) ⋯.newInverse i.newDomain (erosion (nonresonantDomain Ω id K (fundamentalCutoff (↑γ) (2 * M))) ((5 + 7 * Θ) * β))

theorem KamProject.Arnold1963.IterationInput.new_derivative_bounds {n : ℕ} {G Ω : Set (ComplexSpace n)} {ρ β δ γ θ Θ : NNReal} {K M : ℝ} {a : ComplexSpace n → ℂ} {f : AnalyticPhaseFunction n G ρ} {g : ComplexSpace n → ComplexSpace n} (i : IterationInput a f g β δ γ θ Θ K M) {p : ComplexSpace n} (hp : p ∈ i.newDomain) (v : ComplexSpace n) : ↑θ * (1 - ↑δ) * ‖v‖ ≤ ‖(fderiv ℂ (actionFrequency i.newIntegrable) p) v‖ ∧ ‖(fderiv ℂ (actionFrequency i.newIntegrable) p) v‖ ≤ ↑Θ * (1 + ↑δ) * ‖v‖

theorem KamProject.Arnold1963.IterationInput.frequency_displacement {n : ℕ} {G Ω : Set (ComplexSpace n)} {ρ β δ γ θ Θ : NNReal} {K M : ℝ} {a : ComplexSpace n → ℂ} {f : AnalyticPhaseFunction n G ρ} {g : ComplexSpace n → ComplexSpace n} (i : IterationInput a f g β δ γ θ Θ K M) {p : ComplexSpace n} (hp : p ∈ i.newDomain) : ‖actionFrequency i.newIntegrable p - actionFrequency a p‖ < ↑β * ↑δ

theorem KamProject.Arnold1963.IterationInput.new_width_pos {n : ℕ} {G Ω : Set (ComplexSpace n)} {ρ β δ γ θ Θ : NNReal} {K M : ℝ} {a : ComplexSpace n → ℂ} {f : AnalyticPhaseFunction n G ρ} {g : ComplexSpace n → ComplexSpace n} (i : IterationInput a f g β δ γ θ Θ K M) : 0 < ρ - 3 * γ

theorem KamProject.Arnold1963.IterationInput.phase_buffer {n : ℕ} {G Ω : Set (ComplexSpace n)} {ρ β δ γ θ Θ : NNReal} {K M : ℝ} {a : ComplexSpace n → ℂ} {f : AnalyticPhaseFunction n G ρ} {g : ComplexSpace n → ComplexSpace n} (i : IterationInput a f g β δ γ θ Θ K M) : phaseDomain i.newDomain (ρ - 3 * γ) ⊆ erosion (phaseDomain i.wideDomain (ρ - (γ + γ))) β

theorem KamProject.Arnold1963.IterationInput.phase_subset_wide {n : ℕ} {G Ω : Set (ComplexSpace n)} {ρ β δ γ θ Θ : NNReal} {K M : ℝ} {a : ComplexSpace n → ℂ} {f : AnalyticPhaseFunction n G ρ} {g : ComplexSpace n → ComplexSpace n} (i : IterationInput a f g β δ γ θ Θ K M) : phaseDomain i.newDomain (ρ - 3 * γ) ⊆ phaseDomain i.wideDomain (ρ - (γ + γ))

theorem KamProject.Arnold1963.IterationInput.phase_subset_old_erosion {n : ℕ} {G Ω : Set (ComplexSpace n)} {ρ β δ γ θ Θ : NNReal} {K M : ℝ} {a : ComplexSpace n → ℂ} {f : AnalyticPhaseFunction n G ρ} {g : ComplexSpace n → ComplexSpace n} (i : IterationInput a f g β δ γ θ Θ K M) : phaseDomain i.newDomain (ρ - 3 * γ) ⊆ erosion (phaseDomain G ρ) β