Local analytic canonical branches of the generating equation. The neighborhood is open in the ambient target space; the branch properties are conclusions of the construction.

theorem KamProject.Arnold1963.generating_small_of_arnold {n : ℕ} (hn : 0 < n) {r : NNReal} (hr : 0 < r) {M : ℝ} (hM : M < ↑r ^ 2 / (16 * ↑n)) : M / ↑r / ↑r < 1 / 4

structure KamProject.Arnold1963.GeneratingLocalBranch {n : ℕ} (S : ComplexPhaseSpace n → ℂ) (G U : Set (ComplexSpace n)) (r : NNReal) (M : ℝ) (y : ComplexPhaseSpace n) : Type

A local analytic inverse branch of the generating input map around a target point.

• inverse : ComplexPhaseSpace n → ComplexPhaseSpace n

  The local inverse function for the generating input map.

• neighborhood : Set (ComplexPhaseSpace n)

  The open target neighborhood on which the inverse branch is analytic.

• isOpen_neighborhood : IsOpen self.neighborhood
• center_mem : y ∈ self.neighborhood
• analytic_inverse : AnalyticOnNhd ℂ self.inverse self.neighborhood
• implicit_eq (z : ComplexPhaseSpace n) : z ∈ self.neighborhood → generatingInput S (self.inverse z) = z
• source_mem : Set.MapsTo self.inverse self.neighborhood (G ×ˢ U)
• analytic_transform : AnalyticOnNhd ℂ (generatingOutput S ∘ self.inverse) self.neighborhood
• canonical : CanonicalOn (generatingOutput S ∘ self.inverse) self.neighborhood
• mapsTo : Set.MapsTo (generatingOutput S ∘ self.inverse) self.neighborhood (G ×ˢ U)
• derivative_lt_two (z : ComplexPhaseSpace n) : z ∈ self.neighborhood → ‖fderiv ℂ (generatingOutput S ∘ self.inverse) z‖ < 2
• displacement_center : ‖generatingOutput S (self.inverse y) - y‖ ≤ M / ↑r
• root_in_ball : (self.inverse y).2 ∈ Metric.closedBall y.2 ↑r

theorem KamProject.Arnold1963.exists_generatingLocalBranch {n : ℕ} {S : ComplexPhaseSpace n → ℂ} {G U : Set (ComplexSpace n)} {r : NNReal} {M : ℝ} {P Q : ComplexSpace n} (hr : 0 < r) (hS : AnalyticOnNhd ℂ S (G ×ˢ U)) (hM : NormBoundOn S (G ×ˢ U) M) (hsmall : M / ↑r / ↑r < 1 / 4) (hP : P ∈ erosion G (r + r)) (hQ : Q ∈ erosion U (r + r + r)) : Nonempty (GeneratingLocalBranch S G U r M (P, Q))

theorem KamProject.Arnold1963.AnalyticPhaseFunction.exists_generatingLocalBranch {n : ℕ} {G : Set (ComplexSpace n)} {ρ r : NNReal} (S : AnalyticPhaseFunction n G ρ) (hr : 0 < r) (hsmall : S.uniformNorm / ↑r / ↑r < 1 / 4) {P Q : ComplexSpace n} (hP : P ∈ erosion G (r + r)) (hQ : Q ∈ erosion (angleStrip n ρ) (r + r + r)) : Nonempty (GeneratingLocalBranch S.toFun G (angleStrip n ρ) r S.uniformNorm (P, Q))

theorem KamProject.Arnold1963.generatingLocalBranch_center_unique {n : ℕ} {S : ComplexPhaseSpace n → ℂ} {G U : Set (ComplexSpace n)} {r : NNReal} {M : ℝ} {P Q : ComplexSpace n} (hr : 0 < r) (hS : AnalyticOnNhd ℂ S (G ×ˢ U)) (hM : NormBoundOn S (G ×ˢ U) M) (hsmall : M / ↑r / ↑r < 1) (hP : P ∈ erosion G (r + r)) (hQ : Q ∈ erosion U (r + r + r)) (b c : GeneratingLocalBranch S G U r M (P, Q)) : b.inverse (P, Q) = c.inverse (P, Q)

noncomputable def KamProject.Arnold1963.GeneratingLocalBranch.transform {n : ℕ} {S : ComplexPhaseSpace n → ℂ} {G U : Set (ComplexSpace n)} {r : NNReal} {M : ℝ} {y : ComplexPhaseSpace n} (b : GeneratingLocalBranch S G U r M y) : ComplexPhaseSpace n → ComplexPhaseSpace n

The generating output map evaluated through the local inverse branch.

Equations

• b.transform = KamProject.Arnold1963.generatingOutput S ∘ b.inverse

theorem KamProject.Arnold1963.GeneratingLocalBranch.equations {n : ℕ} {S : ComplexPhaseSpace n → ℂ} {G U : Set (ComplexSpace n)} {r : NNReal} {M : ℝ} {y : ComplexPhaseSpace n} (b : GeneratingLocalBranch S G U r M y) {z : ComplexPhaseSpace n} (hz : z ∈ b.neighborhood) : (b.transform z).1 = z.1 + qGradient S (z.1, (b.transform z).2) ∧ z.2 = (b.transform z).2 + pGradient S (z.1, (b.transform z).2)