Local normal form near a coisotropic submanifold

By [F1]--[F2], $K_j$ integrates locally to the characteristic foliation. The equality of restricted forms gives $df(K_0)=K_1$. By [F3], choose a smooth complement $E_0$ to $K_0$ in $T{C}_0$ and put $E_1=df(E_0)$. Each $E_j$ is symplectic: if $e\in E_j$ is orthogonal to $E_j$, it is also orthogonal to $K_j$ because $K_j=T{C}_j^{{\omega }_j}$, hence to all of $T{C}_j$; thus $e\in K_j\cap E_j=0$. Consequently $T{M}_j{\mathrm{\mid }}_{C_j}=E_j\oplus S_j,S_j=E_j^{{\omega }_j},$ where $S_j$ is a smooth symplectic subbundle of rank $2\mathrm{rank}{K}_j$ and $K_j\subset S_j$ is Lagrangian. Smoothness follows locally by solving the constant-rank linear equations defining the symplectic orthogonal.

Choose by [F3] a smooth complement $G_j$ to $K_j$ in $S_j$. The pairing $K_j\times G_j\to \mathbb{R}$, $(k,g)\mapsto {\omega }_j(k,g)$, is nondegenerate. There is therefore a unique smooth bundle map $T_j:G_j\to K_j$ satisfying ${\omega }_j(T_{j}g,h)=-\frac{1}{2}{\omega }_j(g,h)(g,h\in G_j)\mathrm{.}$ For $G_j^{\mathrm{\prime }}=\{g+T_{j}g:g\in G_j\}$, skew-symmetry gives ${\omega }_j(g+T_{j}g,h+T_{j}h)={\omega }_j(g,h)-\frac{1}{2}{\omega }_j(g,h)+\frac{1}{2}{\omega }_j(h,g)=0.$ Thus $S_j=K_j\oplus G_j^{\mathrm{\prime }}$ is a Lagrangian splitting. Define $A:G_0^{\mathrm{\prime }}\to G_1^{\mathrm{\prime }}$ by the nondegenerate-pairing condition ${\omega }_1(df(k),A(g))={\omega }_0(k,g)(k\in K_0)\mathrm{.}$ It is a smooth bundle isomorphism. The map equal to $df$ on $E_0\oplus K_0$ and to $A$ on $G_0^{\mathrm{\prime }}$ preserves the symplectic form on every summand and cross-pairing, hence is a symplectic bundle isomorphism $T{M}_0{\mathrm{\mid }}_{C_0}\to T{M}_1{\mathrm{\mid }}_{C_1}$ extending $df$.

The quotient maps identify the chosen complements $G_j^{\mathrm{\prime }}$ with the quotient normal bundles. Apply the tubular construction in [F4] using these complements: explicitly, in the proof of that construction replace the orthogonal complement by $G_j^{\mathrm{\prime }}$ in the normal-addition map. Its derivative at $(x,0)$ is then $(u,g)\mapsto d{i}_j(u)+g$; the same inverse-function and variable-radius shrinking argument produces a tubular diffeomorphism ${\mathrm{\Psi }}_j$ with that derivative. The bundle map induced by $A:G_0^{\mathrm{\prime }}\to G_1^{\mathrm{\prime }}$ therefore gives $h={\mathrm{\Psi }}_1\circ A\circ {\mathrm{\Psi }}_0^{-1},$ a diffeomorphism between neighbourhoods extending $f$ with $dh{\mathrm{\mid }}_{C_0}$ equal to the full symplectic bundle isomorphism of step 2.1, not merely equal on quotient normals. Hence $h^{\ast }{\omega }_1$ and ${\omega }_0$ agree as full tensors along $C_0$. Their difference is closed and has the fibre-radial relative primitive supplied in [F4].

The interpolation between those two forms is symplectic near $C_0$. Relative Moser therefore gives a correction fixed on $C_0$; composing it with $h$ produces the desired neighbourhood symplectomorphism. The characteristic foliation was derived in step 1.1 rather than assumed as extra data.