The actual recursive Hamiltonian state and its next-stage data.

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

The Hamiltonian, resonance exclusions and frequency chart at a given KAM stage.

• domain : Set (ComplexSpace n)

  The action domain retained by this KAM state.

• ar : ResonanceDomainState n (κ * ↑δ₁) (previousCutoff n δ₁ s)

  The accumulated resonance exclusions and geometric erosion at this stage.

• integrable : ComplexSpace n → ℂ

  The current integrable Hamiltonian depending only on action coordinates.

• perturbation : AnalyticPhaseFunction n self.domain (width n ρ₀ δ₁ s)

  The current analytic perturbation on the retained phase domain.

• inverseFrequency : ComplexSpace n → ComplexSpace n

  The inverse of the current action-frequency chart.

• input : IterationInput self.integrable self.perturbation self.inverseFrequency (beta δ₁ s) (delta δ₁ s) (gamma n δ₁ s) (lower θ₀ δ₁ s) (upper Θ₀ δ₁ s) (κ * ↑δ₁) (Iteration.perturbation n δ₁ s)

noncomputable def KamProject.Arnold1963.Iteration.State.step {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ : ℝ} {s : ℕ} (z : State n Ω₀ δ₁ θ₀ Θ₀ ρ₀ κ s) : InductiveResult z.integrable z.perturbation (z.ar.domain Ω₀) (beta δ₁ s) (delta δ₁ s) (gamma n δ₁ s) (lower θ₀ δ₁ s) (upper Θ₀ δ₁ s) (κ * ↑δ₁) (Iteration.perturbation n δ₁ s)

The inductive KAM step constructed from the current state's verified input data.

Equations

• z.step = ⋯.result

noncomputable def KamProject.Arnold1963.Iteration.State.nextPerturbation {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ : ℝ} {s : ℕ} (z : State n Ω₀ δ₁ θ₀ Θ₀ ρ₀ κ s) : AnalyticPhaseFunction n z.step.domain (width n ρ₀ δ₁ (s + 1))

The next perturbation restricted to the strip width prescribed by the iteration.

Equations

• z.nextPerturbation = z.step.perturbation.restrict ⋯ ⋯ ⋯

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

noncomputable def KamProject.Arnold1963.Iteration.State.nextAR {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} {s : ℕ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (z : State n Ω₀ δ₁ θ₀ Θ₀ ρ₀ κ s) : ResonanceDomainState n (κ * ↑δ₁) (previousCutoff n δ₁ (s + 1))

The next resonance state after adding modes and the prescribed geometric loss.

Equations

• KamProject.Arnold1963.Iteration.State.nextAR b z = z.ar.next ⋯ ⋯ ((5 + 7 * KamProject.Arnold1963.Iteration.upper Θ₀ δ₁ s) * KamProject.Arnold1963.Iteration.beta δ₁ s)

theorem KamProject.Arnold1963.Iteration.State.nextInput {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} {s : ℕ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (z : State n Ω₀ δ₁ θ₀ Θ₀ ρ₀ κ s) : IterationInput (z.perturbation.averagedHamiltonian z.integrable) z.nextPerturbation z.step.inverseFrequency (beta δ₁ (s + 1)) (delta δ₁ (s + 1)) (gamma n δ₁ (s + 1)) (lower θ₀ δ₁ (s + 1)) (upper Θ₀ δ₁ (s + 1)) (κ * ↑δ₁) (Iteration.perturbation n δ₁ (s + 1))

noncomputable def KamProject.Arnold1963.Iteration.State.next {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} {s : ℕ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (z : State n Ω₀ δ₁ θ₀ Θ₀ ρ₀ κ s) : State n Ω₀ δ₁ θ₀ Θ₀ ρ₀ κ (s + 1)

The successor KAM state with updated Hamiltonian, perturbation and frequency chart.

Equations

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

theorem KamProject.Arnold1963.Iteration.State.next_domain_subset {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} {s : ℕ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (z : State n Ω₀ δ₁ θ₀ Θ₀ ρ₀ κ s) : (next b z).domain ⊆ erosion z.domain (beta δ₁ s)

theorem KamProject.Arnold1963.Iteration.State.next_identity {n : ℕ} {Ω₀ : Set (ComplexSpace n)} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} {s : ℕ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (z : State n Ω₀ δ₁ θ₀ Θ₀ ρ₀ κ s) (x : ComplexPhaseSpace n) : z.integrable (z.step.transformation.toFun x).1 + z.perturbation.toFun (z.step.transformation.toFun x) = (next b z).integrable x.1 + (next b z).perturbation.toFun x