Finite local coverage from the original nondegenerate Hamiltonian data. Loss is measured relative to the original action volume; the covering patches may overlap.

structure KamProject.Arnold1963.GlobalHamiltonianData (n : ℕ) (H₀ : ComplexSpace n → ℂ) (ambient : Set (ComplexSpace n)) : Type

The unperturbed Hamiltonian and explicit compact-domain hypotheses for the global theorem.

• dimension_pos : 0 < n
• compact : IsCompact ambient
• domain_conj : ConjInvariant ambient
• analytic : AnalyticOnNhd ℂ H₀ ambient
• conj (p : ComplexSpace n) : p ∈ ambient → H₀ (conjVec p) = star (H₀ p)
• realOpen : Set (RealSpace n)

  The nonempty open real action set whose closure is the ambient domain's real slice.

• isOpen_realOpen : IsOpen self.realOpen
• nonempty_realOpen : self.realOpen.Nonempty
• closure_realOpen : closure self.realOpen = realSlice ambient
• boundary_null : MeasureTheory.volume (frontier self.realOpen) = 0
• complex_interior (p : RealSpace n) : p ∈ self.realOpen → complexify p ∈ interior ambient
• nondegenerate (p : RealSpace n) : p ∈ self.realOpen → hessianDet H₀ (complexify p) ≠ 0

theorem KamProject.Arnold1963.GlobalHamiltonianData.realOpen_subset {n : ℕ} {H₀ : ComplexSpace n → ℂ} {ambient : Set (ComplexSpace n)} (h : GlobalHamiltonianData n H₀ ambient) : h.realOpen ⊆ realSlice ambient

theorem KamProject.Arnold1963.GlobalHamiltonianData.volume_finite {n : ℕ} {H₀ : ComplexSpace n → ℂ} {ambient : Set (ComplexSpace n)} (h : GlobalHamiltonianData n H₀ ambient) : MeasureTheory.volume (realSlice ambient) ≠ ⊤

theorem KamProject.Arnold1963.GlobalHamiltonianData.volume_pos {n : ℕ} {H₀ : ComplexSpace n → ℂ} {ambient : Set (ComplexSpace n)} (h : GlobalHamiltonianData n H₀ ambient) : 0 < MeasureTheory.volume (realSlice ambient)

theorem KamProject.Arnold1963.GlobalHamiltonianData.real_boundary_null {n : ℕ} {H₀ : ComplexSpace n → ℂ} {ambient : Set (ComplexSpace n)} (h : GlobalHamiltonianData n H₀ ambient) : MeasureTheory.volume (realSlice ambient \ h.realOpen) = 0

theorem KamProject.Arnold1963.GlobalHamiltonianData.exists_cover {n : ℕ} {H₀ : ComplexSpace n → ℂ} {ambient : Set (ComplexSpace n)} (h : GlobalHamiltonianData n H₀ ambient) (ε : ℝ) (hε : 0 < ε) : ∃ (s : Finset (HamiltonianPatch n H₀ ambient)), MeasureTheory.volume (realSlice ambient \ ⋃ c ∈ s, realSlice c.domain) < ENNReal.ofReal ε * MeasureTheory.volume (realSlice ambient)