Finite localization and a perturbation-independent common threshold. Patches may have different numerical bounds. The loss budget accounts for the number of patches rather than adding overlapping patch volumes as though they were disjoint.

structure KamProject.Arnold1963.FiniteLocalization (n : ℕ) (H₀ : ComplexSpace n → ℂ) (ambient : Set (ComplexSpace n)) (ρ : NNReal) (κ : ℝ) : Type

A finite collection of Hamiltonian patches with a common threshold and global measure budget.

• dimension_pos : 0 < n
• patches : Finset (HamiltonianPatch n H₀ ambient)

  The finite set of local Hamiltonian patches used for the global construction.

• width : NNReal

  The common positive angle width available in every patch.

• width_pos : 0 < self.width
• width_le_one : self.width ≤ 1
• width_le : self.width ≤ ρ
• fraction : ℝ

  The per-patch relative measure-loss tolerance.

• fraction_pos : 0 < self.fraction
• fraction_lt_one : self.fraction < 1
• fraction_le : self.fraction ≤ κ
• coverError : ℝ

  The relative volume allowed to escape the finite patch cover.

• coverError_pos : 0 < self.coverError
• coverError_lt_one : self.coverError < 1
• cover : MeasureTheory.volume (realSlice ambient \ ⋃ c ∈ self.patches, realSlice c.domain) < ENNReal.ofReal self.coverError * MeasureTheory.volume (realSlice ambient)
• budget : self.coverError + ↑self.patches.card * self.fraction ≤ κ
• threshold : ℝ

  The positive perturbation threshold valid uniformly across the patch collection.

• threshold_pos : 0 < self.threshold
• threshold_le (c : HamiltonianPatch n H₀ ambient) : c ∈ self.patches → self.threshold ≤ c.threshold self.width self.fraction

theorem KamProject.Arnold1963.GlobalHamiltonianData.exists_finiteLocalization {n : ℕ} {H₀ : ComplexSpace n → ℂ} {ambient : Set (ComplexSpace n)} (h : GlobalHamiltonianData n H₀ ambient) {ρ : NNReal} {κ : ℝ} (hρ : 0 < ρ) (hκ : 0 < κ) : Nonempty (FiniteLocalization n H₀ ambient ρ κ)

theorem KamProject.Arnold1963.FiniteLocalization.parameters {n : ℕ} {H₀ : ComplexSpace n → ℂ} {ambient : Set (ComplexSpace n)} {ρ : NNReal} {κ : ℝ} (L : FiniteLocalization n H₀ ambient ρ κ) (c : ↥L.patches) : Iteration.InitialParameters n ((↑c).seed L.width L.fraction) (↑c).lower (↑c).upper L.width L.fraction (↑c).typeConstant

def KamProject.Arnold1963.FiniteLocalization.data {n : ℕ} {H₀ : ComplexSpace n → ℂ} {ambient : Set (ComplexSpace n)} {ρ : NNReal} {κ : ℝ} (L : FiniteLocalization n H₀ ambient ρ κ) (f : AnalyticPhaseFunction n ambient ρ) (hf : f.uniformNorm ≤ L.threshold) (c : ↥L.patches) : Iteration.InitialData n (↑c).frequencyDomain ((↑c).seed L.width L.fraction) (↑c).lower (↑c).upper L.width (↑c).typeConstant

The initial iteration data for a perturbation restricted to a selected patch.

Equations

• L.data f hf c = (↑c).initialData ⋯ ⋯ ⋯ f ⋯ ⋯

theorem KamProject.Arnold1963.FiniteLocalization.local_result {n : ℕ} {H₀ : ComplexSpace n → ℂ} {ambient : Set (ComplexSpace n)} {ρ : NNReal} {κ : ℝ} (L : FiniteLocalization n H₀ ambient ρ κ) (f : AnalyticPhaseFunction n ambient ρ) (hf : f.uniformNorm ≤ L.threshold) (c : ↥L.patches) : LocalKAMResult ⋯ (L.data f hf c)

theorem KamProject.Arnold1963.FiniteLocalization.hamiltonian_zero {n : ℕ} {H₀ : ComplexSpace n → ℂ} {ambient : Set (ComplexSpace n)} {ρ : NNReal} {κ : ℝ} (L : FiniteLocalization n H₀ ambient ρ κ) (f : AnalyticPhaseFunction n ambient ρ) (hf : f.uniformNorm ≤ L.threshold) (c : ↥L.patches) (z : ComplexPhaseSpace n) : Iteration.InitialData.hamiltonian ⋯ (L.data f hf c) 0 z = H₀ z.1 + f.toFun z

theorem KamProject.Arnold1963.FiniteLocalization.patches_nonempty {n : ℕ} {H₀ : ComplexSpace n → ℂ} {ambient : Set (ComplexSpace n)} {ρ : NNReal} {κ : ℝ} (L : FiniteLocalization n H₀ ambient ρ κ) : L.patches.Nonempty