Symplectic coordinate equivalences to standard Euclidean space

Given a real vector space V equipped with a basis indexed by ι ⊕ ι (in the Matrix.J block convention) or by Fin n × Fin 2 (in the interleaved Darboux convention of TauCeti.SymplecticForm.IsDarbouxBasis), this file constructs the coordinate isomorphism from V to the doubled Euclidean model EuclideanSpace ℝ ι × EuclideanSpace ℝ ι carrying b (inr a) (or b (i, 0)) to (EuclideanSpace.single a 1, 0) and b (inl a) (or b (i, 1)) to (0, EuclideanSpace.single a 1).

Because both Matrix.J (ω (b (inr a)) (b (inl a)) = 1) and TauCeti.stdSymplecticForm (ω₀ ((single a 1, 0), (0, single a 1)) = 1) give +1 to that ordered pair, this coordinate equivalence is a linear symplectomorphism from (V, ω) to (EuclideanSpace ℝ ι × EuclideanSpace ℝ ι, stdSymplecticForm) if and only if the matrix of ω in b is Matrix.J (respectively, b is a Darboux basis of ω).

On a normed space V, finite-dimensionality is automatic from the finite basis, upgrading both equivalences to continuous linear equivalences. Combined with LinearMap.BilinForm.IsAlt.exists_basis_apply_eq_J_inl_zero_eq, any nonzero vector in a finite-dimensional symplectic vector space can be sent to either (0, EuclideanSpace.single 0 1) or (EuclideanSpace.single 0 1, 0) by a continuous-linear symplectomorphism onto the standard Euclidean model.

Main declarations

• TauCeti.stdSymplecticBasis: the standard ι ⊕ ι-indexed basis of EuclideanSpace ℝ ι × EuclideanSpace ℝ ι in which stdSymplecticForm has matrix Matrix.J.
• TauCeti.stdDarbouxBasis: the standard Fin n × Fin 2-indexed Darboux basis of EuclideanSpace ℝ (Fin n) × EuclideanSpace ℝ (Fin n).
• TauCeti.fact_finrank_euclideanSpace_prod: the instance recording that EuclideanSpace ℝ ι × EuclideanSpace ℝ ι has dimension 2 * Fintype.card ι.
• Module.Basis.euclideanBasisEquiv / Module.Basis.euclideanBasisContinuousLinearEquiv: coordinate isomorphism from an ι ⊕ ι-indexed basis to EuclideanSpace ℝ ι × EuclideanSpace ℝ ι.
• Module.Basis.darbouxBasisEquiv / Module.Basis.darbouxBasisContinuousLinearEquiv: coordinate isomorphism from a Fin n × Fin 2-indexed basis to EuclideanSpace ℝ (Fin n) × EuclideanSpace ℝ (Fin n).
• TauCeti.SymplecticForm.isSymplectomorphism_euclideanBasisEquiv_iff and TauCeti.SymplecticForm.isSymplectomorphism_darbouxBasisEquiv_iff: necessary and sufficient conditions for these coordinate maps to intertwine ω with stdSymplecticForm.
• TauCeti.SymplecticForm.exists_isSymplectomorphism_stdSymplecticForm, TauCeti.SymplecticForm.exists_continuousLinearEquiv_stdSymplecticForm, and their fixed-dimension and vector-straightening variants (_of_finrank_eq, _apply_eq_snd_single, _apply_eq_fst_single): linear and continuous-linear symplectomorphisms onto the standard Euclidean model, optionally straightening a prescribed nonzero vector.

References

• D. McDuff and D. Salamon, Introduction to Symplectic Topology, 3rd ed., Oxford, 2017, Sections 2.1 and 3.2.

noncomputable def TauCeti.stdSymplecticBasis (ι : Type u_2) [Fintype ι] : Module.Basis (ι ⊕ ι) ℝ (EuclideanSpace ℝ ι × EuclideanSpace ℝ ι)

The standard ι ⊕ ι-indexed basis of EuclideanSpace ℝ ι × EuclideanSpace ℝ ι adapted to Matrix.J: Sum.inr a maps to (single a 1, 0) in the first factor and Sum.inl a maps to (0, single a 1) in the second factor.

theorem TauCeti.stdSymplecticBasis_def (ι : Type u_1) [Fintype ι] : stdSymplecticBasis ι = ((EuclideanSpace.basisFun ι ℝ).toBasis.prod (EuclideanSpace.basisFun ι ℝ).toBasis).reindex (Equiv.sumComm ι ι)

stdSymplecticBasis ι is the product of two copies of the standard basis of EuclideanSpace ℝ ι, with the two summands of the index swapped.

@[simp]

theorem TauCeti.stdSymplecticBasis_inr {ι : Type u_1} [Fintype ι] [DecidableEq ι] (a : ι) : (stdSymplecticBasis ι) (Sum.inr a) = (EuclideanSpace.single a 1, 0)

@[simp]

theorem TauCeti.stdSymplecticBasis_inl {ι : Type u_1} [Fintype ι] [DecidableEq ι] (a : ι) : (stdSymplecticBasis ι) (Sum.inl a) = (0, EuclideanSpace.single a 1)

@[simp]

theorem TauCeti.stdSymplecticBasis_repr_inr {ι : Type u_1} [Fintype ι] (u : EuclideanSpace ℝ ι × EuclideanSpace ℝ ι) (a : ι) : ((stdSymplecticBasis ι).repr u) (Sum.inr a) = u.1.ofLp a

@[simp]

theorem TauCeti.stdSymplecticBasis_repr_inl {ι : Type u_1} [Fintype ι] (u : EuclideanSpace ℝ ι × EuclideanSpace ℝ ι) (a : ι) : ((stdSymplecticBasis ι).repr u) (Sum.inl a) = u.2.ofLp a

@[simp]

theorem TauCeti.toMatrix_stdSymplecticBasis {ι : Type u_1} [Fintype ι] [DecidableEq ι] : (LinearMap.BilinForm.toMatrix (stdSymplecticBasis ι)) stdSymplecticForm.toBilinForm = Matrix.J ι ℝ

In stdSymplecticBasis ι, the matrix of stdSymplecticForm is Matrix.J ι ℝ.

noncomputable def TauCeti.stdDarbouxBasis (n : ℕ) : Module.Basis (Fin n × Fin 2) ℝ (EuclideanSpace ℝ (Fin n) × EuclideanSpace ℝ (Fin n))

The standard Fin n × Fin 2-indexed Darboux basis of EuclideanSpace ℝ (Fin n) × EuclideanSpace ℝ (Fin n), sending (i, 0) to (single i 1, 0) and (i, 1) to (0, single i 1).

@[simp]

theorem TauCeti.stdDarbouxBasis_zero {n : ℕ} (i : Fin n) : (stdDarbouxBasis n) (i, 0) = (EuclideanSpace.single i 1, 0)

@[simp]

theorem TauCeti.stdDarbouxBasis_one {n : ℕ} (i : Fin n) : (stdDarbouxBasis n) (i, 1) = (0, EuclideanSpace.single i 1)

@[simp]

theorem TauCeti.stdDarbouxBasis_repr_zero {n : ℕ} (u : EuclideanSpace ℝ (Fin n) × EuclideanSpace ℝ (Fin n)) (i : Fin n) : ((stdDarbouxBasis n).repr u) (i, 0) = u.1.ofLp i

@[simp]

theorem TauCeti.stdDarbouxBasis_repr_one {n : ℕ} (u : EuclideanSpace ℝ (Fin n) × EuclideanSpace ℝ (Fin n)) (i : Fin n) : ((stdDarbouxBasis n).repr u) (i, 1) = u.2.ofLp i

theorem TauCeti.isDarbouxBasis_stdDarbouxBasis (n : ℕ) : stdSymplecticForm.IsDarbouxBasis (stdDarbouxBasis n)

stdDarbouxBasis n is a Darboux basis of stdSymplecticForm on EuclideanSpace ℝ (Fin n) × EuclideanSpace ℝ (Fin n).

instance TauCeti.fact_finrank_euclideanSpace_prod {ι : Type u_1} [Fintype ι] : Fact (Module.finrank ℝ (EuclideanSpace ℝ ι × EuclideanSpace ℝ ι) = 2 * Fintype.card ι)

EuclideanSpace ℝ ι × EuclideanSpace ℝ ι has dimension 2 * |ι|, so it is a model space for symplectic manifolds of dimension 2 * |ι|.

noncomputable def Module.Basis.euclideanBasisEquiv {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ι : Type u_2} [Fintype ι] (b : Basis (ι ⊕ ι) ℝ V) : V ≃ₗ[ℝ] EuclideanSpace ℝ ι × EuclideanSpace ℝ ι

The linear coordinate equivalence from an ι ⊕ ι-indexed basis b of V to EuclideanSpace ℝ ι × EuclideanSpace ℝ ι sending b (Sum.inr a) to (single a 1, 0) and b (Sum.inl a) to (0, single a 1).

@[simp]

theorem Module.Basis.euclideanBasisEquiv_apply_inr {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (b : Basis (ι ⊕ ι) ℝ V) (a : ι) : b.euclideanBasisEquiv (b (Sum.inr a)) = (EuclideanSpace.single a 1, 0)

@[simp]

theorem Module.Basis.euclideanBasisEquiv_apply_inl {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (b : Basis (ι ⊕ ι) ℝ V) (a : ι) : b.euclideanBasisEquiv (b (Sum.inl a)) = (0, EuclideanSpace.single a 1)

@[simp]

theorem Module.Basis.stdSymplecticBasis_repr_euclideanBasisEquiv {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ι : Type u_2} [Fintype ι] (b : Basis (ι ⊕ ι) ℝ V) (v : V) : (TauCeti.stdSymplecticBasis ι).repr (b.euclideanBasisEquiv v) = b.repr v

@[simp]

theorem Module.Basis.euclideanBasisEquiv_fst_apply {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ι : Type u_2} [Fintype ι] (b : Basis (ι ⊕ ι) ℝ V) (v : V) (a : ι) : (b.euclideanBasisEquiv v).1.ofLp a = (b.repr v) (Sum.inr a)

@[simp]

theorem Module.Basis.euclideanBasisEquiv_snd_apply {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ι : Type u_2} [Fintype ι] (b : Basis (ι ⊕ ι) ℝ V) (v : V) (a : ι) : (b.euclideanBasisEquiv v).2.ofLp a = (b.repr v) (Sum.inl a)

theorem Module.Basis.euclideanBasisEquiv_symm_apply {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ι : Type u_2} [Fintype ι] (b : Basis (ι ⊕ ι) ℝ V) (u : EuclideanSpace ℝ ι × EuclideanSpace ℝ ι) : b.euclideanBasisEquiv.symm u = ∑ a : ι, u.1.ofLp a • b (Sum.inr a) + ∑ a : ι, u.2.ofLp a • b (Sum.inl a)

The inverse of b.euclideanBasisEquiv expands (q, p) as ∑ a, q a • b (inr a) + ∑ a, p a • b (inl a).

noncomputable def Module.Basis.darbouxBasisEquiv {V : Type u_1} [AddCommGroup V] [Module ℝ V] {n : ℕ} (b : Basis (Fin n × Fin 2) ℝ V) : V ≃ₗ[ℝ] EuclideanSpace ℝ (Fin n) × EuclideanSpace ℝ (Fin n)

The linear coordinate equivalence from a Fin n × Fin 2-indexed basis b of V to EuclideanSpace ℝ (Fin n) × EuclideanSpace ℝ (Fin n) sending b (i, 0) to (single i 1, 0) and b (i, 1) to (0, single i 1).

theorem Module.Basis.darbouxBasisEquiv_eq_euclideanBasisEquiv_reindex {V : Type u_1} [AddCommGroup V] [Module ℝ V] {n : ℕ} (b : Basis (Fin n × Fin 2) ℝ V) : b.darbouxBasisEquiv = (b.reindex (TauCeti.SymplecticForm.darbouxIndexEquiv n)).euclideanBasisEquiv

b.darbouxBasisEquiv agrees with euclideanBasisEquiv applied to b relabelled by SymplecticForm.darbouxIndexEquiv n.

@[simp]

theorem Module.Basis.darbouxBasisEquiv_apply_zero {V : Type u_1} [AddCommGroup V] [Module ℝ V] {n : ℕ} (b : Basis (Fin n × Fin 2) ℝ V) (i : Fin n) : b.darbouxBasisEquiv (b (i, 0)) = (EuclideanSpace.single i 1, 0)

@[simp]

theorem Module.Basis.darbouxBasisEquiv_apply_one {V : Type u_1} [AddCommGroup V] [Module ℝ V] {n : ℕ} (b : Basis (Fin n × Fin 2) ℝ V) (i : Fin n) : b.darbouxBasisEquiv (b (i, 1)) = (0, EuclideanSpace.single i 1)

@[simp]

theorem Module.Basis.darbouxBasisEquiv_fst_apply {V : Type u_1} [AddCommGroup V] [Module ℝ V] {n : ℕ} (b : Basis (Fin n × Fin 2) ℝ V) (v : V) (i : Fin n) : (b.darbouxBasisEquiv v).1.ofLp i = (b.repr v) (i, 0)

@[simp]

theorem Module.Basis.darbouxBasisEquiv_snd_apply {V : Type u_1} [AddCommGroup V] [Module ℝ V] {n : ℕ} (b : Basis (Fin n × Fin 2) ℝ V) (v : V) (i : Fin n) : (b.darbouxBasisEquiv v).2.ofLp i = (b.repr v) (i, 1)

theorem Module.Basis.darbouxBasisEquiv_symm_apply {V : Type u_1} [AddCommGroup V] [Module ℝ V] {n : ℕ} (b : Basis (Fin n × Fin 2) ℝ V) (u : EuclideanSpace ℝ (Fin n) × EuclideanSpace ℝ (Fin n)) : b.darbouxBasisEquiv.symm u = ∑ i : Fin n, u.1.ofLp i • b (i, 0) + ∑ i : Fin n, u.2.ofLp i • b (i, 1)

The inverse of b.darbouxBasisEquiv expands (q, p) as ∑ i, q i • b (i, 0) + ∑ i, p i • b (i, 1).

noncomputable def Module.Basis.euclideanBasisContinuousLinearEquiv {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {ι : Type u_2} [Fintype ι] (b : Basis (ι ⊕ ι) ℝ V) : V ≃L[ℝ] EuclideanSpace ℝ ι × EuclideanSpace ℝ ι

The continuous-linear coordinate equivalence from an ι ⊕ ι-indexed basis b of a real normed space V to EuclideanSpace ℝ ι × EuclideanSpace ℝ ι. Finite-dimensionality of V is inferred from the finite basis b.

@[simp]

theorem Module.Basis.euclideanBasisContinuousLinearEquiv_toLinearEquiv {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {ι : Type u_2} [Fintype ι] (b : Basis (ι ⊕ ι) ℝ V) : ↑b.euclideanBasisContinuousLinearEquiv = b.euclideanBasisEquiv

@[simp]

theorem Module.Basis.coe_euclideanBasisContinuousLinearEquiv {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {ι : Type u_2} [Fintype ι] (b : Basis (ι ⊕ ι) ℝ V) : ⇑b.euclideanBasisContinuousLinearEquiv = ⇑b.euclideanBasisEquiv

@[simp]

theorem Module.Basis.coe_euclideanBasisContinuousLinearEquiv_symm {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {ι : Type u_2} [Fintype ι] (b : Basis (ι ⊕ ι) ℝ V) : ⇑b.euclideanBasisContinuousLinearEquiv.symm = ⇑b.euclideanBasisEquiv.symm

noncomputable def Module.Basis.darbouxBasisContinuousLinearEquiv {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {n : ℕ} (b : Basis (Fin n × Fin 2) ℝ V) : V ≃L[ℝ] EuclideanSpace ℝ (Fin n) × EuclideanSpace ℝ (Fin n)

The continuous-linear coordinate equivalence from a Fin n × Fin 2-indexed basis b of a real normed space V to EuclideanSpace ℝ (Fin n) × EuclideanSpace ℝ (Fin n).

@[simp]

theorem Module.Basis.darbouxBasisContinuousLinearEquiv_toLinearEquiv {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {n : ℕ} (b : Basis (Fin n × Fin 2) ℝ V) : ↑b.darbouxBasisContinuousLinearEquiv = b.darbouxBasisEquiv

@[simp]

theorem Module.Basis.coe_darbouxBasisContinuousLinearEquiv {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {n : ℕ} (b : Basis (Fin n × Fin 2) ℝ V) : ⇑b.darbouxBasisContinuousLinearEquiv = ⇑b.darbouxBasisEquiv

@[simp]

theorem Module.Basis.coe_darbouxBasisContinuousLinearEquiv_symm {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {n : ℕ} (b : Basis (Fin n × Fin 2) ℝ V) : ⇑b.darbouxBasisContinuousLinearEquiv.symm = ⇑b.darbouxBasisEquiv.symm

theorem TauCeti.SymplecticForm.isSymplectomorphism_euclideanBasisEquiv_iff {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {ω : SymplecticForm V} {b : Module.Basis (ι ⊕ ι) ℝ V} : ω.IsSymplectomorphism stdSymplecticForm b.euclideanBasisEquiv ↔ (LinearMap.BilinForm.toMatrix b) ω.toBilinForm = Matrix.J ι ℝ

b.euclideanBasisEquiv is a symplectomorphism from ω to stdSymplecticForm if and only if the matrix of ω in b is Matrix.J ι ℝ.

theorem TauCeti.SymplecticForm.isSymplectomorphism_darbouxBasisEquiv_iff {V : Type u_1} [AddCommGroup V] [Module ℝ V] {n : ℕ} {ω : SymplecticForm V} {b : Module.Basis (Fin n × Fin 2) ℝ V} : ω.IsSymplectomorphism stdSymplecticForm b.darbouxBasisEquiv ↔ ω.IsDarbouxBasis b

b.darbouxBasisEquiv is a symplectomorphism from ω to stdSymplecticForm if and only if b is a Darboux basis of ω.

theorem TauCeti.SymplecticForm.IsDarbouxBasis.isSymplectomorphism_darbouxBasisEquiv {V : Type u_1} [AddCommGroup V] [Module ℝ V] {n : ℕ} {ω : SymplecticForm V} {b : Module.Basis (Fin n × Fin 2) ℝ V} (hb : ω.IsDarbouxBasis b) : ω.IsSymplectomorphism stdSymplecticForm b.darbouxBasisEquiv

The coordinate equivalence of a Darboux basis is a linear symplectomorphism onto stdSymplecticForm.

theorem TauCeti.SymplecticForm.IsDarbouxBasis.transport_darbouxBasisEquiv {V : Type u_1} [AddCommGroup V] [Module ℝ V] {n : ℕ} {ω : SymplecticForm V} {b : Module.Basis (Fin n × Fin 2) ℝ V} (hb : ω.IsDarbouxBasis b) : ω.transport b.darbouxBasisEquiv = stdSymplecticForm

Transporting ω along the coordinate equivalence of a Darboux basis yields stdSymplecticForm.

theorem TauCeti.SymplecticForm.exists_isSymplectomorphism_stdSymplecticForm {V : Type u_1} [AddCommGroup V] [Module ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) : ∃ (n : ℕ) (e : V ≃ₗ[ℝ] EuclideanSpace ℝ (Fin n) × EuclideanSpace ℝ (Fin n)), ω.IsSymplectomorphism stdSymplecticForm e

Every finite-dimensional symplectic space is linearly symplectomorphic to EuclideanSpace ℝ (Fin n) × EuclideanSpace ℝ (Fin n) with stdSymplecticForm.

theorem TauCeti.SymplecticForm.exists_isSymplectomorphism_stdSymplecticForm_of_finrank_eq {V : Type u_1} [AddCommGroup V] [Module ℝ V] [FiniteDimensional ℝ V] {n : ℕ} (ω : SymplecticForm V) (hn : Module.finrank ℝ V = 2 * n) : ∃ (e : V ≃ₗ[ℝ] EuclideanSpace ℝ (Fin n) × EuclideanSpace ℝ (Fin n)), ω.IsSymplectomorphism stdSymplecticForm e

A finite-dimensional symplectic space of dimension 2 * n is linearly symplectomorphic to EuclideanSpace ℝ (Fin n) × EuclideanSpace ℝ (Fin n) with stdSymplecticForm.

theorem TauCeti.SymplecticForm.exists_isSymplectomorphism_stdSymplecticForm_apply_eq_snd_single {V : Type u_1} [AddCommGroup V] [Module ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) {v : V} (hv : v ≠ 0) : ∃ (m : ℕ) (e : V ≃ₗ[ℝ] EuclideanSpace ℝ (Fin (m + 1)) × EuclideanSpace ℝ (Fin (m + 1))), ω.IsSymplectomorphism stdSymplecticForm e ∧ e v = (0, EuclideanSpace.single 0 1)

Every nonzero vector in a finite-dimensional symplectic space is mapped to (0, EuclideanSpace.single 0 1) by a linear symplectomorphism onto the standard Euclidean model.

theorem TauCeti.SymplecticForm.exists_isSymplectomorphism_stdSymplecticForm_apply_eq_fst_single {V : Type u_1} [AddCommGroup V] [Module ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) {v : V} (hv : v ≠ 0) : ∃ (m : ℕ) (e : V ≃ₗ[ℝ] EuclideanSpace ℝ (Fin (m + 1)) × EuclideanSpace ℝ (Fin (m + 1))), ω.IsSymplectomorphism stdSymplecticForm e ∧ e v = (EuclideanSpace.single 0 1, 0)

Every nonzero vector in a finite-dimensional symplectic space is mapped to (EuclideanSpace.single 0 1, 0) by a linear symplectomorphism onto the standard Euclidean model.

theorem TauCeti.SymplecticForm.exists_continuousLinearEquiv_stdSymplecticForm {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) : ∃ (n : ℕ) (e : V ≃L[ℝ] EuclideanSpace ℝ (Fin n) × EuclideanSpace ℝ (Fin n)), ω.IsSymplectomorphism stdSymplecticForm ↑e

Every finite-dimensional normed symplectic space is continuous-linearly symplectomorphic to EuclideanSpace ℝ (Fin n) × EuclideanSpace ℝ (Fin n) with stdSymplecticForm.

theorem TauCeti.SymplecticForm.exists_continuousLinearEquiv_stdSymplecticForm_of_finrank_eq {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {n : ℕ} (ω : SymplecticForm V) (hn : Module.finrank ℝ V = 2 * n) : ∃ (e : V ≃L[ℝ] EuclideanSpace ℝ (Fin n) × EuclideanSpace ℝ (Fin n)), ω.IsSymplectomorphism stdSymplecticForm ↑e

A finite-dimensional normed symplectic space of dimension 2 * n is continuous-linearly symplectomorphic to EuclideanSpace ℝ (Fin n) × EuclideanSpace ℝ (Fin n) with stdSymplecticForm.

theorem TauCeti.SymplecticForm.exists_continuousLinearEquiv_stdSymplecticForm_apply_eq_snd_single {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) {v : V} (hv : v ≠ 0) : ∃ (m : ℕ) (e : V ≃L[ℝ] EuclideanSpace ℝ (Fin (m + 1)) × EuclideanSpace ℝ (Fin (m + 1))), ω.IsSymplectomorphism stdSymplecticForm ↑e ∧ e v = (0, EuclideanSpace.single 0 1)

Every nonzero vector in a finite-dimensional normed symplectic space is carried to (0, EuclideanSpace.single 0 1) by a continuous-linear symplectomorphism onto the standard Euclidean model.

theorem TauCeti.SymplecticForm.exists_continuousLinearEquiv_stdSymplecticForm_apply_eq_fst_single {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) {v : V} (hv : v ≠ 0) : ∃ (m : ℕ) (e : V ≃L[ℝ] EuclideanSpace ℝ (Fin (m + 1)) × EuclideanSpace ℝ (Fin (m + 1))), ω.IsSymplectomorphism stdSymplecticForm ↑e ∧ e v = (EuclideanSpace.single 0 1, 0)

Every nonzero vector in a finite-dimensional normed symplectic space is carried to (EuclideanSpace.single 0 1, 0) by a continuous-linear symplectomorphism onto the standard Euclidean model.