The real and complex coordinate spaces use the maximum norm. Phase coordinates are ordered (p, q). Fourier indices use the sum of absolute coordinates, separately from the ambient norm.

@[reducible, inline]

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

Real coordinate space with the supremum norm.

Equations

• KamProject.Arnold1963.RealSpace n = (Fin n → ℝ)

@[reducible, inline]

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

Complex coordinate space with the supremum norm.

Equations

• KamProject.Arnold1963.ComplexSpace n = (Fin n → ℂ)

@[reducible, inline]

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

Integer Fourier indices for the angle coordinates.

Equations

• KamProject.Arnold1963.FourierIndex n = (Fin n → ℤ)

@[reducible, inline]

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

Complex action coordinates paired with complex angle coordinates.

Equations

• KamProject.Arnold1963.ComplexPhaseSpace n = (KamProject.Arnold1963.ComplexSpace n × KamProject.Arnold1963.ComplexSpace n)

def KamProject.Arnold1963.complexify {n : ℕ} (x : RealSpace n) : ComplexSpace n

Coordinatewise embedding of real vectors into complex coordinate space.

Equations

• KamProject.Arnold1963.complexify x j = ↑(x j)

@[simp]

theorem KamProject.Arnold1963.complexify_zero {n : ℕ} : complexify 0 = 0

theorem KamProject.Arnold1963.isometry_complexify (n : ℕ) : Isometry complexify

theorem KamProject.Arnold1963.continuous_complexify (n : ℕ) : Continuous complexify

def KamProject.Arnold1963.conjVec {n : ℕ} (z : ComplexSpace n) : ComplexSpace n

Coordinatewise complex conjugation of an action or angle vector.

Equations

• KamProject.Arnold1963.conjVec z j = star (z j)

def KamProject.Arnold1963.realPart {n : ℕ} (z : ComplexSpace n) : RealSpace n

Coordinatewise real part of a complex vector.

Equations

• KamProject.Arnold1963.realPart z j = (z j).re

def KamProject.Arnold1963.imagPart {n : ℕ} (z : ComplexSpace n) : RealSpace n

Coordinatewise imaginary part of a complex vector.

Equations

• KamProject.Arnold1963.imagPart z j = (z j).im

def KamProject.Arnold1963.conjPhase {n : ℕ} (z : ComplexPhaseSpace n) : ComplexPhaseSpace n

Coordinatewise conjugation of both action and angle components.

Equations

• KamProject.Arnold1963.conjPhase z = (KamProject.Arnold1963.conjVec z.1, KamProject.Arnold1963.conjVec z.2)

@[simp]

theorem KamProject.Arnold1963.conjPhase_eq_star {n : ℕ} (x : ComplexPhaseSpace n) : conjPhase x = star x

@[simp]

theorem KamProject.Arnold1963.conjVec_eq_star {n : ℕ} (x : ComplexSpace n) : conjVec x = star x

@[simp]

theorem KamProject.Arnold1963.star_complexify {n : ℕ} (x : RealSpace n) : star (complexify x) = complexify x

def KamProject.Arnold1963.indexLength {n : ℕ} (k : FourierIndex n) : ℝ

The real-valued sum of absolute Fourier coordinates.

Equations

• KamProject.Arnold1963.indexLength k = ∑ j : Fin n, |↑(k j)|

def KamProject.Arnold1963.indexPairing {n : ℕ} (k : FourierIndex n) (z : ComplexSpace n) : ℂ

The bilinear pairing of an integer Fourier index with a complex vector.

Equations

• KamProject.Arnold1963.indexPairing k z = ∑ j : Fin n, ↑(k j) * z j

theorem KamProject.Arnold1963.complex_norm_le_iff {n : ℕ} (z : ComplexSpace n) {r : ℝ} (hr : 0 ≤ r) : ‖z‖ ≤ r ↔ ∀ (j : Fin n), ‖z j‖ ≤ r

theorem KamProject.Arnold1963.real_norm_le_iff {n : ℕ} (x : RealSpace n) {r : ℝ} (hr : 0 ≤ r) : ‖x‖ ≤ r ↔ ∀ (j : Fin n), |x j| ≤ r

@[simp]

theorem KamProject.Arnold1963.norm_complexify {n : ℕ} (x : RealSpace n) : ‖complexify x‖ = ‖x‖

theorem KamProject.Arnold1963.complex_coordinate_norm_le {n : ℕ} (z : ComplexSpace n) (j : Fin n) : ‖z j‖ ≤ ‖z‖

theorem KamProject.Arnold1963.phase_norm_eq {n : ℕ} (z : ComplexPhaseSpace n) : ‖z‖ = max ‖z.1‖ ‖z.2‖

@[simp]

theorem KamProject.Arnold1963.realPart_complexify {n : ℕ} (x : RealSpace n) : realPart (complexify x) = x

@[simp]

theorem KamProject.Arnold1963.imagPart_complexify {n : ℕ} (x : RealSpace n) : imagPart (complexify x) = 0

theorem KamProject.Arnold1963.conjVec_complexify {n : ℕ} (x : RealSpace n) : conjVec (complexify x) = complexify x

theorem KamProject.Arnold1963.conjVec_conjVec {n : ℕ} (z : ComplexSpace n) : conjVec (conjVec z) = z

theorem KamProject.Arnold1963.indexLength_nonneg {n : ℕ} (k : FourierIndex n) : 0 ≤ indexLength k

theorem KamProject.Arnold1963.norm_indexPairing_le {n : ℕ} (k : FourierIndex n) (z : ComplexSpace n) : ‖indexPairing k z‖ ≤ indexLength k * ‖z‖