Analytic Hamiltonian KAM on the compact domains specified by GlobalHamiltonianData. A common positive threshold precedes the perturbation. The actual local constructions and cross-chart orbit-closure argument produce a pairwise disjoint family with a strict measure-loss bound.

theorem KamProject.Arnold1963.theorem1PeriodPositive : Fact (0 < 2 * Real.pi)

structure KamProject.Arnold1963.Theorem1Result (n : ℕ) (H₀ : ComplexSpace n → ℂ) (G : Set (ComplexSpace n)) (ρ : NNReal) (κ : ℝ) (f : AnalyticPhaseFunction n G ρ) : Type

The global KAM partition, measure bounds, realized tori and all-time Hamiltonian trajectories.

• width : NNReal

  The positive output width on which every realized torus lift is analytic.

• width_pos : 0 < self.width
• width_le : self.width ≤ ρ
• goodSet : Set (RealPhaseSpace n)

  The compact positive-measure set covered by the realized invariant tori.

• badSet : Set (RealPhaseSpace n)

  The measurable exceptional set complementary to the good set in the initial phase domain.

• tori : Set (Set (RealPhaseSpace n))

  The family of pairwise disjoint realized invariant tori.

• good_compact : IsCompact self.goodSet
• good_measurable : MeasurableSet self.goodSet
• bad_measurable : MeasurableSet self.badSet
• partition : self.goodSet ∪ self.badSet = realSlice G ×ˢ Set.univ
• disjoint_partition : Disjoint self.goodSet self.badSet
• good_volume_pos : 0 < MeasureTheory.volume self.goodSet
• good_nonempty : self.goodSet.Nonempty
• good_large : ENNReal.ofReal (1 - κ) * MeasureTheory.volume (realSlice G ×ˢ Set.univ) < MeasureTheory.volume self.goodSet
• bad_small : MeasureTheory.volume self.badSet < ENNReal.ofReal κ * MeasureTheory.volume (realSlice G ×ˢ Set.univ)
• union_eq : self.goodSet = ⋃₀ self.tori
• pairwise_disjoint : self.tori.Pairwise Disjoint
• realization (T : Set (RealPhaseSpace n)) : T ∈ self.tori → Nonempty (KAMTorus n H₀ f.toFun G self.width κ T)
• global_orbits (z : RealPhaseSpace n) : z ∈ self.goodSet → ∃ (γ : ℝ → ComplexPhaseSpace n), torusProjection (realPartPhase (γ 0)) = z ∧ (∀ (t : ℝ), HasDerivAt γ (hamiltonianVectorField (fun (w : ComplexPhaseSpace n) => H₀ w.1 + f.toFun w) (γ t)) t) ∧ (∀ (t : ℝ), complexifyPhase (realPartPhase (γ t)) = γ t) ∧ ∀ (t : ℝ), torusProjection (realPartPhase (γ t)) ∈ self.goodSet

theorem KamProject.Arnold1963.FiniteLocalization.goodSet_volume_gt {n : ℕ} {H₀ : ComplexSpace n → ℂ} {G : Set (ComplexSpace n)} {ρ : NNReal} {κ : ℝ} (L : FiniteLocalization n H₀ G ρ κ) (hG : IsCompact G) (f : AnalyticPhaseFunction n G ρ) (hf : f.uniformNorm ≤ L.threshold) : ENNReal.ofReal (1 - κ) * MeasureTheory.volume L.phase < MeasureTheory.volume (L.goodSet f hf)

noncomputable def KamProject.Arnold1963.FiniteLocalization.theorem1Result {n : ℕ} {H₀ : ComplexSpace n → ℂ} {G : Set (ComplexSpace n)} {ρ : NNReal} {κ : ℝ} (L : FiniteLocalization n H₀ G ρ κ) (hG : IsCompact G) (f : AnalyticPhaseFunction n G ρ) (hf : f.uniformNorm ≤ L.threshold) : Theorem1Result n H₀ G ρ κ f

The global KAM result assembled from a finite localization and a small perturbation.

Equations

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

theorem KamProject.Arnold1963.theorem1 {n : ℕ} {H₀ : ComplexSpace n → ℂ} {G : Set (ComplexSpace n)} (h : GlobalHamiltonianData n H₀ G) {ρ : NNReal} {κ : ℝ} (hρ : 0 < ρ) (hκ : 0 < κ) : ∃ (M : ℝ), 0 < M ∧ ∀ (f : AnalyticPhaseFunction n G ρ), f.uniformNorm ≤ M → Nonempty (Theorem1Result n H₀ G ρ κ f)

theorem KamProject.Arnold1963.theorem1_of_pointwise {n : ℕ} {H₀ : ComplexSpace n → ℂ} {G : Set (ComplexSpace n)} (h : GlobalHamiltonianData n H₀ G) {ρ : NNReal} {κ : ℝ} (hρ : 0 < ρ) (hκ : 0 < κ) : ∃ (M : ℝ), 0 < M ∧ ∀ (f : AnalyticPhaseFunction n G ρ), (∀ z ∈ phaseDomain G ρ, ‖f.toFun z‖ < M) → Nonempty (Theorem1Result n H₀ G ρ κ f)