[proofplan] We first use $\omega$ to identify the normal bundle of the Lagrangian submanifold $L$ with $T^*L$. A tubular neighbourhood embedding with this prescribed first-order behaviour gives a preliminary diffeomorphism from a neighbourhood of the zero section in $T^*L$ onto a neighbourhood of $L$ in $M$. The preliminary map is chosen with a full first derivative along the zero section that identifies the standard symplectic model $T_xL\oplus T_x^*L$ with $T_xM$, so the pullback of $\omega$ and the canonical form $\omega_{\mathrm{can}}$ agree along the zero section. The [relative Moser lemma](/theorems/10051) then deforms one form to the other while fixing the zero section. Composing the preliminary tubular map with this Moser correction gives the desired symplectomorphism. [/proofplan]

[step:Identify the normal bundle of $L$ with $T^*L$ using $\omega$]Let \begin{align*} i:L\to M \end{align*} denote the inclusion map, and let \begin{align*} \nu_L:=i^*TM/TL \end{align*} denote the normal [vector bundle](/page/Vector%20Bundle) of $L$ in $M$. For each $x\in L$, define a [linear map](/page/Linear%20Map) \begin{align*} \Theta_x:(\nu_L)_x&\to T_x^*L \end{align*} by \begin{align*} \Theta_x([v])(u)=\omega_x(v,u) \end{align*} for $[v]\in T_xM/T_xL$ and $u\in T_xL$. This is well-defined: if $v'=v+w$ with $w\in T_xL$, then \begin{align*} \omega_x(v',u)=\omega_x(v,u)+\omega_x(w,u)=\omega_x(v,u), \end{align*} because $L$ is Lagrangian and hence $\omega_x|_{T_xL}=0$. If $\Theta_x([v])=0$, then $\omega_x(v,u)=0$ for every $u\in T_xL$, so $v\in (T_xL)^\omega$. Since $L$ is Lagrangian, $(T_xL)^\omega=T_xL$, and therefore $[v]=0$ in $T_xM/T_xL$. Thus $\Theta_x$ is injective. Since \begin{align*} \dim(\nu_L)_x=\dim M-\dim L=\dim L=\dim T_x^*L, \end{align*} the map $\Theta_x$ is an isomorphism. These fibrewise maps vary smoothly with $x$, so they define a [smooth vector bundle](/page/Smooth%20Vector%20Bundle) isomorphism \begin{align*} \Theta:\nu_L\to T^*L. \end{align*} We also choose a smooth lift of this normal-bundle identification with Lagrangian image. Choose any smooth bundle map \begin{align*} B:T^*L\to i^*TM \end{align*} whose composition with the quotient map $i^*TM\to\nu_L$ is $\Theta^{-1}$. For $x\in L$, define the skew-symmetric [bilinear form](/page/Bilinear%20Form) \begin{align*} K_x:T_x^*L\times T_x^*L\to\mathbb R \end{align*} by \begin{align*} K_x(\alpha,\beta)=\omega_x(B_x\alpha,B_x\beta). \end{align*} Choose a Riemannian metric on $L$. For each $\beta\in T_x^*L$, let $S_x\beta\in T_xL$ be the unique vector satisfying \begin{align*} \alpha(S_x\beta)=-\frac{1}{2}K_x(\alpha,\beta) \end{align*} for every $\alpha\in T_x^*L$. Smooth dependence on $x$ follows from smoothness of $B$, $K$, and the metric identification between $TL$ and $T^*L$. Define \begin{align*} A:T^*L\to i^*TM \end{align*} by \begin{align*} A_x\alpha=B_x\alpha+S_x\alpha. \end{align*} Then the class of $A_x\alpha$ in $T_xM/T_xL$ is $\Theta_x^{-1}(\alpha)$, and for all $u\in T_xL$ and $\alpha,\beta\in T_x^*L$, \begin{align*} \omega_x(A_x\alpha,u)=\alpha(u) \end{align*} and \begin{align*} \omega_x(A_x\alpha,A_x\beta)=0. \end{align*} Indeed, the first identity follows because adding $S_x\alpha\in T_xL$ does not change the pairing with $u\in T_xL$. For the second identity, expand by bilinearity and use $\omega_x|_{T_xL}=0$: \begin{align*} \omega_x(A_x\alpha,A_x\beta)=K_x(\alpha,\beta)+\alpha(S_x\beta)-\beta(S_x\alpha)=0. \end{align*}[/step]

[guided]The first-order information transverse to $L$ is the essential input. Let \begin{align*} i:L\to M \end{align*} be the inclusion, and define the normal bundle \begin{align*} \nu_L:=i^*TM/TL. \end{align*} For each point $x\in L$, a normal vector is a class $[v]\in T_xM/T_xL$. We send this class to the covector on $T_xL$ obtained by inserting $v$ into the first slot of $\omega_x$: \begin{align*} \Theta_x:(\nu_L)_x&\to T_x^*L \end{align*} with \begin{align*} \Theta_x([v])(u)=\omega_x(v,u) \end{align*} for $u\in T_xL$. We must check that this formula does not depend on the representative $v$. If $v'=v+w$ for some $w\in T_xL$, then \begin{align*} \omega_x(v',u)=\omega_x(v,u)+\omega_x(w,u). \end{align*} Because $L$ is Lagrangian, $\omega_x(w,u)=0$ for all $w,u\in T_xL$. Therefore \begin{align*} \omega_x(v',u)=\omega_x(v,u), \end{align*} so $\Theta_x$ is well-defined. Next we prove that $\Theta_x$ is an isomorphism. If $\Theta_x([v])=0$, then \begin{align*} \omega_x(v,u)=0 \end{align*} for every $u\in T_xL$. This says exactly that $v\in (T_xL)^\omega$. Since $L$ is Lagrangian, its tangent space equals its symplectic orthogonal: \begin{align*} (T_xL)^\omega=T_xL. \end{align*} Hence $v\in T_xL$, so $[v]=0$ in $T_xM/T_xL$. Thus $\Theta_x$ is injective. The domain and codomain have the same dimension, because \begin{align*} \dim(\nu_L)_x=\dim M-\dim L=\dim L=\dim T_x^*L. \end{align*} An injective linear map between finite-dimensional vector spaces of the same dimension is an isomorphism. Since the construction uses the smooth bundle map induced by the smooth two-form $\omega$, the maps $\Theta_x$ assemble into a smooth vector bundle isomorphism \begin{align*} \Theta:\nu_L\to T^*L. \end{align*} This quotient-level identification is not yet enough for the later comparison of two-forms, because a two-form also sees the pairing of two chosen normal representatives. We therefore choose the representatives in a controlled way. Let \begin{align*} B:T^*L\to i^*TM \end{align*} be a smooth bundle map lifting $\Theta^{-1}$ through the quotient map $i^*TM\to\nu_L$. For each $x\in L$, define \begin{align*} K_x:T_x^*L\times T_x^*L\to\mathbb R \end{align*} by \begin{align*} K_x(\alpha,\beta)=\omega_x(B_x\alpha,B_x\beta). \end{align*} This is the unwanted vertical-vertical pairing. To remove it, choose a Riemannian metric on $L$ and define $S_x\beta\in T_xL$ by the condition \begin{align*} \alpha(S_x\beta)=-\frac{1}{2}K_x(\alpha,\beta) \end{align*} for every $\alpha\in T_x^*L$. The metric gives the required smooth identification of covectors and vectors, so $S:T^*L\to TL$ is smooth. Now set \begin{align*} A:T^*L\to i^*TM \end{align*} by \begin{align*} A_x\alpha=B_x\alpha+S_x\alpha. \end{align*} Adding $S_x\alpha\in T_xL$ does not change the normal class, so $A_x\alpha$ still represents $\Theta_x^{-1}(\alpha)$. It also preserves the mixed pairing: for $u\in T_xL$, \begin{align*} \omega_x(A_x\alpha,u)=\omega_x(B_x\alpha,u)+\omega_x(S_x\alpha,u)=\alpha(u), \end{align*} because $\omega_x(S_x\alpha,u)=0$ on the Lagrangian subspace $T_xL$. Finally, expanding the vertical-vertical pairing gives \begin{align*} \omega_x(A_x\alpha,A_x\beta)=K_x(\alpha,\beta)+\alpha(S_x\beta)-\beta(S_x\alpha). \end{align*} By the definition of $S$ and the skew-symmetry of $K_x$, \begin{align*} \alpha(S_x\beta)-\beta(S_x\alpha)=-K_x(\alpha,\beta). \end{align*} Hence \begin{align*} \omega_x(A_x\alpha,A_x\beta)=0. \end{align*} This constructs the full first-order symplectic model needed in the next step.[/guided]

[step:Choose a tubular neighbourhood map with the prescribed full derivative] Let \begin{align*} j:L\to T^*L \end{align*} be the zero section. Along $j(L)$), use the vector bundle splitting \begin{align*} T_{0_x}(T^*L)\cong T_xL\oplus T_x^*L, \end{align*} where $0_x=j(x)$. Define a smooth bundle isomorphism \begin{align*} D:T(T^*L)|_{j(L)}\to i^*TM \end{align*} by \begin{align*} D_{0_x}(u,\alpha)=di_x(u)+A_x\alpha. \end{align*} Its restriction to $Tj(TL)$ is $di$, and its induced map on normal bundles is $\Theta^{-1}:T^*L\to\nu_L$. By the [tubular neighbourhood theorem](/theorems/2276) with prescribed first derivative along the embedded submanifold, applied to the embeddings $j:L\to T^*L$ and $i:L\to M$ and to the bundle isomorphism $D$, there exist an open neighbourhood $U_0\subset T^*L$ of $j(L)$, an open neighbourhood $V_0\subset M$ of $L$, and a diffeomorphism \begin{align*} F:U_0\to V_0 \end{align*} such that \begin{align*} F\circ j=i \end{align*} and \begin{align*} dF_{0_x}=D_{0_x} \end{align*} for every $x\in L$. Thus, for $u\in T_xL$ and $\alpha\in T_x^*L$, \begin{align*} dF_{0_x}(u,\alpha)=di_x(u)+A_x\alpha. \end{align*} [/step]

[step:Compare the two symplectic forms along the zero section]Define \begin{align*} \omega_0&:=\omega_{\mathrm{can}}|_{U_0}\in\Omega^2(U_0), \end{align*} and define \begin{align*} \omega_1&:=F^*\omega\in\Omega^2(U_0). \end{align*} Both forms are closed and nondegenerate after shrinking $U_0$ if necessary: $\omega_0$ is symplectic on all of $T^*L$, while $\omega_1$ is symplectic because $F$ is a diffeomorphism and $\omega$ is symplectic. We now show that $\omega_0$ and $\omega_1$ agree at every point of the zero section. Fix $x\in L$, and write $0_x=j(x)$. Under the splitting \begin{align*} T_{0_x}(T^*L)\cong T_xL\oplus T_x^*L, \end{align*} the canonical symplectic form with convention $\omega_{\mathrm{can}}=-d\lambda$ satisfies \begin{align*} (\omega_0)_{0_x}\bigl((u,\alpha),(v,\beta)\bigr)=\alpha(v)-\beta(u) \end{align*} for all $u,v\in T_xL$ and $\alpha,\beta\in T_x^*L$. By the prescribed first derivative of $F$, \begin{align*} dF_{0_x}(u,\alpha)=di_x(u)+A_x\alpha \end{align*} and \begin{align*} dF_{0_x}(v,\beta)=di_x(v)+A_x\beta. \end{align*} Therefore \begin{align*} (\omega_1)_{0_x}\bigl((u,\alpha),(v,\beta)\bigr)=\omega_x(di_x(u)+A_x\alpha,di_x(v)+A_x\beta). \end{align*} Expanding by bilinearity gives \begin{align*} (\omega_1)_{0_x}\bigl((u,\alpha),(v,\beta)\bigr)=\omega_x(di_x(u),di_x(v))+\omega_x(di_x(u),A_x\beta)+\omega_x(A_x\alpha,di_x(v))+\omega_x(A_x\alpha,A_x\beta). \end{align*} The Lagrangian condition gives $\omega_x(di_x(u),di_x(v))=0$. The construction of $A$ gives $\omega_x(A_x\alpha,A_x\beta)=0$, $\omega_x(A_x\alpha,di_x(v))=\alpha(v)$, and $\omega_x(A_x\beta,di_x(u))=\beta(u)$. Using skew-symmetry for the second mixed term, \begin{align*} \omega_x(di_x(u),A_x\beta)=-\omega_x(A_x\beta,di_x(u))=-\beta(u). \end{align*} Thus \begin{align*} (\omega_1)_{0_x}\bigl((u,\alpha),(v,\beta)\bigr)=\alpha(v)-\beta(u). \end{align*} Therefore \begin{align*} (\omega_1)_{0_x}=(\omega_0)_{0_x} \end{align*} for every $x\in L$.[/step]

[guided]The goal of this step is to arrange the hypothesis needed for the relative Moser lemma: the two symplectic forms must agree along the submanifold that will be fixed, namely the zero section. Define \begin{align*} \omega_0&:=\omega_{\mathrm{can}}|_{U_0}\in\Omega^2(U_0), \end{align*} and \begin{align*} \omega_1&:=F^*\omega\in\Omega^2(U_0). \end{align*} The form $\omega_0$ is symplectic because $\omega_{\mathrm{can}}=-d\lambda$ is the canonical symplectic form on $T^*L$. The form $\omega_1$ is symplectic because it is the pullback of the symplectic form $\omega$ by the diffeomorphism $F$. Both are closed, since $d\omega_{\mathrm{can}}=0$ and \begin{align*} d(F^*\omega)=F^*(d\omega)=0. \end{align*} Now fix $x\in L$, and write $0_x=j(x)$ for the corresponding point of the zero section. The tangent space to the cotangent bundle along the zero section has the vector bundle splitting \begin{align*} T_{0_x}(T^*L)\cong T_xL\oplus T_x^*L. \end{align*} Under this splitting, the canonical symplectic form is \begin{align*} (\omega_0)_{0_x}\bigl((u,\alpha),(v,\beta)\bigr)=\alpha(v)-\beta(u) \end{align*} for $u,v\in T_xL$ and $\alpha,\beta\in T_x^*L$. This formula follows from the definition of the tautological one-form and the convention $\omega_{\mathrm{can}}=-d\lambda$. We compare this with $\omega_1=F^*\omega$. The tubular map $F$ was chosen with full first derivative \begin{align*} dF_{0_x}(u,\alpha)=di_x(u)+A_x\alpha \end{align*} for $u\in T_xL$ and $\alpha\in T_x^*L$. Hence \begin{align*} (\omega_1)_{0_x}\bigl((u,\alpha),(v,\beta)\bigr)=\omega_x(di_x(u)+A_x\alpha,di_x(v)+A_x\beta). \end{align*} Expanding by bilinearity gives four terms: \begin{align*} (\omega_1)_{0_x}\bigl((u,\alpha),(v,\beta)\bigr)=\omega_x(di_x(u),di_x(v))+\omega_x(di_x(u),A_x\beta)+\omega_x(A_x\alpha,di_x(v))+\omega_x(A_x\alpha,A_x\beta). \end{align*} Now each term has a verified reason. Since $L$ is Lagrangian, the tangent-tangent term is zero: \begin{align*} \omega_x(di_x(u),di_x(v))=0. \end{align*} The lift $A$ was constructed so that its image is Lagrangian in the vertical directions, so \begin{align*} \omega_x(A_x\alpha,A_x\beta)=0. \end{align*} The same construction gives the mixed pairing \begin{align*} \omega_x(A_x\alpha,di_x(v))=\alpha(v) \end{align*} and \begin{align*} \omega_x(A_x\beta,di_x(u))=\beta(u). \end{align*} Using skew-symmetry of $\omega_x$ on the remaining mixed term, \begin{align*} \omega_x(di_x(u),A_x\beta)=-\omega_x(A_x\beta,di_x(u))=-\beta(u). \end{align*} Substituting these four evaluations into the expansion yields \begin{align*} (\omega_1)_{0_x}\bigl((u,\alpha),(v,\beta)\bigr)=\alpha(v)-\beta(u). \end{align*} Thus \begin{align*} (\omega_1)_{0_x}=(\omega_0)_{0_x} \end{align*} for every $x\in L$.[/guided]

[step:Apply the relative Moser lemma to correct the preliminary map] Apply [citetheorem:10051] to the [smooth manifold](/page/Smooth%20Manifold) $T^*L$, the embedded submanifold $j(L)\subset T^*L$, and the symplectic forms $\omega_0$ and $\omega_1$ on the neighbourhood $U_0$ of $j(L)$. Its hypotheses hold: both forms are symplectic on $U_0$, and the previous step proves \begin{align*} (\omega_0)_{0_x}=(\omega_1)_{0_x} \end{align*} for every $x\in L$. After possibly shrinking $U_0$, the relative Moser lemma gives an open neighbourhood $U\subset U_0$ of $j(L)$ and a diffeomorphism \begin{align*} \psi:U\to \psi(U)\subset U_0 \end{align*} such that \begin{align*} \psi|_{j(L)}=\operatorname{id}_{j(L)} \end{align*} and \begin{align*} \psi^*\omega_1=\omega_0. \end{align*} [/step]

[step:Compose the correction with the tubular map] Define \begin{align*} \Phi:U&\to M \end{align*} by \begin{align*} \Phi=F\circ\psi. \end{align*} Let \begin{align*} V:=\Phi(U)=F(\psi(U)). \end{align*} Since $\psi$ and $F$ are diffeomorphisms onto their images, $\Phi:U\to V$ is a diffeomorphism. For $x\in L$, using the identification of $x$ with $0_x=j(x)$ in the zero section, \begin{align*} \Phi(0_x)=F(\psi(0_x))=F(0_x)=x, \end{align*} so \begin{align*} \Phi|_L=\operatorname{id}_L. \end{align*} Finally, \begin{align*} \Phi^*\omega=(F\circ\psi)^*\omega=\psi^*(F^*\omega)=\psi^*\omega_1=\omega_0=\omega_{\mathrm{can}}|_U. \end{align*} Thus $U$ is a neighbourhood of the zero section in $T^*L$, $V$ is a neighbourhood of $L$ in $M$, and $\Phi$ has the required properties. [/step]