Supporting results for the analytic Hamiltonian KAM construction.

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

The transformed Hamiltonian remainder packaged as an analytic perturbation.

Equations

• i.newPerturbation = { toFun := i.remainder, domain_conj := ⋯, analytic := ⋯, periodic := ⋯, conj_compatible := ⋯, bounded := ⋯ }

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

theorem KamProject.Arnold1963.FundamentalInput.transformed_hamiltonian {n : ℕ} {G E : Set (ComplexSpace n)} {ρ β δ γ : NNReal} {K M Θ : ℝ} {h : ComplexSpace n → ℂ} {f : AnalyticPhaseFunction n G ρ} (i : FundamentalInput h f) (z : ComplexPhaseSpace n) : h (i.transform z).1 + f.toFun (i.transform z) = h z.1 + i.newPerturbation.toFun z

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

The fundamental canonical transformation and its quantitative perturbation remainder.

• transformation : AnalyticCanonicalTransformation (phaseDomain (erosion E (β + β)) (ρ - (γ + γ))) (phaseDomain G ρ) (homologicalBound n M K ↑δ / ↑β)

  The canonical transformation constructed by the fundamental step.

• perturbation : AnalyticPhaseFunction n (erosion E (β + β)) (ρ - (γ + γ))

  The analytic remainder of the transformed Hamiltonian on the retained phase domain.

• identity (z : ComplexPhaseSpace n) : h (self.transformation.toFun z).1 + f.toFun (self.transformation.toFun z) = h z.1 + self.perturbation.toFun z
• bound : self.perturbation.uniformNorm < fundamentalRemainderBound n M ↑δ ↑β
• displacement_lt (z : ComplexPhaseSpace n) : z ∈ phaseDomain (erosion E (β + β)) (ρ - (γ + γ)) → ‖self.transformation.toFun z - z‖ < ↑β
• action_bound (z : ComplexPhaseSpace n) : z ∈ phaseDomain (erosion E (β + β)) (ρ - (γ + γ)) → ‖(self.transformation.toFun z).1 - z.1‖ ≤ homologicalBound n M K ↑δ / ↑δ
• periodic (z : ComplexPhaseSpace n) : z ∈ phaseDomain (erosion E (β + β)) (ρ - (γ + γ)) → ∀ (k : FourierIndex n), self.transformation.toFun (phaseShift k z) = phaseShift k (self.transformation.toFun z)
• conj_compatible (z : ComplexPhaseSpace n) : z ∈ phaseDomain (erosion E (β + β)) (ρ - (γ + γ)) → self.transformation.toFun (conjPhase z) = conjPhase (self.transformation.toFun z)

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

The fundamental-step result assembled from its verified analytic and numerical inputs.

Equations

• i.result = { transformation := i.transformation, perturbation := i.newPerturbation, identity := ⋯, bound := ⋯, displacement_lt := ⋯, action_bound := ⋯, periodic := ⋯, conj_compatible := ⋯ }

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

theorem KamProject.Arnold1963.FundamentalInput.onNonresonantDomain {n : ℕ} {G : Set (ComplexSpace n)} {ρ β δ γ : NNReal} {K M Θ : ℝ} {h : ComplexSpace n → ℂ} {f : AnalyticPhaseFunction n G ρ} (hi : IntegrableData h G Θ) (hb : FundamentalParameters n ρ β δ γ K M Θ) (hf : f.uniformNorm ≤ M) (hzero : ∀ p ∈ G, f.angleAverage p = 0) : FundamentalInput h f