Analytic canonical transformations on shrunken domains and analytic Hamiltonian pullbacks.

theorem KamProject.Arnold1963.phaseDomain_subset_generatingTarget {n : ℕ} (G : Set (ComplexSpace n)) {ρ r : NNReal} (hρ : r + r + r ≤ ρ) : phaseDomain (erosion G (r + r)) (ρ - (r + r + r)) ⊆ generatingTarget G (angleStrip n ρ) r

structure KamProject.Arnold1963.AnalyticCanonicalTransformation {n : ℕ} (D V : Set (ComplexPhaseSpace n)) (ε : ℝ) : Type

An analytic canonical transformation with analytic inverse and displacement control.

• toFun : ComplexPhaseSpace n → ComplexPhaseSpace n

  The forward complex phase transformation.

• invFun : ComplexPhaseSpace n → ComplexPhaseSpace n

  The inverse function on the forward transformation's image.

• analytic : AnalyticOnNhd ℂ self.toFun D
• inverse_analytic : AnalyticOnNhd ℂ self.invFun (self.toFun '' D)
• mapsTo : Set.MapsTo self.toFun D V
• left_inv : Set.LeftInvOn self.invFun self.toFun D
• right_inv : Set.RightInvOn self.invFun self.toFun (self.toFun '' D)
• inverse_mapsTo : Set.MapsTo self.invFun (self.toFun '' D) D
• canonical : CanonicalOn self.toFun D
• inverse_canonical : CanonicalOn self.invFun (self.toFun '' D)
• displacement : NormBoundOn (fun (x : ComplexPhaseSpace n) => self.toFun x - x) D ε
• derivative_bound (x : ComplexPhaseSpace n) : x ∈ D → ‖fderiv ℂ self.toFun x‖ < 2

theorem KamProject.Arnold1963.AnalyticCanonicalTransformation.injOn {n : ℕ} {D V : Set (ComplexPhaseSpace n)} {ε : ℝ} (B : AnalyticCanonicalTransformation D V ε) : Set.InjOn B.toFun D

theorem KamProject.Arnold1963.AnalyticCanonicalTransformation.bijOn_image {n : ℕ} {D V : Set (ComplexPhaseSpace n)} {ε : ℝ} (B : AnalyticCanonicalTransformation D V ε) : Set.BijOn B.toFun D (B.toFun '' D)

def KamProject.Arnold1963.AnalyticCanonicalTransformation.homeomorph {n : ℕ} {D V : Set (ComplexPhaseSpace n)} {ε : ℝ} (B : AnalyticCanonicalTransformation D V ε) : ↑D ≃ₜ ↑(B.toFun '' D)

The transformation as a homeomorphism between its source and its actual image.

Equations

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

def KamProject.Arnold1963.AnalyticCanonicalTransformation.restrict {n : ℕ} {D V : Set (ComplexPhaseSpace n)} {ε : ℝ} (B : AnalyticCanonicalTransformation D V ε) {D' : Set (ComplexPhaseSpace n)} (hD : D' ⊆ D) : AnalyticCanonicalTransformation D' V ε

Restriction of the canonical transformation to a smaller source domain.

Equations

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

theorem KamProject.Arnold1963.GeneratingData.of_arnold {n : ℕ} {S : ComplexPhaseSpace n → ℂ} {G U : Set (ComplexSpace n)} {r : NNReal} {M : ℝ} (hn : 0 < n) (hr : 0 < r) (hS : AnalyticOnNhd ℂ S (G ×ˢ U)) (hb : NormBoundOn S (G ×ˢ U) M) (hM : M < ↑r ^ 2 / (16 * ↑n)) : GeneratingData S G U r M

noncomputable def KamProject.Arnold1963.GeneratingData.transformation {n : ℕ} {S : ComplexPhaseSpace n → ℂ} {G U : Set (ComplexSpace n)} {r : NNReal} {M : ℝ} (d : GeneratingData S G U r M) : AnalyticCanonicalTransformation (generatingTarget G U r) (G ×ˢ U) (M / ↑r)

The canonical transformation constructed from analytic generating data.

Equations

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

theorem KamProject.Arnold1963.GeneratingData.action_displacement {n : ℕ} {S : ComplexPhaseSpace n → ℂ} {G U : Set (ComplexSpace n)} {r : NNReal} {M : ℝ} (d : GeneratingData S G U r M) {δ : NNReal} (hδ : 0 < δ) {y : ComplexPhaseSpace n} (hP : y.1 ∈ erosion G (r + r)) (hQ : y.2 ∈ erosion U (r + r + r + δ)) : ‖(generatingTransform S G U r y).1 - y.1‖ ≤ M / ↑δ

theorem KamProject.Arnold1963.AnalyticPhaseFunction.generatingData {n : ℕ} {G : Set (ComplexSpace n)} {ρ r : NNReal} (S : AnalyticPhaseFunction n G ρ) (hn : 0 < n) (hr : 0 < r) (hM : S.uniformNorm < ↑r ^ 2 / (16 * ↑n)) : GeneratingData S.toFun G (angleStrip n ρ) r S.uniformNorm

noncomputable def KamProject.Arnold1963.AnalyticPhaseFunction.pullbackGenerating {n : ℕ} {G : Set (ComplexSpace n)} {ρ r : NNReal} {M : ℝ} (H S : AnalyticPhaseFunction n G ρ) (d : GeneratingData S.toFun G (angleStrip n ρ) r M) (hρ : r + r + r ≤ ρ) : AnalyticPhaseFunction n (erosion G (r + r)) (ρ - (r + r + r))

Pullback of an analytic Hamiltonian through a generating transformation on a smaller domain.

Equations

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

theorem KamProject.Arnold1963.AnalyticPhaseFunction.uniformNorm_pullbackGenerating_le {n : ℕ} {G : Set (ComplexSpace n)} {ρ r : NNReal} {M : ℝ} (H S : AnalyticPhaseFunction n G ρ) (d : GeneratingData S.toFun G (angleStrip n ρ) r M) (hρ : r + r + r ≤ ρ) : (H.pullbackGenerating S d hρ).uniformNorm ≤ H.uniformNorm