Mixed-coordinate maps (P, q + S_P) and (P + S_q, q), and the Hessian symplectic identity.

noncomputable def KamProject.Arnold1963.generatingInput {n : ℕ} (S : ComplexPhaseSpace n → ℂ) (x : ComplexPhaseSpace n) : ComplexPhaseSpace n

The input coordinate map associated with a generating function.

Equations

• KamProject.Arnold1963.generatingInput S x = (x.1, x.2 + KamProject.Arnold1963.pGradient S x)

noncomputable def KamProject.Arnold1963.generatingOutput {n : ℕ} (S : ComplexPhaseSpace n → ℂ) (x : ComplexPhaseSpace n) : ComplexPhaseSpace n

The output coordinate map associated with a generating function.

Equations

• KamProject.Arnold1963.generatingOutput S x = (x.1 + KamProject.Arnold1963.qGradient S x, x.2)

theorem KamProject.Arnold1963.analyticAt_generatingInput {n : ℕ} {S : ComplexPhaseSpace n → ℂ} {x : ComplexPhaseSpace n} (hS : AnalyticAt ℂ S x) : AnalyticAt ℂ (generatingInput S) x

theorem KamProject.Arnold1963.analyticAt_generatingOutput {n : ℕ} {S : ComplexPhaseSpace n → ℂ} {x : ComplexPhaseSpace n} (hS : AnalyticAt ℂ S x) : AnalyticAt ℂ (generatingOutput S) x

theorem KamProject.Arnold1963.fderiv_generatingInput_apply {n : ℕ} {S : ComplexPhaseSpace n → ℂ} {x : ComplexPhaseSpace n} (hS : AnalyticAt ℂ S x) (v : ComplexPhaseSpace n) : (fderiv ℂ (generatingInput S) x) v = (v.1, v.2 + (fderiv ℂ (pGradient S) x) v)

theorem KamProject.Arnold1963.fderiv_generatingOutput_apply {n : ℕ} {S : ComplexPhaseSpace n → ℂ} {x : ComplexPhaseSpace n} (hS : AnalyticAt ℂ S x) (v : ComplexPhaseSpace n) : (fderiv ℂ (generatingOutput S) x) v = (v.1 + (fderiv ℂ (qGradient S) x) v, v.2)

theorem KamProject.Arnold1963.norm_fderiv_generatingInput_sub_id_le {n : ℕ} {S : ComplexPhaseSpace n → ℂ} {x : ComplexPhaseSpace n} (hS : AnalyticAt ℂ S x) : ‖fderiv ℂ (generatingInput S) x - ContinuousLinearMap.id ℂ (ComplexPhaseSpace n)‖ ≤ ‖fderiv ℂ (pGradient S) x‖

theorem KamProject.Arnold1963.norm_fderiv_generatingOutput_sub_id_le {n : ℕ} {S : ComplexPhaseSpace n → ℂ} {x : ComplexPhaseSpace n} (hS : AnalyticAt ℂ S x) : ‖fderiv ℂ (generatingOutput S) x - ContinuousLinearMap.id ℂ (ComplexPhaseSpace n)‖ ≤ ‖fderiv ℂ (qGradient S) x‖

theorem KamProject.Arnold1963.generating_symplectic_identity {n : ℕ} {S : ComplexPhaseSpace n → ℂ} {x : ComplexPhaseSpace n} (hS : AnalyticAt ℂ S x) (v w : ComplexPhaseSpace n) : symplecticForm ((fderiv ℂ (generatingOutput S) x) v) ((fderiv ℂ (generatingOutput S) x) w) = symplecticForm ((fderiv ℂ (generatingInput S) x) v) ((fderiv ℂ (generatingInput S) x) w)

theorem KamProject.Arnold1963.canonicalAt_generating_branch {n : ℕ} {S : ComplexPhaseSpace n → ℂ} {g : ComplexPhaseSpace n → ComplexPhaseSpace n} {y : ComplexPhaseSpace n} (hS : AnalyticAt ℂ S (g y)) (hg : AnalyticAt ℂ g y) (he : ∀ᶠ (z : ComplexPhaseSpace n) in nhds y, generatingInput S (g z) = z) : CanonicalAt (generatingOutput S ∘ g) y

theorem KamProject.Arnold1963.norm_fderiv_generating_branch_le {n : ℕ} {S : ComplexPhaseSpace n → ℂ} {g : ComplexPhaseSpace n → ComplexPhaseSpace n} {y : ComplexPhaseSpace n} (hS : AnalyticAt ℂ S (g y)) (hg : AnalyticAt ℂ g y) (he : ∀ᶠ (z : ComplexPhaseSpace n) in nhds y, generatingInput S (g z) = z) (hp : ‖fderiv ℂ (pGradient S) (g y)‖ ≤ 1 / 4) (hq : ‖fderiv ℂ (qGradient S) (g y)‖ ≤ 1 / 4) : ‖fderiv ℂ (generatingOutput S ∘ g) y‖ ≤ 5 / 3