noncomputable def SymplecticGeometry.AlternatingMap.scalarWedge {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {m k : ℕ} (ω : E [⋀^Fin m]→ₗ[ℝ] ℝ) (η : E [⋀^Fin k]→ₗ[ℝ] ℝ) : E [⋀^Fin (m + k)]→ₗ[ℝ] ℝ

The wedge product $\omega \wedge \eta$ of two scalar-valued alternating forms, producing an alternating $(m + k)$-form on $E$.

noncomputable def SymplecticGeometry.AlternatingMap.wedgePower {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (ω : E [⋀^Fin 2]→ₗ[ℝ] ℝ) (n : ℕ) : E [⋀^Fin (2 * n)]→ₗ[ℝ] ℝ

The $n$-th wedge power $\omega^{\wedge n} = \underbrace{\omega \wedge \cdots \wedge \omega}_{n}$ of a $2$-form, yielding a $2n$-form.

structure SymplecticGeometry.SymplecticManifold (n : ℕ) (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℝ E] : Type u_1

A symplectic manifold of dimension $2n$: a $2$-form $\omega$ on $E$ that is closed ($d\omega = 0$) and nondegenerate (the top wedge $\omega^n$ is a volume form).

• ω : E → E [⋀^Fin 2]→L[ℝ] ℝ
• dim_eq : Module.finrank ℝ E = 2 * n
• closed (x : E) : extDeriv self.ω x = 0
• nondegenerate (x : E) : AlternatingMap.wedgePower (self.ω x).toAlternatingMap n ≠ 0

noncomputable def SymplecticGeometry.SymplecticManifold.flat {n : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (S : SymplecticManifold n E) (x : E) : E →L[ℝ] E [⋀^Fin 1]→L[ℝ] ℝ

The musical isomorphism $\flat : T_xE \to T^*_xE$ at $x$, sending $v$ to $\omega_x(v, \cdot)$.

theorem SymplecticGeometry.SymplecticManifold.map_perm {n : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (S : SymplecticManifold n E) (x : E) (v : Fin 2 → E) (σ : Equiv.Perm (Fin 2)) : (S.ω x) (v ∘ ⇑σ) = Equiv.Perm.sign σ • (S.ω x) v

Antisymmetry of $\omega_x$: permuting inputs by $\sigma$ multiplies by $\mathrm{sgn}(\sigma)$.

theorem SymplecticGeometry.SymplecticManifold.isClosed {n : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (S : SymplecticManifold n E) (x : E) : extDeriv S.ω x = 0

A symplectic form is closed: $d\omega = 0$ at every point $x$.

theorem SymplecticGeometry.SymplecticManifold.isNondegenerate {n : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (S : SymplecticManifold n E) (x : E) : AlternatingMap.wedgePower (S.ω x).toAlternatingMap n ≠ 0

Nondegeneracy: the top wedge power $\omega_x^n$ is nonzero at every $x$.