[proofplan] We first choose local coordinates whose derivative at $x_0$ identifies $\omega_{x_0}$ with the standard symplectic form. In those coordinates, we connect the constant standard form $\omega_0$ to the given form $\omega$ by the straight-line family $\omega_t=(1-t)\omega_0+t\omega$, after shrinking so every $\omega_t$ remains symplectic. The difference $\omega-\omega_0$ is exact locally, and a Moser vector field solving $\iota_{X_t}\omega_t=-\sigma$ produces an isotopy whose pullback freezes the family $\omega_t$. The time-one map then converts $\omega$ to $\omega_0$, and composing the original coordinates with this map gives the required Darboux coordinates. [/proofplan]

[step:Normalize the form at $x_0$ by choosing linear symplectic coordinates] Let $\Omega_{\mathrm{std}}$ denote the standard alternating form on $\mathbb R^{2n}$ defined by \begin{align*} \Omega_{\mathrm{std}}=\sum_{i=1}^n e_i^*\wedge e_{n+i}^*, \end{align*} where $(e_1,\dots,e_{2n})$ is the standard basis of $\mathbb R^{2n}$ and $(e_1^*,\dots,e_{2n}^*)$ is its [dual basis](/theorems/414). Since $\omega_{x_0}$ is a nondegenerate alternating form on the $2n$-dimensional [vector space](/page/Vector%20Space) $T_{x_0}M$, the [citetheorem:10037] gives a basis $(v_1,\dots,v_n,w_1,\dots,w_n)$ of $T_{x_0}M$ such that \begin{align*} \omega_{x_0}(v_i,w_j)=\delta_{ij},\qquad \omega_{x_0}(v_i,v_j)=0,\qquad \omega_{x_0}(w_i,w_j)=0 \end{align*} for all $1\le i,j\le n$. Choose a smooth coordinate chart \begin{align*} \psi:U_1\to \psi(U_1)\subset \mathbb R^{2n} \end{align*} with $x_0\in U_1$ and $\psi(x_0)=0$, and compose it with an invertible [linear map](/page/Linear%20Map) of $\mathbb R^{2n}$ so that \begin{align*} d\psi_{x_0}(v_i)=e_i,\qquad d\psi_{x_0}(w_i)=e_{n+i} \end{align*} for every $1\le i\le n$. Let $(y_1,\dots,y_{2n})$ denote the coordinate functions of this adjusted chart. Define the constant $2$-form $\omega_0$ on $U_1$ by \begin{align*} \omega_0=\sum_{i=1}^n dy_i\wedge dy_{n+i}. \end{align*} The preceding choice of coordinates gives \begin{align*} (\omega_0)_{x_0}=\omega_{x_0}. \end{align*} [/step]

[step:Shrink the coordinate neighbourhood so the straight-line forms are symplectic] For $t\in[0,1]$, define the smooth $2$-form \begin{align*} \omega_t=(1-t)\omega_0+t\omega \end{align*} on $U_1$. Each $\omega_t$ is closed because $d\omega_0=0$ in the chosen coordinates and $d\omega=0$ since $\omega$ is symplectic. At $x_0$, \begin{align*} (\omega_t)_{x_0}=(1-t)(\omega_0)_{x_0}+t\omega_{x_0}=\omega_{x_0}, \end{align*} so $(\omega_t)_{x_0}$ is nondegenerate for every $t\in[0,1]$. Nondegeneracy is an open condition on alternating bilinear forms. Since $[0,1]$ is compact and the map $(t,x)\mapsto(\omega_t)_x$ is smooth, there is an open neighbourhood $U_2\subset U_1$ of $x_0$ such that $(\omega_t)_x$ is nondegenerate for every $x\in U_2$ and every $t\in[0,1]$. Replacing $U_1$ by $U_2$, we may assume that each $\omega_t$ is a symplectic form on $U_2$. [/step]

[step:Choose a local primitive for $\omega-\omega_0$ vanishing at $x_0$] Define the closed $2$-form \begin{align*} \alpha=\omega-\omega_0 \end{align*} on $U_2$. Since $\alpha_{x_0}=0$ and $d\alpha=d\omega-d\omega_0=0$, replace $U_2$ by an open coordinate ball containing $x_0$ whose image under $(y_1,\dots,y_{2n})$ is star-shaped with respect to $0$. For the embedded submanifold $N=\{x_0\}\subset U_2$, the restriction of $\alpha$ to $N$ is zero because $\alpha_{x_0}=0$. Applying the [citetheorem:10050] to this closed $2$-form near $N$ gives a $1$-form $\tau$ on the shrunken $U_2$ satisfying \begin{align*} d\tau=\alpha. \end{align*} Moreover, the primitive may be chosen so that $\tau_{x_0}=0$; the subtraction below is therefore harmless but keeps the normalization explicit. Let $\ell$ be the constant $1$-form, in the coordinates $(y_1,\dots,y_{2n})$, whose value at every point is $\tau_{x_0}$. Define \begin{align*} \sigma=\tau-\ell. \end{align*} Since $d\ell=0$, we have \begin{align*} d\sigma=d\tau=\omega-\omega_0. \end{align*} Also $\sigma_{x_0}=0$ by construction. After this shrink, still denoted $U_2$, all $\omega_t$ remain symplectic on $U_2$. [/step]

[step:Solve Moser's equation and integrate the resulting vector field]For each $t\in[0,1]$ and each $x\in U_2$, nondegeneracy of $(\omega_t)_x$ implies that the linear map \begin{align*} T_xU_2&\to T_x^*U_2 \end{align*} given by $v\mapsto \iota_v(\omega_t)_x$ is an isomorphism. Therefore there is a unique vector $X_t(x)\in T_xU_2$ satisfying \begin{align*} \iota_{X_t(x)}(\omega_t)_x=-\sigma_x. \end{align*} Smooth dependence on $(t,x)$ follows from smooth inversion of the coefficient matrix of $\omega_t$ in the coordinates $(y_1,\dots,y_{2n})$. Thus we obtain a smooth time-dependent vector field \begin{align*} X:[0,1]\times U_2&\to TU_2 \end{align*} with $X(t,x)=X_t(x)$. Because $\sigma_{x_0}=0$ and $(\omega_t)_{x_0}$ is nondegenerate, the defining equation gives $X_t(x_0)=0$ for all $t\in[0,1]$. By local existence and smooth dependence of flows for time-dependent vector fields, after shrinking to an open neighbourhood $U_3\subset U_2$ of $x_0$, the flow \begin{align*} \psi_t:U_3\to U_2 \end{align*} of $X_t$ exists for every $t\in[0,1]$, satisfies $\psi_0=\operatorname{id}_{U_3}$, and satisfies \begin{align*} \frac{d}{dt}\psi_t(x)=X_t(\psi_t(x)) \end{align*} for all $x\in U_3$. The inverse-flow part of the same local flow theorem gives, after this shrink, that each $\psi_t$ is a diffeomorphism from $U_3$ onto its image $\psi_t(U_3)\subset U_2$. Since $X_t(x_0)=0$, uniqueness of solutions to ordinary differential equations gives $\psi_t(x_0)=x_0$ for every $t\in[0,1]$.[/step]

[guided]The role of this step is to convert the problem of normalizing a $2$-form into an [ordinary differential equation](/page/Ordinary%20Differential%20Equation). For each fixed $t\in[0,1]$ and $x\in U_2$, the form $(\omega_t)_x$ is nondegenerate. This means the contraction map \begin{align*} T_xU_2&\to T_x^*U_2 \end{align*} defined by $v\mapsto \iota_v(\omega_t)_x$ is a linear isomorphism. Hence the equation \begin{align*} \iota_{X_t(x)}(\omega_t)_x=-\sigma_x \end{align*} has exactly one solution $X_t(x)\in T_xU_2$. This is Moser's equation. The sign is chosen so that the later derivative computation cancels: the variation of the forms is $\dot{\omega}_t=\omega-\omega_0=d\sigma$, while the Lie derivative contribution will contain $d(\iota_{X_t}\omega_t)=-d\sigma$. We also need $X_t$ to be a smooth time-dependent vector field, not merely a pointwise-defined vector. In the coordinates $(y_1,\dots,y_{2n})$, the form $\omega_t$ is represented by a smooth family of invertible skew-symmetric matrices. Matrix inversion is smooth on the [open set](/page/Open%20Set) of invertible matrices, so the solution vector $X_t(x)$ depends smoothly on $(t,x)$. Thus \begin{align*} X:[0,1]\times U_2&\to TU_2 \end{align*} given by $X(t,x)=X_t(x)$ is smooth. At the base point $x_0$, the primitive was arranged to satisfy $\sigma_{x_0}=0$. Therefore Moser's equation becomes \begin{align*} \iota_{X_t(x_0)}(\omega_t)_{x_0}=0. \end{align*} Because $(\omega_t)_{x_0}$ is nondegenerate, this forces $X_t(x_0)=0$ for every $t\in[0,1]$. Finally, we integrate $X_t$. The local flow theorem for smooth time-dependent vector fields gives a flow after possibly shrinking the initial neighbourhood of $x_0$; its inverse-flow statement also gives that each time-$t$ map is a diffeomorphism from its domain onto its image. Thus there is an open neighbourhood $U_3\subset U_2$ of $x_0$ and smooth maps \begin{align*} \psi_t:U_3\to U_2 \end{align*} defined for all $t\in[0,1]$, with $\psi_0=\operatorname{id}_{U_3}$ and \begin{align*} \frac{d}{dt}\psi_t(x)=X_t(\psi_t(x)). \end{align*} Since the constant curve $t\mapsto x_0$ also solves this differential equation and has initial value $x_0$, uniqueness gives $\psi_t(x_0)=x_0$ for all $t\in[0,1]$.[/guided]

[step:Show the Moser flow makes the pulled-back form independent of $t$] We compute the derivative of the pulled-back family $\psi_t^*\omega_t$. The standard time-dependent pullback formula for a flow, obtained from Cartan's formula for the Lie derivative of differential forms, gives \begin{align*} \frac{d}{dt}(\psi_t^*\omega_t)=\psi_t^*(\dot{\omega}_t+\mathcal L_{X_t}\omega_t). \end{align*} Since \begin{align*} \dot{\omega}_t=\omega-\omega_0=d\sigma, \end{align*} and since $d\omega_t=0$, Cartan's formula gives \begin{align*} \mathcal L_{X_t}\omega_t=d(\iota_{X_t}\omega_t)+\iota_{X_t}(d\omega_t)=d(-\sigma)+0=-d\sigma. \end{align*} Therefore \begin{align*} \dot{\omega}_t+\mathcal L_{X_t}\omega_t=d\sigma-d\sigma=0. \end{align*} It follows that \begin{align*} \frac{d}{dt}(\psi_t^*\omega_t)=0. \end{align*} Hence $\psi_t^*\omega_t$ is independent of $t$. Evaluating at $t=0$ and $t=1$ gives \begin{align*} \psi_1^*\omega=\omega_0|_{U_3}. \end{align*} [/step]

[step:Compose the inverse time-one map with the original coordinates to obtain Darboux coordinates] Set \begin{align*} V=\psi_1(U_3)\subset U_2. \end{align*} Since $\psi_1:U_3\to V$ is a diffeomorphism and $\psi_1(x_0)=x_0$, the set $V$ is an open neighbourhood of $x_0$. Let \begin{align*} \varphi:V\to \mathbb R^{2n} \end{align*} be the smooth map defined by \begin{align*} \varphi=\psi\circ\psi_1^{-1}. \end{align*} After shrinking $U_3$ further if necessary, $\varphi$ is a coordinate chart because $\psi$ is a coordinate chart and $\psi_1^{-1}:V\to U_3$ is a diffeomorphism. Since $\psi_1^{-1}(x_0)=x_0$ and $\psi(x_0)=0$, we have $\varphi(x_0)=0$. Let $(q_1,\dots,q_n,p_1,\dots,p_n)$ denote the coordinate functions of $\varphi$, so \begin{align*} q_i=y_i\circ\psi_1^{-1},\qquad p_i=y_{n+i}\circ\psi_1^{-1} \end{align*} for $1\le i\le n$. The identity $\psi_1^*\omega=\omega_0|_{U_3}$ is equivalent, after pulling back by $\psi_1^{-1}:V\to U_3$, to \begin{align*} \omega|_V=(\psi_1^{-1})^*\omega_0. \end{align*} Using the definition of $\omega_0$, we obtain \begin{align*} (\psi_1^{-1})^*\omega_0=\sum_{i=1}^n d(y_i\circ\psi_1^{-1})\wedge d(y_{n+i}\circ\psi_1^{-1})=\sum_{i=1}^n dq_i\wedge dp_i. \end{align*} Therefore \begin{align*} \omega|_V=\sum_{i=1}^n dq_i\wedge dp_i \end{align*} on the coordinate neighbourhood $V$. Thus $(q_1,\dots,q_n,p_1,\dots,p_n)$ are Darboux coordinates centered at $x_0$, completing the proof. [/step]