We prove the Weinstein neighborhood theorem with the canonical sign convention . The essential first step is to match the two symplectic forms as bilinear forms on the entire tangent space along , not only after pulling them back to .
Here is the needed symplectic splitting along a Lagrangian submanifold. Write and . Choose a smooth vector bundle complement of , for example using a Riemannian metric. Since is a Lagrangian subspace in every fiber, the pairing map
is an isomorphism: its kernel is , and both bundles have rank . Let be its inverse and put . Define by
and set . Nondegeneracy of the dual pairing gives a unique smooth . Since is alternating,
Thus is a smooth Lagrangian complement to . The map
is a vector bundle isomorphism, is the identity on , and satisfies
The last equality uses the canonical splitting of the tangent bundle of along its zero section.
Choose a Riemannian metric near for which is orthogonal to . The tubular neighborhood construction using its Riemannian exponential map gives a diffeomorphism
after shrinking around the zero section. It restricts to the given inclusion of and has differential along it. Consequently and agree pointwise as ambient bilinear forms at every point of the zero section.
We use the following precise relative Moser theorem. If two closed symplectic forms near a compact embedded submanifold agree as ambient bilinear forms along , then, on smaller neighborhoods, there is a diffeomorphism fixing pointwise with . One sufficient version allows a symplectic path with and as ambient covectors along : solve and use its flow. The vector field vanishes on , so the flow fixes , and compactness permits a common smaller neighborhood for the full time interval.
For completeness, all hypotheses can be checked directly here. Put and . At the zero section, every equals . The nondegenerate property is open, and compactness of allows a single smaller neighborhood on which all are symplectic forms. Choose it fiberwise star-shaped. Write and let be the vertical radial vector field. The radial homotopy primitive near a zero section
is smooth, is zero as an ambient covector along the zero section, and satisfies
The radial homotopy operator gives this identity, using and . Smoothness at follows because contraction with supplies a factor of after evaluation at ; the vanishing of along supplies additional vanishing. Therefore solve . By Cartan's magic formula, its flow maps satisfy
After shrinking the starting neighborhood, these flows exist for and fix . This is a relative local construction, not an assertion of completeness throughout the noncompact cotangent bundle.
Finally set , let be its sufficiently small domain, and let . Then
Thus the map is a symplectomorphism of neighborhoods and agrees with the specified inclusion at every point of .