The union of actual local KAM outputs and a strict global bad-set measure bound. Local frequency labels retain their chart branches; cross-chart disjointness is proved separately.

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

def KamProject.Arnold1963.FiniteLocalization.phase {n : ℕ} {H₀ : ComplexSpace n → ℂ} {ambient : Set (ComplexSpace n)} {ρ : NNReal} {κ : ℝ} (_L : FiniteLocalization n H₀ ambient ρ κ) : Set (RealPhaseSpace n)

The initial real action-angle phase set over the ambient action domain.

Equations

• _L.phase = KamProject.Arnold1963.realSlice ambient ×ˢ Set.univ

def KamProject.Arnold1963.FiniteLocalization.goodSet {n : ℕ} {H₀ : ComplexSpace n → ℂ} {ambient : Set (ComplexSpace n)} {ρ : NNReal} {κ : ℝ} (L : FiniteLocalization n H₀ ambient ρ κ) (f : AnalyticPhaseFunction n ambient ρ) (hf : f.uniformNorm ≤ L.threshold) : Set (RealPhaseSpace n)

The union of good sets constructed by the finitely many local iterations.

Equations

• L.goodSet f hf = ⋃ (c : ↥L.patches), KamProject.Arnold1963.Iteration.InitialData.localF1 ⋯ (L.data f hf c)

def KamProject.Arnold1963.FiniteLocalization.badSet {n : ℕ} {H₀ : ComplexSpace n → ℂ} {ambient : Set (ComplexSpace n)} {ρ : NNReal} {κ : ℝ} (L : FiniteLocalization n H₀ ambient ρ κ) (f : AnalyticPhaseFunction n ambient ρ) (hf : f.uniformNorm ≤ L.threshold) : Set (RealPhaseSpace n)

The complement of the global good set inside the initial real phase set.

Equations

• L.badSet f hf = L.phase \ L.goodSet f hf

theorem KamProject.Arnold1963.FiniteLocalization.localPhase_subset {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) : (L.data f hf c).localPhase ⊆ L.phase

theorem KamProject.Arnold1963.FiniteLocalization.goodSet_subset {n : ℕ} {H₀ : ComplexSpace n → ℂ} {ambient : Set (ComplexSpace n)} {ρ : NNReal} {κ : ℝ} (L : FiniteLocalization n H₀ ambient ρ κ) (f : AnalyticPhaseFunction n ambient ρ) (hf : f.uniformNorm ≤ L.threshold) : L.goodSet f hf ⊆ L.phase

theorem KamProject.Arnold1963.FiniteLocalization.goodSet_compact {n : ℕ} {H₀ : ComplexSpace n → ℂ} {ambient : Set (ComplexSpace n)} {ρ : NNReal} {κ : ℝ} (L : FiniteLocalization n H₀ ambient ρ κ) (f : AnalyticPhaseFunction n ambient ρ) (hf : f.uniformNorm ≤ L.threshold) : IsCompact (L.goodSet f hf)

theorem KamProject.Arnold1963.FiniteLocalization.badSet_measurable {n : ℕ} {H₀ : ComplexSpace n → ℂ} {ambient : Set (ComplexSpace n)} {ρ : NNReal} {κ : ℝ} (L : FiniteLocalization n H₀ ambient ρ κ) (hG : IsCompact ambient) (f : AnalyticPhaseFunction n ambient ρ) (hf : f.uniformNorm ≤ L.threshold) : MeasurableSet (L.badSet f hf)

theorem KamProject.Arnold1963.FiniteLocalization.partition {n : ℕ} {H₀ : ComplexSpace n → ℂ} {ambient : Set (ComplexSpace n)} {ρ : NNReal} {κ : ℝ} (L : FiniteLocalization n H₀ ambient ρ κ) (f : AnalyticPhaseFunction n ambient ρ) (hf : f.uniformNorm ≤ L.threshold) : L.goodSet f hf ∪ L.badSet f hf = L.phase ∧ Disjoint (L.goodSet f hf) (L.badSet f hf)

theorem KamProject.Arnold1963.FiniteLocalization.phase_volume_finite {n : ℕ} {H₀ : ComplexSpace n → ℂ} {ambient : Set (ComplexSpace n)} {ρ : NNReal} {κ : ℝ} (L : FiniteLocalization n H₀ ambient ρ κ) (hG : IsCompact ambient) : MeasureTheory.volume L.phase ≠ ⊤

theorem KamProject.Arnold1963.FiniteLocalization.phase_cover {n : ℕ} {H₀ : ComplexSpace n → ℂ} {ambient : Set (ComplexSpace n)} {ρ : NNReal} {κ : ℝ} (L : FiniteLocalization n H₀ ambient ρ κ) (f : AnalyticPhaseFunction n ambient ρ) (hf : f.uniformNorm ≤ L.threshold) : MeasureTheory.volume (L.phase \ ⋃ (c : ↥L.patches), (L.data f hf c).localPhase) < ENNReal.ofReal L.coverError * MeasureTheory.volume L.phase

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

theorem KamProject.Arnold1963.FiniteLocalization.goodSet_eq_tori {n : ℕ} {H₀ : ComplexSpace n → ℂ} {ambient : Set (ComplexSpace n)} {ρ : NNReal} {κ : ℝ} (L : FiniteLocalization n H₀ ambient ρ κ) (f : AnalyticPhaseFunction n ambient ρ) (hf : f.uniformNorm ≤ L.threshold) : L.goodSet f hf = ⋃ (c : ↥L.patches), ⋃ ω ∈ Iteration.InitialData.retainedRealFrequencies ⋯ (L.data f hf c), Iteration.InitialData.frequencyTorus ⋯ (L.data f hf c) ω

theorem KamProject.Arnold1963.FiniteLocalization.goodSet_volume_pos {n : ℕ} {H₀ : ComplexSpace n → ℂ} {ambient : Set (ComplexSpace n)} {ρ : NNReal} {κ : ℝ} (L : FiniteLocalization n H₀ ambient ρ κ) (f : AnalyticPhaseFunction n ambient ρ) (hf : f.uniformNorm ≤ L.threshold) : 0 < MeasureTheory.volume (L.goodSet f hf)

theorem KamProject.Arnold1963.FiniteLocalization.corrections_small {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) {p q : ComplexSpace n} (hp : p ∈ Iteration.InitialData.limitDomain ⋯ (L.data f hf c)) (hq : q ∈ Iteration.InitialData.commonAngleStrip n L.width) : ‖Iteration.InitialData.actionCorrection ⋯ (L.data f hf c) p q‖ < κ ∧ ‖Iteration.InitialData.angleCorrection ⋯ (L.data f hf c) p q‖ < κ

theorem KamProject.Arnold1963.FiniteLocalization.orbit_original {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) {p : RealSpace n} (hp : p ∈ realSlice (Iteration.InitialData.limitDomain ⋯ (L.data f hf c))) (q : RealSpace n) (t : ℝ) : HasDerivAt (Iteration.InitialData.orbit ⋯ (L.data f hf c) p q) (hamiltonianVectorField (fun (z : ComplexPhaseSpace n) => H₀ z.1 + f.toFun z) (Iteration.InitialData.orbit ⋯ (L.data f hf c) p q t)) t

theorem KamProject.Arnold1963.FiniteLocalization.orbit_mem_goodSet {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) {p : RealSpace n} (hp : p ∈ realSlice (Iteration.InitialData.limitDomain ⋯ (L.data f hf c))) (q : RealSpace n) (t : ℝ) : torusProjection (realPartPhase (Iteration.InitialData.orbit ⋯ (L.data f hf c) p q t)) ∈ L.goodSet f hf

theorem KamProject.Arnold1963.FiniteLocalization.exists_global_orbit {n : ℕ} {H₀ : ComplexSpace n → ℂ} {ambient : Set (ComplexSpace n)} {ρ : NNReal} {κ : ℝ} (L : FiniteLocalization n H₀ ambient ρ κ) (f : AnalyticPhaseFunction n ambient ρ) (hf : f.uniformNorm ≤ L.threshold) {z : RealPhaseSpace n} (hz : z ∈ L.goodSet f hf) : ∃ (γ : ℝ → 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)) ∈ L.goodSet f hf

theorem KamProject.Arnold1963.global_kam_cover {n : ℕ} {H₀ : ComplexSpace n → ℂ} {ambient : Set (ComplexSpace n)} (h : GlobalHamiltonianData n H₀ ambient) {ρ : NNReal} {κ : ℝ} (hρ : 0 < ρ) (hκ : 0 < κ) : ∃ (L : FiniteLocalization n H₀ ambient ρ κ), ∀ (f : AnalyticPhaseFunction n ambient ρ) (hf : f.uniformNorm ≤ L.threshold), IsCompact (L.goodSet f hf) ∧ L.goodSet f hf ∪ L.badSet f hf = L.phase ∧ Disjoint (L.goodSet f hf) (L.badSet f hf) ∧ MeasureTheory.volume (L.badSet f hf) < ENNReal.ofReal κ * MeasureTheory.volume L.phase ∧ 0 < MeasureTheory.volume (L.goodSet f hf) ∧ ∀ (c : ↥L.patches), LocalKAMResult ⋯ (L.data f hf c)