Construct the Hamiltonian states and cumulative transformations recursively from initial data. Stage existence and the Hamiltonian identities are proved by the construction.

structure KamProject.Arnold1963.Iteration.InitialData (n : ℕ) (Ω₀ : Set (ComplexSpace n)) (δ₁ θ₀ Θ₀ ρ₀ : NNReal) (D : ℝ) : Type

Analytic Hamiltonian, perturbation and frequency-chart data initiating the KAM iteration.

• domain : Set (ComplexSpace n)

  The initial complex action domain.

• integrable : ComplexSpace n → ℂ

  The initial integrable Hamiltonian depending only on action coordinates.

• perturbation : AnalyticPhaseFunction n self.domain ρ₀

  The initial analytic perturbation on the prescribed phase domain.

• inverseFrequency : ComplexSpace n → ComplexSpace n

  The inverse of the initial action-frequency chart.

• chart : AnalyticFrequencyChart (actionFrequency self.integrable) self.inverseFrequency self.domain Ω₀
• analytic : AnalyticOnNhd ℂ self.integrable self.domain
• conj (p : ComplexSpace n) : p ∈ self.domain → self.integrable (conjVec p) = star (self.integrable p)
• lower (p : ComplexSpace n) : p ∈ self.domain → ∀ (v : ComplexSpace n), ↑θ₀ * ‖v‖ ≤ ‖(fderiv ℂ (actionFrequency self.integrable) p) v‖
• upper (p : ComplexSpace n) : p ∈ self.domain → ‖fderiv ℂ (actionFrequency self.integrable) p‖ ≤ ↑Θ₀
• bound : self.perturbation.uniformNorm ≤ Iteration.perturbation n δ₁ 0
• typeD : TypeD Ω₀ D

theorem KamProject.Arnold1963.Iteration.InitialData.volume_pos {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {D : ℝ} (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) : 0 < realVolume h.domain

theorem KamProject.Arnold1963.Iteration.InitialData.volume_finite {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {D : ℝ} (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) : realVolume h.domain ≠ ⊤

noncomputable def KamProject.Arnold1963.Iteration.InitialData.initialState {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) : State n Ω₀ δ₁ θ₀ Θ₀ ρ₀ κ 0

The initial KAM state assembled from the Hamiltonian and parameter data.

Equations

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

def KamProject.Arnold1963.Iteration.InitialData.state {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) (s : ℕ) : State n Ω₀ δ₁ θ₀ Θ₀ ρ₀ κ s

The recursively constructed KAM state at each iteration stage.

Equations

• KamProject.Arnold1963.Iteration.InitialData.state b h 0 = KamProject.Arnold1963.Iteration.InitialData.initialState b h
• KamProject.Arnold1963.Iteration.InitialData.state b h s.succ = KamProject.Arnold1963.Iteration.State.next b (KamProject.Arnold1963.Iteration.InitialData.state b h s)

@[simp]

theorem KamProject.Arnold1963.Iteration.InitialData.state_zero {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) : state b h 0 = initialState b h

theorem KamProject.Arnold1963.Iteration.InitialData.state_succ {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) (s : ℕ) : state b h (s + 1) = State.next b (state b h s)

def KamProject.Arnold1963.Iteration.InitialData.actionDomain {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) (s : ℕ) : Set (ComplexSpace n)

The action domain retained at a given iteration stage.

Equations

• KamProject.Arnold1963.Iteration.InitialData.actionDomain b h s = (KamProject.Arnold1963.Iteration.InitialData.state b h s).domain

def KamProject.Arnold1963.Iteration.InitialData.phase {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) (s : ℕ) : Set (ComplexPhaseSpace n)

The phase domain retained at a given iteration stage.

Equations

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

noncomputable def KamProject.Arnold1963.Iteration.InitialData.hamiltonian {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) (s : ℕ) (z : ComplexPhaseSpace n) : ℂ

The sum of the integrable Hamiltonian and perturbation at a given stage.

Equations

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

noncomputable def KamProject.Arnold1963.Iteration.InitialData.transformation {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) (s : ℕ) : AnalyticCanonicalTransformation (phase b h (s + 1)) (phase b h s) ↑(beta δ₁ s)

The canonical transformation carrying the next phase domain into the current one.

Equations

• KamProject.Arnold1963.Iteration.InitialData.transformation b h s = (KamProject.Arnold1963.Iteration.InitialData.state b h s).step.transformation.restrict ⋯

theorem KamProject.Arnold1963.Iteration.InitialData.domain_zero {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) : actionDomain b h 0 = h.domain

theorem KamProject.Arnold1963.Iteration.InitialData.domain_step_subset {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) (s : ℕ) : actionDomain b h (s + 1) ⊆ erosion (actionDomain b h s) (beta δ₁ s)

theorem KamProject.Arnold1963.Iteration.InitialData.domain_antitone {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) : Antitone (actionDomain b h)

theorem KamProject.Arnold1963.Iteration.InitialData.domain_compact {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) (s : ℕ) : IsCompact (actionDomain b h s)

theorem KamProject.Arnold1963.Iteration.InitialData.perturbation_bound {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) (s : ℕ) : (state b h (s + 1)).perturbation.uniformNorm < Iteration.perturbation n δ₁ (s + 1)

theorem KamProject.Arnold1963.Iteration.InitialData.step_identity {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) (s : ℕ) (z : ComplexPhaseSpace n) : hamiltonian b h s ((transformation b h s).toFun z) = hamiltonian b h (s + 1) z

def KamProject.Arnold1963.Iteration.InitialData.cumulative {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) : ℕ → ComplexPhaseSpace n → ComplexPhaseSpace n

The cumulative composition carrying an iteration stage back to the original coordinates.

Equations

• One or more equations did not get rendered due to their size.
• KamProject.Arnold1963.Iteration.InitialData.cumulative b h 0 = id

theorem KamProject.Arnold1963.Iteration.InitialData.cumulative_maps {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) (s : ℕ) : Set.MapsTo (cumulative b h s) (phase b h s) (phase b h 0)

theorem KamProject.Arnold1963.Iteration.InitialData.cumulative_identity {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D) (s : ℕ) (z : ComplexPhaseSpace n) : hamiltonian b h 0 (cumulative b h s z) = hamiltonian b h s z