Supporting results for the analytic Hamiltonian KAM construction.
structure
KamProject.Arnold1963.IterationInput
{n : ℕ}
{G Ω : Set (ComplexSpace n)}
{ρ : NNReal}
(a : ComplexSpace n → ℂ)
(f : AnalyticPhaseFunction n G ρ)
(g : ComplexSpace n → ComplexSpace n)
(β δ γ θ Θ : NNReal)
(K M : ℝ)
:
The analytic chart and quantitative hypotheses required for one inductive KAM step.
- chart : AnalyticFrequencyChart (actionFrequency a) g G Ω
- analytic : AnalyticOnNhd ℂ a G
- conj (p : ComplexSpace n) : p ∈ G → a (conjVec p) = star (a p)
- lower (p : ComplexSpace n) : p ∈ G → ∀ (v : ComplexSpace n), ↑θ * ‖v‖ ≤ ‖(fderiv ℂ (actionFrequency a) p) v‖
- upper (p : ComplexSpace n) : p ∈ G → ‖fderiv ℂ (actionFrequency a) p‖ ≤ ↑Θ
- budget : IterationParameters n ρ β δ γ θ Θ K M
Instances For
theorem
KamProject.Arnold1963.IterationInput.frequencyChange
{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)
:
FrequencyChangeInput (actionFrequency a) g f.frequencyShift G Ω β δ θ Θ
noncomputable def
KamProject.Arnold1963.IterationInput.newIntegrable
{n : ℕ}
{G Ω : Set (ComplexSpace n)}
{ρ β δ γ θ Θ : NNReal}
{K M : ℝ}
{a : ComplexSpace n → ℂ}
{f : AnalyticPhaseFunction n G ρ}
{g : ComplexSpace n → ComplexSpace n}
:
IterationInput a f g β δ γ θ Θ K M → ComplexSpace n → ℂ
The updated integrable Hamiltonian after absorbing the angle average.
Equations
- x✝.newIntegrable = f.averagedHamiltonian a
Instances For
noncomputable def
KamProject.Arnold1963.IterationInput.centeredPerturbation
{n : ℕ}
{G Ω : Set (ComplexSpace n)}
{ρ β δ γ θ Θ : NNReal}
{K M : ℝ}
{a : ComplexSpace n → ℂ}
{f : AnalyticPhaseFunction n G ρ}
{g : ComplexSpace n → ComplexSpace n}
:
IterationInput a f g β δ γ θ Θ K M → AnalyticPhaseFunction n (erosion G β) ρ
The centered perturbation restricted to the once-eroded action domain.
Equations
- x✝.centeredPerturbation = f.centered.restrict ⋯ ⋯ ⋯
Instances For
theorem
KamProject.Arnold1963.IterationInput.frequency_eventually
{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 ∈ G)
:
actionFrequency i.newIntegrable =ᶠ[nhds p] fun (p : ComplexSpace n) => actionFrequency a p + f.frequencyShift p
theorem
KamProject.Arnold1963.IterationInput.newIntegrable_data
{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)
:
IntegrableData i.newIntegrable (erosion G β) (2 * ↑Θ)
theorem
KamProject.Arnold1963.IterationInput.fundamental
{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)
: