The real covering space and its quotient by the physical angle lattice.

@[reducible, inline]

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

Real action coordinates paired with unwrapped real angles.

Equations

• KamProject.Arnold1963.RealPhaseCover n = (KamProject.Arnold1963.RealSpace n × KamProject.Arnold1963.RealSpace n)

def KamProject.Arnold1963.complexifyPhase {n : ℕ} (x : RealPhaseCover n) : ComplexPhaseSpace n

Complexification of both real action and unwrapped angle coordinates.

Equations

• KamProject.Arnold1963.complexifyPhase x = (KamProject.Arnold1963.complexify x.1, KamProject.Arnold1963.complexify x.2)

def KamProject.Arnold1963.realPartPhase {n : ℕ} (x : ComplexPhaseSpace n) : RealPhaseCover n

Real-part projection of complex action and angle coordinates.

Equations

• KamProject.Arnold1963.realPartPhase x = (KamProject.Arnold1963.realPart x.1, KamProject.Arnold1963.realPart x.2)

@[simp]

theorem KamProject.Arnold1963.realPartPhase_complexifyPhase {n : ℕ} (x : RealPhaseCover n) : realPartPhase (complexifyPhase x) = x

theorem KamProject.Arnold1963.conjPhase_complexifyPhase {n : ℕ} (x : RealPhaseCover n) : conjPhase (complexifyPhase x) = complexifyPhase x

theorem KamProject.Arnold1963.complexify_realPart_of_conj {n : ℕ} {z : ComplexSpace n} (h : conjVec z = z) : complexify (realPart z) = z

theorem KamProject.Arnold1963.complexifyPhase_realPartPhase_of_conj {n : ℕ} {z : ComplexPhaseSpace n} (h : conjPhase z = z) : complexifyPhase (realPartPhase z) = z

noncomputable def KamProject.Arnold1963.realAngleShift {n : ℕ} (k : FourierIndex n) : RealSpace n

The real angle shift corresponding to integer multiples of the period.

Equations

• KamProject.Arnold1963.realAngleShift k j = 2 * Real.pi * ↑(k j)

noncomputable def KamProject.Arnold1963.realPhaseShift {n : ℕ} (k : FourierIndex n) (x : RealPhaseCover n) : RealPhaseCover n

Translation of unwrapped real phase space by an integer angle-period shift.

Equations

• KamProject.Arnold1963.realPhaseShift k x = (x.1, x.2 + KamProject.Arnold1963.realAngleShift k)

noncomputable def KamProject.Arnold1963.torusProjection {n : ℕ} (x : RealPhaseCover n) : RealPhaseSpace n

Projection from unwrapped real angles to angles modulo 2π.

Equations

• KamProject.Arnold1963.torusProjection x = (x.1, fun (j : Fin n) => ↑(x.2 j))

@[simp]

theorem KamProject.Arnold1963.torusProjection_shift {n : ℕ} (k : FourierIndex n) (x : RealPhaseCover n) : torusProjection (realPhaseShift k x) = torusProjection x

theorem KamProject.Arnold1963.torusProjection_eq_iff {n : ℕ} (x y : RealPhaseCover n) : torusProjection x = torusProjection y ↔ ∃ (k : FourierIndex n), x = realPhaseShift k y

theorem KamProject.Arnold1963.instFactLtRealOfNatHMulPi_leanPool : Fact (0 < 2 * Real.pi)

noncomputable def KamProject.Arnold1963.torusRepresentative {n : ℕ} (x : RealPhaseSpace n) : RealPhaseCover n

Representatives of real torus angles in the fundamental interval (0, 2π].

Equations

• KamProject.Arnold1963.torusRepresentative x = (x.1, fun (j : Fin n) => ↑((AddCircle.equivIoc (2 * Real.pi) 0) (x.2 j)))

@[simp]

theorem KamProject.Arnold1963.torusProjection_representative {n : ℕ} (x : RealPhaseSpace n) : torusProjection (torusRepresentative x) = x