The direct specification of one analytic invariant torus: center, frequency, lift, quotient embedding, inverse angle map, and all-time trajectories, realized by the same local limit.

structure KamProject.Arnold1963.KAMTorus (n : ℕ) (H₀ : ComplexSpace n → ℂ) (H₁ : ComplexPhaseSpace n → ℂ) (ambient : Set (ComplexSpace n)) (r : NNReal) (κ : ℝ) (T : Set (RealPhaseSpace n)) : Type

An analytic nonresonant torus with small displacement and original Hamiltonian trajectories.

• center : RealSpace n

  The real action center whose original frequency labels this torus.

• frequency : RealSpace n

  The nonresonant real frequency of the torus's uniform rotation.

• lift : ComplexSpace n → ComplexPhaseSpace n

  The analytic lift from complex angles to complex phase space.

• embedding : RealTorus n → RealPhaseSpace n

  The closed embedding of the real angle torus into real phase space.

• angleInverse : ComplexSpace n → ComplexSpace n

  The analytic inverse for the angle component of the torus lift at real points.

• center_mem : self.center ∈ realSlice ambient
• frequency_eq : actionFrequency H₀ (complexify self.center) = complexify self.frequency
• nonresonance (k : FourierIndex n) : k ≠ 0 → indexPairing k (complexify self.frequency) ≠ 0
• analytic : AnalyticOnNhd ℂ self.lift (angleStrip n r)
• periodic (q : ComplexSpace n) : q ∈ angleStrip n r → ∀ (k : FourierIndex n), self.lift (q + angleShift k) = phaseShift k (self.lift q)
• real_value (q : RealSpace n) : complexifyPhase (realPartPhase (self.lift (complexify q))) = self.lift (complexify q)
• embedding_lift (q : RealSpace n) : (self.embedding fun (j : Fin n) => ↑(q j)) = torusProjection (realPartPhase (self.lift (complexify q)))
• embedding_range : Set.range self.embedding = T
• closedEmbedding : Topology.IsClosedEmbedding self.embedding
• immersion (q : ComplexSpace n) : q ∈ angleStrip n r → Function.Injective ⇑(fderiv ℂ self.lift q)
• angle_homeomorph : ∃ (e : RealTorus n ≃ₜ RealTorus n), ∀ (Q : RealTorus n), e Q = (self.embedding Q).2
• inverse_analytic (Q : RealSpace n) : AnalyticAt ℂ self.angleInverse (complexify Q)
• inverse_left (q : RealSpace n) : self.angleInverse (self.lift (complexify q)).2 = complexify q
• inverse_right (Q : RealSpace n) : (self.lift (self.angleInverse (complexify Q))).2 = complexify Q
• displacement (q : ComplexSpace n) : q ∈ angleStrip n r → ‖(self.lift q).1 - complexify self.center‖ < κ ∧ ‖(self.lift q).2 - q‖ < κ
• orbit_equation (q : RealSpace n) (t : ℝ) : HasDerivAt (fun (u : ℝ) => self.lift (complexify (q + u • self.frequency))) (hamiltonianVectorField (fun (z : ComplexPhaseSpace n) => H₀ z.1 + H₁ z) (self.lift (complexify (q + t • self.frequency)))) t
• orbit_mem (q : RealSpace n) (t : ℝ) : torusProjection (realPartPhase (self.lift (complexify (q + t • self.frequency)))) ∈ T

noncomputable def KamProject.Arnold1963.FiniteLocalization.torusResult {n : ℕ} {H₀ : ComplexSpace n → ℂ} {ambient : Set (ComplexSpace n)} {ρ : NNReal} {κ : ℝ} (L : FiniteLocalization n H₀ ambient ρ κ) (f : AnalyticPhaseFunction n ambient ρ) (hf : f.uniformNorm ≤ L.threshold) (c : ↥L.patches) {p : RealSpace n} (hp : p ∈ realSlice (Iteration.InitialData.limitDomain ⋯ (L.data f hf c))) : KAMTorus n H₀ f.toFun ambient (L.width / 6) κ (Iteration.InitialData.invariantTorus ⋯ (L.data f hf c) p)

A realized invariant torus extracted from one local patch's limiting construction.

Equations

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