The standard symplectic form in (p, q) coordinates, its nondegeneracy, and covector duality. Symplecticity means preservation of this concrete bilinear form; it implies linear invertibility.

def KamProject.Arnold1963.pDirection {n : ℕ} (j : Fin n) : ComplexPhaseSpace n

The action-coordinate basis direction in phase space.

Equations

• KamProject.Arnold1963.pDirection j = (Pi.single j 1, 0)

def KamProject.Arnold1963.qDirection {n : ℕ} (j : Fin n) : ComplexPhaseSpace n

The angle-coordinate basis direction in phase space.

Equations

• KamProject.Arnold1963.qDirection j = (0, Pi.single j 1)

@[simp]

theorem KamProject.Arnold1963.norm_pDirection {n : ℕ} (j : Fin n) : ‖pDirection j‖ = 1

@[simp]

theorem KamProject.Arnold1963.norm_qDirection {n : ℕ} (j : Fin n) : ‖qDirection j‖ = 1

def KamProject.Arnold1963.symplecticForm {n : ℕ} (v w : ComplexPhaseSpace n) : ℂ

The standard complex symplectic form in action-angle coordinates.

Equations

• KamProject.Arnold1963.symplecticForm v w = ∑ j : Fin n, (v.1 j * w.2 j - v.2 j * w.1 j)

theorem KamProject.Arnold1963.phase_decomposition {n : ℕ} (v : ComplexPhaseSpace n) : v = ∑ j : Fin n, v.1 j • pDirection j + ∑ j : Fin n, v.2 j • qDirection j

@[simp]

theorem KamProject.Arnold1963.symplecticForm_pDirection {n : ℕ} (j : Fin n) (w : ComplexPhaseSpace n) : symplecticForm (pDirection j) w = w.2 j

@[simp]

theorem KamProject.Arnold1963.symplecticForm_qDirection {n : ℕ} (j : Fin n) (w : ComplexPhaseSpace n) : symplecticForm (qDirection j) w = -w.1 j

theorem KamProject.Arnold1963.symplecticForm_skew {n : ℕ} (v w : ComplexPhaseSpace n) : symplecticForm v w = -symplecticForm w v

@[simp]

theorem KamProject.Arnold1963.symplecticForm_self {n : ℕ} (v : ComplexPhaseSpace n) : symplecticForm v v = 0

theorem KamProject.Arnold1963.symplecticForm_add_left {n : ℕ} (u v w : ComplexPhaseSpace n) : symplecticForm (u + v) w = symplecticForm u w + symplecticForm v w

theorem KamProject.Arnold1963.symplecticForm_smul_left {n : ℕ} (c : ℂ) (v w : ComplexPhaseSpace n) : symplecticForm (c • v) w = c * symplecticForm v w

theorem KamProject.Arnold1963.symplecticForm_ext_right {n : ℕ} {u w : ComplexPhaseSpace n} (h : ∀ (v : ComplexPhaseSpace n), symplecticForm v u = symplecticForm v w) : u = w

def KamProject.Arnold1963.symplecticSharp {n : ℕ} (L : ComplexPhaseSpace n →ₗ[ℂ] ℂ) : ComplexPhaseSpace n

The phase vector associated with a linear functional by the symplectic form.

Equations

• KamProject.Arnold1963.symplecticSharp L = (fun (j : Fin n) => -L (KamProject.Arnold1963.qDirection j), fun (j : Fin n) => L (KamProject.Arnold1963.pDirection j))

theorem KamProject.Arnold1963.linearForm_decomposition {n : ℕ} (L : ComplexPhaseSpace n →ₗ[ℂ] ℂ) (v : ComplexPhaseSpace n) : L v = ∑ j : Fin n, v.1 j * L (pDirection j) + ∑ j : Fin n, v.2 j * L (qDirection j)

theorem KamProject.Arnold1963.symplecticForm_sharp {n : ℕ} (L : ComplexPhaseSpace n →ₗ[ℂ] ℂ) (v : ComplexPhaseSpace n) : symplecticForm v (symplecticSharp L) = L v

def KamProject.Arnold1963.IsSymplecticLinear {n : ℕ} (A : ComplexPhaseSpace n →ₗ[ℂ] ComplexPhaseSpace n) : Prop

Preservation of the standard symplectic form by a linear phase transformation.

Equations

• KamProject.Arnold1963.IsSymplecticLinear A = ∀ (v w : KamProject.Arnold1963.ComplexPhaseSpace n), KamProject.Arnold1963.symplecticForm (A v) (A w) = KamProject.Arnold1963.symplecticForm v w

theorem KamProject.Arnold1963.IsSymplecticLinear.injective {n : ℕ} {A : ComplexPhaseSpace n →ₗ[ℂ] ComplexPhaseSpace n} (hA : IsSymplecticLinear A) : Function.Injective ⇑A

theorem KamProject.Arnold1963.IsSymplecticLinear.surjective {n : ℕ} {A : ComplexPhaseSpace n →ₗ[ℂ] ComplexPhaseSpace n} (hA : IsSymplecticLinear A) : Function.Surjective ⇑A

theorem KamProject.Arnold1963.IsSymplecticLinear.comp {n : ℕ} {A B : ComplexPhaseSpace n →ₗ[ℂ] ComplexPhaseSpace n} (hA : IsSymplecticLinear A) (hB : IsSymplecticLinear B) : IsSymplecticLinear (A ∘ₗ B)

theorem KamProject.Arnold1963.IsSymplecticLinear.map_sharp_comp {n : ℕ} {A : ComplexPhaseSpace n →ₗ[ℂ] ComplexPhaseSpace n} (hA : IsSymplecticLinear A) (L : ComplexPhaseSpace n →ₗ[ℂ] ℂ) : A (symplecticSharp (L ∘ₗ A)) = symplecticSharp L

def KamProject.Arnold1963.phaseDirection {n : ℕ} : Fin n ⊕ Fin n → ComplexPhaseSpace n

A unified action-angle basis indexed by the disjoint union of coordinate indices.

Equations

• KamProject.Arnold1963.phaseDirection (Sum.inl j) = KamProject.Arnold1963.pDirection j
• KamProject.Arnold1963.phaseDirection (Sum.inr j) = KamProject.Arnold1963.qDirection j

def KamProject.Arnold1963.symplecticMatrix (n : ℕ) : Matrix (Fin n ⊕ Fin n) (Fin n ⊕ Fin n) ℂ

The matrix of the chosen symplectic sign convention in the unified phase basis.

Equations

• KamProject.Arnold1963.symplecticMatrix n = -Matrix.J (Fin n) ℂ

@[simp]

theorem KamProject.Arnold1963.symplecticMatrix_pp {n : ℕ} (i j : Fin n) : symplecticMatrix n (Sum.inl i) (Sum.inl j) = 0

@[simp]

theorem KamProject.Arnold1963.symplecticMatrix_pq {n : ℕ} (i j : Fin n) : symplecticMatrix n (Sum.inl i) (Sum.inr j) = if i = j then 1 else 0

@[simp]

theorem KamProject.Arnold1963.symplecticMatrix_qp {n : ℕ} (i j : Fin n) : symplecticMatrix n (Sum.inr i) (Sum.inl j) = -if i = j then 1 else 0

@[simp]

theorem KamProject.Arnold1963.symplecticMatrix_qq {n : ℕ} (i j : Fin n) : symplecticMatrix n (Sum.inr i) (Sum.inr j) = 0

theorem KamProject.Arnold1963.symplecticMatrix_apply {n : ℕ} (i j : Fin n ⊕ Fin n) : symplecticMatrix n i j = symplecticForm (phaseDirection i) (phaseDirection j)