Global generating transformations on a fixed source, their analytic inverses, and estimates used by the next iteration step.

theorem KamProject.Arnold1963.canonicalAt_inverse_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, generatingOutput S (g z) = z) : CanonicalAt (generatingInput S ∘ g) y

def KamProject.Arnold1963.generatingSource {n : ℕ} (G U : Set (ComplexSpace n)) (r : NNReal) : Set (ComplexSpace n × ComplexSpace n)

The eroded phase source used to invert the generating input map.

Equations

• KamProject.Arnold1963.generatingSource G U r = KamProject.Arnold1963.erosion (G ×ˢ U) r

def KamProject.Arnold1963.generatingTarget {n : ℕ} (G U : Set (ComplexSpace n)) (r : NNReal) : Set (ComplexSpace n × ComplexSpace n)

The asymmetric action-angle erosion retained by the generating transformation.

Equations

• KamProject.Arnold1963.generatingTarget G U r = KamProject.Arnold1963.erosion G (r + r) ×ˢ KamProject.Arnold1963.erosion U (r + r + r)

noncomputable def KamProject.Arnold1963.generatingInverse {n : ℕ} (S : ComplexPhaseSpace n → ℂ) (G U : Set (ComplexSpace n)) (r : NNReal) (b : ComplexPhaseSpace n) : ComplexPhaseSpace n

A set-restricted inverse of the generating input map on its phase source.

Equations

• KamProject.Arnold1963.generatingInverse S G U r = Function.invFunOn (KamProject.Arnold1963.generatingInput S) (KamProject.Arnold1963.generatingSource G U r)

noncomputable def KamProject.Arnold1963.generatingTransform {n : ℕ} (S : ComplexPhaseSpace n → ℂ) (G U : Set (ComplexSpace n)) (r : NNReal) : ComplexPhaseSpace n → ComplexPhaseSpace n

The generating output map composed with the inverse generating input map.

Equations

• KamProject.Arnold1963.generatingTransform S G U r = KamProject.Arnold1963.generatingOutput S ∘ KamProject.Arnold1963.generatingInverse S G U r

noncomputable def KamProject.Arnold1963.generatingTransformInv {n : ℕ} (S : ComplexPhaseSpace n → ℂ) (G U : Set (ComplexSpace n)) (r : NNReal) : ComplexPhaseSpace n → ComplexPhaseSpace n

The reverse generating transformation obtained by inverting the generating output map.

Equations

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

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

Analyticity and smallness data ensuring the generating transformation is well defined.

• radius_pos : 0 < r
• analytic : AnalyticOnNhd ℂ S (G ×ˢ U)
• bounded : NormBoundOn S (G ×ˢ U) M
• small : M / ↑r / ↑r < 1 / 16

theorem KamProject.Arnold1963.GeneratingData.input_injOn {n : ℕ} {S : ComplexPhaseSpace n → ℂ} {G U : Set (ComplexSpace n)} {r : NNReal} {M : ℝ} (d : GeneratingData S G U r M) : Set.InjOn (generatingInput S) (generatingSource G U r)

theorem KamProject.Arnold1963.GeneratingData.output_injOn {n : ℕ} {S : ComplexPhaseSpace n → ℂ} {G U : Set (ComplexSpace n)} {r : NNReal} {M : ℝ} (d : GeneratingData S G U r M) : Set.InjOn (generatingOutput S) (generatingSource G U r)

theorem KamProject.Arnold1963.GeneratingData.inverse_eq_of_input {n : ℕ} {S : ComplexPhaseSpace n → ℂ} {G U : Set (ComplexSpace n)} {r : NNReal} {M : ℝ} (d : GeneratingData S G U r M) {x y : ComplexPhaseSpace n} (hx : x ∈ generatingSource G U r) (he : generatingInput S x = y) : generatingInverse S G U r y = x

theorem KamProject.Arnold1963.GeneratingData.inverse_spec {n : ℕ} {S : ComplexPhaseSpace n → ℂ} {G U : Set (ComplexSpace n)} {r : NNReal} {M : ℝ} (d : GeneratingData S G U r M) {y : ComplexPhaseSpace n} (hy : y ∈ generatingTarget G U r) : generatingInverse S G U r y ∈ erosion (G ×ˢ U) (r + r) ∧ generatingInput S (generatingInverse S G U r y) = y ∧ (generatingInverse S G U r y).1 = y.1 ∧ (generatingInverse S G U r y).2 ∈ Metric.closedBall y.2 ↑r

theorem KamProject.Arnold1963.GeneratingData.inverse_mem {n : ℕ} {S : ComplexPhaseSpace n → ℂ} {G U : Set (ComplexSpace n)} {r : NNReal} {M : ℝ} (d : GeneratingData S G U r M) {y : ComplexPhaseSpace n} (hy : y ∈ generatingTarget G U r) : generatingInverse S G U r y ∈ generatingSource G U r

theorem KamProject.Arnold1963.GeneratingData.inverse_analytic_right {n : ℕ} {S : ComplexPhaseSpace n → ℂ} {G U : Set (ComplexSpace n)} {r : NNReal} {M : ℝ} (d : GeneratingData S G U r M) {y : ComplexPhaseSpace n} (hy : y ∈ generatingTarget G U r) : AnalyticAt ℂ (generatingInverse S G U r) y ∧ ∀ᶠ (z : ComplexPhaseSpace n) in nhds y, generatingInput S (generatingInverse S G U r z) = z

theorem KamProject.Arnold1963.GeneratingData.transform_analytic {n : ℕ} {S : ComplexPhaseSpace n → ℂ} {G U : Set (ComplexSpace n)} {r : NNReal} {M : ℝ} (d : GeneratingData S G U r M) : AnalyticOnNhd ℂ (generatingTransform S G U r) (generatingTarget G U r)

theorem KamProject.Arnold1963.GeneratingData.transform_canonical {n : ℕ} {S : ComplexPhaseSpace n → ℂ} {G U : Set (ComplexSpace n)} {r : NNReal} {M : ℝ} (d : GeneratingData S G U r M) : CanonicalOn (generatingTransform S G U r) (generatingTarget G U r)

theorem KamProject.Arnold1963.GeneratingData.transform_bounds {n : ℕ} {S : ComplexPhaseSpace n → ℂ} {G U : Set (ComplexSpace n)} {r : NNReal} {M : ℝ} (d : GeneratingData S G U r M) {y : ComplexPhaseSpace n} (hy : y ∈ generatingTarget G U r) : ‖generatingTransform S G U r y - y‖ ≤ M / ↑r ∧ generatingTransform S G U r y ∈ G ×ˢ U

theorem KamProject.Arnold1963.GeneratingData.displacement_bound {n : ℕ} {S : ComplexPhaseSpace n → ℂ} {G U : Set (ComplexSpace n)} {r : NNReal} {M : ℝ} (d : GeneratingData S G U r M) : NormBoundOn (fun (y : ComplexPhaseSpace n) => generatingTransform S G U r y - y) (generatingTarget G U r) (M / ↑r)

theorem KamProject.Arnold1963.GeneratingData.transform_mapsTo {n : ℕ} {S : ComplexPhaseSpace n → ℂ} {G U : Set (ComplexSpace n)} {r : NNReal} {M : ℝ} (d : GeneratingData S G U r M) : Set.MapsTo (generatingTransform S G U r) (generatingTarget G U r) (G ×ˢ U)

theorem KamProject.Arnold1963.GeneratingData.derivative_bound {n : ℕ} {S : ComplexPhaseSpace n → ℂ} {G U : Set (ComplexSpace n)} {r : NNReal} {M : ℝ} (d : GeneratingData S G U r M) {y : ComplexPhaseSpace n} (hy : y ∈ generatingTarget G U r) : ‖fderiv ℂ (generatingTransform S G U r) y‖ ≤ 5 / 3

theorem KamProject.Arnold1963.GeneratingData.transform_injOn {n : ℕ} {S : ComplexPhaseSpace n → ℂ} {G U : Set (ComplexSpace n)} {r : NNReal} {M : ℝ} (d : GeneratingData S G U r M) : Set.InjOn (generatingTransform S G U r) (generatingTarget G U r)

theorem KamProject.Arnold1963.GeneratingData.transform_left_inv {n : ℕ} {S : ComplexPhaseSpace n → ℂ} {G U : Set (ComplexSpace n)} {r : NNReal} {M : ℝ} (d : GeneratingData S G U r M) {y : ComplexPhaseSpace n} (hy : y ∈ generatingTarget G U r) : generatingTransformInv S G U r (generatingTransform S G U r y) = y

theorem KamProject.Arnold1963.GeneratingData.transformInv_analytic {n : ℕ} {S : ComplexPhaseSpace n → ℂ} {G U : Set (ComplexSpace n)} {r : NNReal} {M : ℝ} (d : GeneratingData S G U r M) : AnalyticOnNhd ℂ (generatingTransformInv S G U r) (generatingTransform S G U r '' generatingTarget G U r)

theorem KamProject.Arnold1963.GeneratingData.transform_right_inv {n : ℕ} {S : ComplexPhaseSpace n → ℂ} {G U : Set (ComplexSpace n)} {r : NNReal} {M : ℝ} (d : GeneratingData S G U r M) {z : ComplexPhaseSpace n} (hz : z ∈ generatingTransform S G U r '' generatingTarget G U r) : generatingTransform S G U r (generatingTransformInv S G U r z) = z

theorem KamProject.Arnold1963.GeneratingData.transformInv_canonical {n : ℕ} {S : ComplexPhaseSpace n → ℂ} {G U : Set (ComplexSpace n)} {r : NNReal} {M : ℝ} (d : GeneratingData S G U r M) : CanonicalOn (generatingTransformInv S G U r) (generatingTransform S G U r '' generatingTarget G U r)

theorem KamProject.Arnold1963.GeneratingData.equations {n : ℕ} {S : ComplexPhaseSpace n → ℂ} {G U : Set (ComplexSpace n)} {r : NNReal} {M : ℝ} (d : GeneratingData S G U r M) {y : ComplexPhaseSpace n} (hy : y ∈ generatingTarget G U r) : (generatingTransform S G U r y).1 = y.1 + qGradient S (y.1, (generatingTransform S G U r y).2) ∧ y.2 = (generatingTransform S G U r y).2 + pGradient S (y.1, (generatingTransform S G U r y).2)