Periodicity on the complex cover and the real torus with period 2 * pi. Periodicity constrains values on the specified phase domain; arbitrary extensions outside that domain are immaterial.

@[reducible, inline]

abbrev KamProject.Arnold1963.RealTorus (n : ℕ) : Type

The real angle torus with period 2π in each coordinate.

Equations

• KamProject.Arnold1963.RealTorus n = (Fin n → AddCircle (2 * Real.pi))

@[reducible, inline]

abbrev KamProject.Arnold1963.RealPhaseSpace (n : ℕ) : Type

Real action coordinates paired with angles modulo 2π.

Equations

• KamProject.Arnold1963.RealPhaseSpace n = (KamProject.Arnold1963.RealSpace n × KamProject.Arnold1963.RealTorus n)

noncomputable def KamProject.Arnold1963.angleShift {n : ℕ} (k : FourierIndex n) : ComplexSpace n

The angle displacement associated with an integer multiple of each period.

Equations

• KamProject.Arnold1963.angleShift k = KamProject.Arnold1963.complexify fun (j : Fin n) => 2 * Real.pi * ↑(k j)

def KamProject.Arnold1963.AnglePeriodicOn {n : ℕ} (G : Set (ComplexSpace n)) (ρ : NNReal) (f : ComplexPhaseSpace n → ℂ) : Prop

Invariance of a phase function under integer angle-period shifts on its domain.

Equations

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

@[simp]

theorem KamProject.Arnold1963.imagPart_add_angleShift {n : ℕ} (q : ComplexSpace n) (k : FourierIndex n) : imagPart (q + angleShift k) = imagPart q

theorem KamProject.Arnold1963.add_angleShift_mem_iff {n : ℕ} (q : ComplexSpace n) (k : FourierIndex n) (ρ : NNReal) : q + angleShift k ∈ angleStrip n ρ ↔ q ∈ angleStrip n ρ