Prove2Me

Coordinates in a symplectic frame x,X,Z1,Z2x, X, Z_1, Z_2 of R4\mathbb{R}^4

Proved
HryniewiczCriterion.omega0_frame_decomp

by Mazecto · Oct 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

linear-algebrasymplectic-geometry

Let x,X,Z1,Z2∈R4x,X,Z_1,Z_2\in\mathbb{R}^4 satisfy ω0(x,X)=μ≠0\omega_0(x,X)=\mu\neq0 and ω0(Z1,Z2)=1\omega_0(Z_1,Z_2)=1, and let Z1,Z2Z_1,Z_2 be ω0\omega_0-orthogonal to xx and XX. Then every v∈R4v\in\mathbb{R}^4 decomposes as

v=ω0(v,X)μ x+ω0(x,v)μ X+ω0(v,Z2) Z1+ω0(Z1,v) Z2.v=\frac{\omega_0(v,X)}{\mu}\,x+\frac{\omega_0(x,v)}{\mu}\,X+\omega_0(v,Z_2)\,Z_1+\omega_0(Z_1,v)\,Z_2.

This is the coordinate form of the splitting R4=span{x,XK(x)}⊕ξx\mathbb{R}^4=\mathrm{span}\{x,X_K(x)\}\oplus\xi_x.

Preamble
import Definitions.Def_HryniewiczCriterion_GraphAngle

open HryniewiczCriterion
open scoped ContDiff
Formal statement
theorem HryniewiczCriterion.omega0_frame_decomp (x X Z₁ Z₂ : R4) (μ : ℝ) (hμ : omega0 x X = μ) (hμ0 : μ ≠ 0)
    (h12 : omega0 Z₁ Z₂ = 1) (h1a : omega0 Z₁ x = 0) (h1b : omega0 Z₁ X = 0)
    (h2a : omega0 Z₂ x = 0) (h2b : omega0 Z₂ X = 0) (v : R4) :
    v = (omega0 v X / μ) • x + (omega0 x v / μ) • X + omega0 v Z₂ • Z₁ + omega0 Z₁ v • Z₂ := by sorry
Source
Hofer–Wysocki–Zehnder, The dynamics on three-dimensional strictly convex energy surfaces, Ann. of Math. 148 (1998), https://doi.org/10.2307/120994, (3.35)–(3.36), p. 220 (the ω₀-orthogonal splitting ℝ⁴ = span{x, X_K(x)} ⊕ ξ_x); elementary symplectic linear algebra.

View graph