Supporting results for the analytic Hamiltonian KAM construction.

structure KamProject.Arnold1963.FundamentalInput {n : ℕ} {G E : Set (ComplexSpace n)} {ρ β δ γ : NNReal} {K M Θ : ℝ} (h : ComplexSpace n → ℂ) (f : AnalyticPhaseFunction n G ρ) : Prop

The analytic, nonresonance and numerical hypotheses for the fundamental KAM construction.

• integrable : IntegrableData h G Θ
• domain_subset : E ⊆ G
• domain_conj : ConjInvariant E
• perturbation_bound : f.uniformNorm ≤ M
• mean_zero (p : ComplexSpace n) : p ∈ E → f.angleAverage p = 0
• nonresonant (p : ComplexSpace n) : p ∈ E → FiniteNonresonant (actionFrequency h p) K (fundamentalCutoff (↑γ) M)
• budget : FundamentalParameters n ρ β δ γ K M Θ

noncomputable def KamProject.Arnold1963.FundamentalInput.generator {n : ℕ} {G E : Set (ComplexSpace n)} {ρ β δ γ : NNReal} {K M Θ : ℝ} {h : ComplexSpace n → ℂ} {f : AnalyticPhaseFunction n G ρ} (i : FundamentalInput h f) : AnalyticPhaseFunction n E (ρ - (δ + δ))

The bounded analytic generating function solving the finite homological equation.

Equations

• i.generator = KamProject.Arnold1963.homologicalFunction f (KamProject.Arnold1963.actionFrequency h) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

theorem KamProject.Arnold1963.FundamentalInput.generator_bound {n : ℕ} {G E : Set (ComplexSpace n)} {ρ β δ γ : NNReal} {K M Θ : ℝ} {h : ComplexSpace n → ℂ} {f : AnalyticPhaseFunction n G ρ} (i : FundamentalInput h f) : i.generator.uniformNorm ≤ homologicalBound n M K ↑δ

theorem KamProject.Arnold1963.FundamentalInput.generatingData {n : ℕ} {G E : Set (ComplexSpace n)} {ρ β δ γ : NNReal} {K M Θ : ℝ} {h : ComplexSpace n → ℂ} {f : AnalyticPhaseFunction n G ρ} (i : FundamentalInput h f) : GeneratingData i.generator.toFun E (angleStrip n (ρ - (δ + δ))) β (homologicalBound n M K ↑δ)

noncomputable def KamProject.Arnold1963.FundamentalInput.transform {n : ℕ} {G E : Set (ComplexSpace n)} {ρ β δ γ : NNReal} {K M Θ : ℝ} {h : ComplexSpace n → ℂ} {f : AnalyticPhaseFunction n G ρ} (i : FundamentalInput h f) : ComplexPhaseSpace n → ComplexPhaseSpace n

The phase transformation obtained from the fundamental step's generating function.

Equations

• i.transform = KamProject.Arnold1963.generatingTransform i.generator.toFun E (KamProject.Arnold1963.angleStrip n (ρ - (δ + δ))) β

noncomputable def KamProject.Arnold1963.FundamentalInput.transformation {n : ℕ} {G E : Set (ComplexSpace n)} {ρ β δ γ : NNReal} {K M Θ : ℝ} {h : ComplexSpace n → ℂ} {f : AnalyticPhaseFunction n G ρ} (i : FundamentalInput h f) : AnalyticCanonicalTransformation (phaseDomain (erosion E (β + β)) (ρ - (γ + γ))) (phaseDomain G ρ) (homologicalBound n M K ↑δ / ↑β)

The fundamental canonical transformation on its retained phase domain.

Equations

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

theorem KamProject.Arnold1963.FundamentalInput.displacement {n : ℕ} {G E : Set (ComplexSpace n)} {ρ β δ γ : NNReal} {K M Θ : ℝ} {h : ComplexSpace n → ℂ} {f : AnalyticPhaseFunction n G ρ} (i : FundamentalInput h f) {z : ComplexPhaseSpace n} (hz : z ∈ phaseDomain (erosion E (β + β)) (ρ - (γ + γ))) : ‖i.transform z - z‖ ≤ homologicalBound n M K ↑δ / ↑β

theorem KamProject.Arnold1963.FundamentalInput.action_displacement {n : ℕ} {G E : Set (ComplexSpace n)} {ρ β δ γ : NNReal} {K M Θ : ℝ} {h : ComplexSpace n → ℂ} {f : AnalyticPhaseFunction n G ρ} (i : FundamentalInput h f) {z : ComplexPhaseSpace n} (hz : z ∈ phaseDomain (erosion E (β + β)) (ρ - (γ + γ))) : ‖(i.transform z).1 - z.1‖ ≤ homologicalBound n M K ↑δ / ↑δ

theorem KamProject.Arnold1963.FundamentalInput.action_displacement_beta {n : ℕ} {G E : Set (ComplexSpace n)} {ρ β δ γ : NNReal} {K M Θ : ℝ} {h : ComplexSpace n → ℂ} {f : AnalyticPhaseFunction n G ρ} (i : FundamentalInput h f) {z : ComplexPhaseSpace n} (hz : z ∈ phaseDomain (erosion E (β + β)) (ρ - (γ + γ))) : ‖(i.transform z).1 - z.1‖ ≤ ↑β

theorem KamProject.Arnold1963.FundamentalInput.angle_displacement_beta {n : ℕ} {G E : Set (ComplexSpace n)} {ρ β δ γ : NNReal} {K M Θ : ℝ} {h : ComplexSpace n → ℂ} {f : AnalyticPhaseFunction n G ρ} (i : FundamentalInput h f) {z : ComplexPhaseSpace n} (hz : z ∈ phaseDomain (erosion E (β + β)) (ρ - (γ + γ))) : dist (i.transform z).2 z.2 ≤ ↑β

theorem KamProject.Arnold1963.FundamentalInput.action_segment {n : ℕ} {G E : Set (ComplexSpace n)} {ρ β δ γ : NNReal} {K M Θ : ℝ} {h : ComplexSpace n → ℂ} {f : AnalyticPhaseFunction n G ρ} (i : FundamentalInput h f) {z : ComplexPhaseSpace n} (hz : z ∈ phaseDomain (erosion E (β + β)) (ρ - (γ + γ))) : segment ℝ z.1 (i.transform z).1 ⊆ erosion G β

theorem KamProject.Arnold1963.FundamentalInput.transformed_angle {n : ℕ} {G E : Set (ComplexSpace n)} {ρ β δ γ : NNReal} {K M Θ : ℝ} {h : ComplexSpace n → ℂ} {f : AnalyticPhaseFunction n G ρ} (i : FundamentalInput h f) {z : ComplexPhaseSpace n} (hz : z ∈ phaseDomain (erosion E (β + β)) (ρ - (γ + γ))) : (i.transform z).2 ∈ angleStrip n (ρ - (δ + γ))