Coordinate matrices for the symplectic form. The matrix identity uses ordinary transpose, rather than conjugate transpose, and the same (p, q) coordinate order.

theorem KamProject.Arnold1963.symplecticMatrix_eq_neg_mathlibJ (n : ℕ) : symplecticMatrix n = -Matrix.J (Fin n) ℂ

theorem KamProject.Arnold1963.symplectic_matrix_identity_iff_mathlib {n : ℕ} (M : Matrix (Fin n ⊕ Fin n) (Fin n ⊕ Fin n) ℂ) : M.transpose * symplecticMatrix n * M = symplecticMatrix n ↔ M.transpose * Matrix.J (Fin n) ℂ * M = Matrix.J (Fin n) ℂ

def KamProject.Arnold1963.phaseCoordinate {n : ℕ} (v : ComplexPhaseSpace n) : Fin n ⊕ Fin n → ℂ

The unified coordinate function of a phase vector.

Equations

• KamProject.Arnold1963.phaseCoordinate v = Sum.elim v.1 v.2

def KamProject.Arnold1963.phaseLinearMatrix {n : ℕ} (A : ComplexPhaseSpace n →ₗ[ℂ] ComplexPhaseSpace n) : Matrix (Fin n ⊕ Fin n) (Fin n ⊕ Fin n) ℂ

The matrix of a linear phase transformation in the unified coordinate basis.

Equations

• KamProject.Arnold1963.phaseLinearMatrix A i j = KamProject.Arnold1963.phaseCoordinate (A (KamProject.Arnold1963.phaseDirection j)) i

theorem KamProject.Arnold1963.phaseLinearMatrix_symplectic_apply {n : ℕ} (A : ComplexPhaseSpace n →ₗ[ℂ] ComplexPhaseSpace n) (i j : Fin n ⊕ Fin n) : ((phaseLinearMatrix A).transpose * symplecticMatrix n * phaseLinearMatrix A) i j = symplecticForm (A (phaseDirection i)) (A (phaseDirection j))

theorem KamProject.Arnold1963.IsSymplecticLinear.matrix_identity {n : ℕ} {A : ComplexPhaseSpace n →ₗ[ℂ] ComplexPhaseSpace n} (hA : IsSymplecticLinear A) : (phaseLinearMatrix A).transpose * symplecticMatrix n * phaseLinearMatrix A = symplecticMatrix n