structure SymplecticLinearAlgebra.IsComplexStructure {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J : V →ₗ[ℝ] V) : Prop

A linear map $J: V \to V$ is a complex structure iff $J^2 = -I$.

• sq_eq_neg : J ∘ₗ J = -LinearMap.id

theorem SymplecticLinearAlgebra.IsComplexStructure.apply_apply {V : Type u_1} [AddCommGroup V] [Module ℝ V] {J : V →ₗ[ℝ] V} (hJ : IsComplexStructure J) (v : V) : J (J v) = -v

Pointwise form of $J^2 = -I$: $J(J v) = -v$ for every $v \in V$.

structure SymplecticLinearAlgebra.IsCompatibleComplexStr {V : Type u_1} [AddCommGroup V] [Module ℝ V] (Ω : LinearMap.BilinForm ℝ V) (J : V →ₗ[ℝ] V) : Prop

A complex structure $J$ is compatible with a symplectic form $\Omega$ iff $J^2 = -I$, $\Omega(Ju, Jv) = \Omega(u, v)$ (preservation), and $\Omega(u, Ju) > 0$ for $u \neq 0$ (taming).

• complex_str : IsComplexStructure J
• preserves (u v : V) : (Ω (J u)) (J v) = (Ω u) v
• positive (u : V) : u ≠ 0 → (Ω u) (J u) > 0

theorem SymplecticLinearAlgebra.exists_compatible_complex_structure {V : Type u_1} [AddCommGroup V] [Module ℝ V] [FiniteDimensional ℝ V] {Ω : LinearMap.BilinForm ℝ V} (hΩ : IsSymplecticForm Ω) : ∃ (J : V →ₗ[ℝ] V), IsCompatibleComplexStr Ω J

Every finite-dimensional symplectic vector space admits a compatible complex structure, constructed in a symplectic standard basis by sending $e_i \mapsto f_i$, $f_i \mapsto -e_i$.

theorem SymplecticLinearAlgebra.compatible_forms_convex_linear {V : Type u_1} [AddCommGroup V] [Module ℝ V] {Ω₀ Ω₁ : LinearMap.BilinForm ℝ V} {J : V →ₗ[ℝ] V} (h₀ : IsCompatibleComplexStr Ω₀ J) (h₁ : IsCompatibleComplexStr Ω₁ J) (t : ℝ) (ht : t ∈ Set.Icc 0 1) : IsCompatibleComplexStr ((1 - t) • Ω₀ + t • Ω₁) J

Convexity (Proposition 3): the set of symplectic forms compatible with a fixed $J$ is convex—if $J$ is compatible with $\Omega_0$ and $\Omega_1$ then it is compatible with $(1 - t)\Omega_0 + t\Omega_1$ for every $t \in [0,1]$.