structure BlockSymplecticData (V : Type u_1) (W : Type u_2) [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] : Type (max u_1 u_2)

Algebraic data packaging a 2×2 block-matrix symplectic form on $V \oplus W$: an evaluation pairing $\mathrm{eval} : W \otimes V \to \mathbb{R}$, an invertible block endomorphism $B$ on $V$ together with its transpose-inverse $B^{-T}$ on $W$, and a skew form $C$ on $W$ realized via $\tilde C : W \to V$.

• eval : W →ₗ[ℝ] V →ₗ[ℝ] ℝ
• B_endo : V →ₗ[ℝ] V
• B_inv : V →ₗ[ℝ] V
• hBinv_left (v : V) : self.B_inv (self.B_endo v) = v
• hBinv_right (v : V) : self.B_endo (self.B_inv v) = v
• B_inv_t : W →ₗ[ℝ] W
• hBinvt (w : W) (v : V) : (self.eval (self.B_inv_t w)) v = (self.eval w) (self.B_inv v)
• C_form : W →ₗ[ℝ] W →ₗ[ℝ] ℝ
• hC_skew (w₁ w₂ : W) : (self.C_form w₁) w₂ = -(self.C_form w₂) w₁
• C_tilde : W →ₗ[ℝ] V
• hCtilde (w₁ w₂ : W) : (self.eval w₁) (self.C_tilde w₂) = (self.C_form w₁) w₂

noncomputable def BlockSymplecticData.omega0 {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (d : BlockSymplecticData V W) (p₁ p₂ : V × W) : ℝ

The "untwisted" model symplectic form $\omega_0((v_1,w_1),(v_2,w_2)) = \mathrm{eval}(w_1, v_2) - \mathrm{eval}(w_2, v_1)$ on $V \times W$.

noncomputable def BlockSymplecticData.omega1 {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (d : BlockSymplecticData V W) (p₁ p₂ : V × W) : ℝ

The "twisted" symplectic form $\omega_1((v_1,w_1),(v_2,w_2)) = \mathrm{eval}(w_1, Bv_2) - \mathrm{eval}(w_2, Bv_1) + C(w_1,w_2)$ obtained by composing the $V$-pairing with $B$ and adding the skew form $C$ on $W$.

noncomputable def BlockSymplecticData.correctionMap {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (d : BlockSymplecticData V W) (p : V × W) : V × W

Block linear change of variables $(v,w) \mapsto (v - \tfrac{1}{2} B^{-1} \tilde C (B^{-T} w), B^{-T} w)$ used to relate the twisted symplectic form $\omega_1$ back to the model form $\omega_0$.