Supporting results for the analytic Hamiltonian KAM construction.

noncomputable def KamProject.Arnold1963.iterationRemainderBound (n : ℕ) (M δ β : ℝ) : ℝ

The quadratic perturbation bound supplied by one inductive KAM step.

Equations

• KamProject.Arnold1963.iterationRemainderBound n M δ β = M ^ 2 / (δ ^ (2 * KamProject.Arnold1963.stepExponent n) * β ^ 2)

theorem KamProject.Arnold1963.fundamentalRemainderBound_eq_iterationRemainderBound (n : ℕ) (M δ β : ℝ) : fundamentalRemainderBound n (2 * M) δ β = iterationRemainderBound n M δ β

noncomputable def KamProject.Arnold1963.IterationInput.wideResult {n : ℕ} {G Ω : Set (ComplexSpace n)} {ρ β δ γ θ Θ : NNReal} {K M : ℝ} {a : ComplexSpace n → ℂ} {f : AnalyticPhaseFunction n G ρ} {g : ComplexSpace n → ComplexSpace n} (i : IterationInput a f g β δ γ θ Θ K M) : FundamentalResult i.newIntegrable i.centeredPerturbation (⋯.iterationE K (fundamentalCutoff (↑γ) (2 * M))) β δ γ K (2 * M)

The fundamental result before restricting to the narrower inductive phase domain.

Equations

• i.wideResult = ⋯.result

theorem KamProject.Arnold1963.IterationInput.newDomain_subset_wide {n : ℕ} {G Ω : Set (ComplexSpace n)} {ρ β δ γ θ Θ : NNReal} {K M : ℝ} {a : ComplexSpace n → ℂ} {f : AnalyticPhaseFunction n G ρ} {g : ComplexSpace n → ComplexSpace n} (i : IterationInput a f g β δ γ θ Θ K M) : i.newDomain ⊆ i.wideDomain

noncomputable def KamProject.Arnold1963.IterationInput.newPerturbation {n : ℕ} {G Ω : Set (ComplexSpace n)} {ρ β δ γ θ Θ : NNReal} {K M : ℝ} {a : ComplexSpace n → ℂ} {f : AnalyticPhaseFunction n G ρ} {g : ComplexSpace n → ComplexSpace n} (i : IterationInput a f g β δ γ θ Θ K M) : AnalyticPhaseFunction n i.newDomain (ρ - 3 * γ)

The next perturbation restricted to the inductive action domain and angle strip.

Equations

• i.newPerturbation = i.wideResult.perturbation.restrict ⋯ ⋯ ⋯

theorem KamProject.Arnold1963.IterationInput.newPerturbation_bound {n : ℕ} {G Ω : Set (ComplexSpace n)} {ρ β δ γ θ Θ : NNReal} {K M : ℝ} {a : ComplexSpace n → ℂ} {f : AnalyticPhaseFunction n G ρ} {g : ComplexSpace n → ComplexSpace n} (i : IterationInput a f g β δ γ θ Θ K M) : i.newPerturbation.uniformNorm < iterationRemainderBound n M ↑δ ↑β

noncomputable def KamProject.Arnold1963.IterationInput.transformation {n : ℕ} {G Ω : Set (ComplexSpace n)} {ρ β δ γ θ Θ : NNReal} {K M : ℝ} {a : ComplexSpace n → ℂ} {f : AnalyticPhaseFunction n G ρ} {g : ComplexSpace n → ComplexSpace n} (i : IterationInput a f g β δ γ θ Θ K M) : AnalyticCanonicalTransformation (phaseDomain i.newDomain (ρ - 3 * γ)) (phaseDomain G ρ) ↑β

The inductive canonical transformation restricted to its retained phase domain.

Equations

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

theorem KamProject.Arnold1963.IterationInput.transformed_hamiltonian {n : ℕ} {G Ω : Set (ComplexSpace n)} {ρ β δ γ θ Θ : NNReal} {K M : ℝ} {a : ComplexSpace n → ℂ} {f : AnalyticPhaseFunction n G ρ} {g : ComplexSpace n → ComplexSpace n} (i : IterationInput a f g β δ γ θ Θ K M) (z : ComplexPhaseSpace n) : a (i.transformation.toFun z).1 + f.toFun (i.transformation.toFun z) = i.newIntegrable z.1 + i.newPerturbation.toFun z

theorem KamProject.Arnold1963.IterationInput.displacement_lt {n : ℕ} {G Ω : Set (ComplexSpace n)} {ρ β δ γ θ Θ : NNReal} {K M : ℝ} {a : ComplexSpace n → ℂ} {f : AnalyticPhaseFunction n G ρ} {g : ComplexSpace n → ComplexSpace n} (i : IterationInput a f g β δ γ θ Θ K M) {z : ComplexPhaseSpace n} (hz : z ∈ phaseDomain i.newDomain (ρ - 3 * γ)) : ‖i.transformation.toFun z - z‖ < ↑β

theorem KamProject.Arnold1963.IterationInput.remainder_derivative_bound {n : ℕ} {G Ω : Set (ComplexSpace n)} {ρ β δ γ θ Θ : NNReal} {K M : ℝ} {a : ComplexSpace n → ℂ} {f : AnalyticPhaseFunction n G ρ} {g : ComplexSpace n → ComplexSpace n} (i : IterationInput a f g β δ γ θ Θ K M) {z : ComplexPhaseSpace n} (hz : z ∈ phaseDomain i.newDomain (ρ - 3 * γ)) : ‖fderiv ℂ i.newPerturbation.toFun z‖ < iterationRemainderBound n M ↑δ ↑β / ↑β

theorem KamProject.Arnold1963.IterationInput.remainder_second_derivative_bound {n : ℕ} {G Ω : Set (ComplexSpace n)} {ρ β δ γ θ Θ : NNReal} {K M : ℝ} {a : ComplexSpace n → ℂ} {f : AnalyticPhaseFunction n G ρ} {g : ComplexSpace n → ComplexSpace n} (i : IterationInput a f g β δ γ θ Θ K M) {z : ComplexPhaseSpace n} (hz : z ∈ phaseDomain i.newDomain (ρ - 3 * γ)) (j k : Fin n ⊕ Fin n) : ‖((fderiv ℂ (fderiv ℂ i.newPerturbation.toFun) z) (phaseBasis j)) (phaseBasis k)‖ < 2 * iterationRemainderBound n M ↑δ ↑β / ↑β ^ 2

structure KamProject.Arnold1963.InductiveResult {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (a : ComplexSpace n → ℂ) (f : AnalyticPhaseFunction n G ρ) (Ω : Set (ComplexSpace n)) (β δ γ θ Θ : NNReal) (K M : ℝ) : Type

The updated frequency chart, canonical transformation and remainder of an inductive step.

• domain : Set (ComplexSpace n)

  The retained action domain of the inductive step.

• inverseFrequency : ComplexSpace n → ComplexSpace n

  The inverse of the updated action-frequency chart.

• chart : AnalyticFrequencyChart (actionFrequency (f.averagedHamiltonian a)) self.inverseFrequency self.domain (erosion (nonresonantDomain Ω id K (fundamentalCutoff (↑γ) (2 * M))) ((5 + 7 * Θ) * β))
• domain_subset : self.domain ⊆ erosion G β
• width_pos : 0 < ρ - 3 * γ
• analytic : AnalyticOnNhd ℂ (f.averagedHamiltonian a) self.domain
• conj (p : ComplexSpace n) : p ∈ self.domain → f.averagedHamiltonian a (conjVec p) = star (f.averagedHamiltonian a p)
• lower_pos : 0 < ↑θ * (1 - ↑δ)
• derivative_bounds (p : ComplexSpace n) : p ∈ self.domain → ∀ (v : ComplexSpace n), ↑θ * (1 - ↑δ) * ‖v‖ ≤ ‖(fderiv ℂ (actionFrequency (f.averagedHamiltonian a)) p) v‖ ∧ ‖(fderiv ℂ (actionFrequency (f.averagedHamiltonian a)) p) v‖ ≤ ↑Θ * (1 + ↑δ) * ‖v‖
• frequency_displacement (p : ComplexSpace n) : p ∈ self.domain → ‖actionFrequency (f.averagedHamiltonian a) p - actionFrequency a p‖ < ↑β * ↑δ
• transformation : AnalyticCanonicalTransformation (phaseDomain self.domain (ρ - 3 * γ)) (phaseDomain G ρ) ↑β

  The canonical transformation carrying the retained phase domain into the previous one.

• perturbation : AnalyticPhaseFunction n self.domain (ρ - 3 * γ)

  The analytic perturbation remainder after updating the integrable Hamiltonian.

• identity (z : ComplexPhaseSpace n) : a (self.transformation.toFun z).1 + f.toFun (self.transformation.toFun z) = f.averagedHamiltonian a z.1 + self.perturbation.toFun z
• bound : self.perturbation.uniformNorm < iterationRemainderBound n M ↑δ ↑β
• displacement_lt (z : ComplexPhaseSpace n) : z ∈ phaseDomain self.domain (ρ - 3 * γ) → ‖self.transformation.toFun z - z‖ < ↑β
• periodic (z : ComplexPhaseSpace n) : z ∈ phaseDomain self.domain (ρ - 3 * γ) → ∀ (k : FourierIndex n), self.transformation.toFun (phaseShift k z) = phaseShift k (self.transformation.toFun z)
• conj_compatible (z : ComplexPhaseSpace n) : z ∈ phaseDomain self.domain (ρ - 3 * γ) → self.transformation.toFun (conjPhase z) = conjPhase (self.transformation.toFun z)
• phase_buffer : phaseDomain self.domain (ρ - 3 * γ) ⊆ erosion (phaseDomain G ρ) β
• derivative (z : ComplexPhaseSpace n) : z ∈ phaseDomain self.domain (ρ - 3 * γ) → ‖fderiv ℂ self.perturbation.toFun z‖ < iterationRemainderBound n M ↑δ ↑β / ↑β
• second_derivative (z : ComplexPhaseSpace n) : z ∈ phaseDomain self.domain (ρ - 3 * γ) → ∀ (j k : Fin n ⊕ Fin n), ‖((fderiv ℂ (fderiv ℂ self.perturbation.toFun) z) (phaseBasis j)) (phaseBasis k)‖ < 2 * iterationRemainderBound n M ↑δ ↑β / ↑β ^ 2
• measure : realVolume (G \ self.domain) ≤ ENNReal.ofReal ((↑θ)⁻¹ ^ n) * realVolume (Ω \ erosion (nonresonantDomain Ω id K (fundamentalCutoff (↑γ) (2 * M))) ((6 + 7 * Θ) * β))

noncomputable def KamProject.Arnold1963.IterationInput.result {n : ℕ} {G Ω : Set (ComplexSpace n)} {ρ β δ γ θ Θ : NNReal} {K M : ℝ} {a : ComplexSpace n → ℂ} {f : AnalyticPhaseFunction n G ρ} {g : ComplexSpace n → ComplexSpace n} (i : IterationInput a f g β δ γ θ Θ K M) : InductiveResult a f Ω β δ γ θ Θ K M

The inductive-step result assembled from its verified input data.

Equations

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

theorem KamProject.Arnold1963.inductive_lemma {n : ℕ} {G Ω : Set (ComplexSpace n)} {ρ β δ γ θ Θ : NNReal} {K M : ℝ} {a : ComplexSpace n → ℂ} {f : AnalyticPhaseFunction n G ρ} {g : ComplexSpace n → ComplexSpace n} (i : IterationInput a f g β δ γ θ Θ K M) : Nonempty (InductiveResult a f Ω β δ γ θ Θ K M)