Nondegeneracy of the Hamiltonian Hessian supplies local frequency data. HamiltonianPatch is an output format whose existence is proved before the perturbation is chosen.

noncomputable def KamProject.Arnold1963.hessianDet {n : ℕ} (H₀ : ComplexSpace n → ℂ) (p : ComplexSpace n) : ℂ

The determinant of the derivative of the action-frequency map.

Equations

• KamProject.Arnold1963.hessianDet H₀ p = LinearMap.det ↑(fderiv ℂ (KamProject.Arnold1963.actionFrequency H₀) p)

theorem KamProject.Arnold1963.frequency_derivative_apply {n : ℕ} {H₀ : ComplexSpace n → ℂ} {p : ComplexSpace n} (ha : AnalyticAt ℂ H₀ p) (v : ComplexSpace n) (j : Fin n) : (fderiv ℂ (actionFrequency H₀) p) v j = ((fderiv ℂ (fderiv ℂ H₀) p) v) (Pi.single j 1)

theorem KamProject.Arnold1963.hessianDet_eq_matrix {n : ℕ} {H₀ : ComplexSpace n → ℂ} {p : ComplexSpace n} (ha : AnalyticAt ℂ H₀ p) : hessianDet H₀ p = Matrix.det fun (i j : Fin n) => ((fderiv ℂ (fderiv ℂ H₀) p) (Pi.single j 1)) (Pi.single i 1)

theorem KamProject.Arnold1963.isUnit_frequency_derivative_iff {n : ℕ} (H₀ : ComplexSpace n → ℂ) (p : ComplexSpace n) : IsUnit (fderiv ℂ (actionFrequency H₀) p) ↔ hessianDet H₀ p ≠ 0

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

A compact Hamiltonian patch with an analytic frequency chart and uniform derivative bounds.

• domain : Set (ComplexSpace n)

  The patch's compact complex action domain.

• subset : self.domain ⊆ ambient
• center : RealSpace n

  The real center of the patch's frequency polydisc.

• radius : ℝ

  The common coordinate radius of the patch's frequency polydisc.

• radius_pos : 0 < self.radius
• inverse : ComplexSpace n → ComplexSpace n

  The analytic inverse of the action-frequency chart on its frequency polydisc.

• chart : AnalyticFrequencyChart (actionFrequency H₀) self.inverse self.domain (realCenteredPolydisc self.center fun (x : Fin n) => self.radius)
• analytic : AnalyticOnNhd ℂ H₀ self.domain
• conj (p : ComplexSpace n) : p ∈ self.domain → H₀ (conjVec p) = star (H₀ p)
• lower : NNReal

  The positive lower bound on the frequency derivative, chosen below one.

• upper : NNReal

  The upper bound on the frequency derivative, chosen above one.

• lower_pos : 0 < self.lower
• lower_lt_one : self.lower < 1
• upper_gt_one : 1 < self.upper
• derivative_lower (p : ComplexSpace n) : p ∈ self.domain → ∀ (v : ComplexSpace n), ↑self.lower * ‖v‖ ≤ ‖(fderiv ℂ (actionFrequency H₀) p) v‖
• derivative_upper (p : ComplexSpace n) : p ∈ self.domain → ‖fderiv ℂ (actionFrequency H₀) p‖ ≤ ↑self.upper

def KamProject.Arnold1963.HamiltonianPatch.frequencyDomain {n : ℕ} {H₀ : ComplexSpace n → ℂ} {ambient : Set (ComplexSpace n)} (c : HamiltonianPatch n H₀ ambient) : Set (ComplexSpace n)

The frequency polydisc associated with the Hamiltonian patch.

Equations

• c.frequencyDomain = KamProject.Arnold1963.realCenteredPolydisc c.center fun (x : Fin n) => c.radius

noncomputable def KamProject.Arnold1963.HamiltonianPatch.typeConstant {n : ℕ} {H₀ : ComplexSpace n → ℂ} {ambient : Set (ComplexSpace n)} (c : HamiltonianPatch n H₀ ambient) : ℝ

The geometric type constant for the patch's frequency polydisc.

Equations

• c.typeConstant = KamProject.Arnold1963.polydiscTypeConstant fun (x : Fin n) => c.radius

theorem KamProject.Arnold1963.HamiltonianPatch.typeD {n : ℕ} {H₀ : ComplexSpace n → ℂ} {ambient : Set (ComplexSpace n)} (c : HamiltonianPatch n H₀ ambient) (hn : 0 < n) : TypeD c.frequencyDomain c.typeConstant

theorem KamProject.Arnold1963.HamiltonianPatch.exists_at {n : ℕ} {H₀ : ComplexSpace n → ℂ} {ambient : Set (ComplexSpace n)} {x : RealSpace n} {V : Set (ComplexSpace n)} (hV : V ∈ nhds (complexify x)) (hVG : V ⊆ ambient) (ha : AnalyticOnNhd ℂ H₀ ambient) (hc : ∀ p ∈ ambient, H₀ (conjVec p) = star (H₀ p)) (hnd : hessianDet H₀ (complexify x) ≠ 0) : ∃ (c : HamiltonianPatch n H₀ ambient), c.domain ⊆ V ∧ complexify x ∈ interior c.domain

theorem KamProject.Arnold1963.HamiltonianPatch.exists_finite_cover {n : ℕ} {H₀ : ComplexSpace n → ℂ} {ambient : Set (ComplexSpace n)} {K : Set (RealSpace n)} (hK : IsCompact K) (hKG : ∀ x ∈ K, complexify x ∈ interior ambient) (ha : AnalyticOnNhd ℂ H₀ ambient) (hc : ∀ p ∈ ambient, H₀ (conjVec p) = star (H₀ p)) (hnd : ∀ x ∈ K, hessianDet H₀ (complexify x) ≠ 0) : ∃ (s : Finset (HamiltonianPatch n H₀ ambient)), K ⊆ ⋃ c ∈ s, realSlice (interior c.domain)