1: \begin{proof}

2: We have

3: \begin{equation}\label{eq:boundi}

4: \Vert z(t_n) - z^{n,h}_0\Vert_{L^2} \leq \Vert z(t_n) - z_0(t_n)\Vert_{L^2} + \Vert z_0(t_n) - z^{n,h}_0\Vert_{L^2}.

5: \end{equation}

6: By Theorem \ref{thm:main} we have over the time interval $(0,T)$ and $c > c_0$,

7: \begin{equation}\label{eq:boundi1}

8: \Vert z(t_n) - z_0(t_n)\Vert_{L^2}\leq C  c^{-2}.

9: \end{equation}

10: To bound the second term we use the following inequality

11: \begin{equation*}

12: \begin{aligned}

13: \Vert z_0(t_n) - z^{n,h}_0\Vert_{L^2} &\leq  \Vert\mathrm{e}^{ic^2t_n}( u_0(t_n) - u_0^{n,h})\Vert_{L^2}+\Vert \mathrm{e}^{ic^2t_n}(v_0(t_n) - v_0^{n,h})\Vert_{L^2}\\

14: &\leq  \Vert  u_0(t_n) - u_0^{n,h} \Vert_{L^2}+\Vert v_0(t_n) - v_0^{n,h} \Vert_{L^2}.

15: \end{aligned}

16: \end{equation*}

17: Using arguments similar to  \cite[Theorem IV.17]{Faou12} (see also \cite{Lubich08}), it is then possible to prove that 

18: \begin{equation}

19: \label{eq:umun}

20: \Vert   u_0(t_n) - u_0^{n,h}\Vert_{L^2}+\Vert  v_0(t_n) - v_0^{n,h}\Vert_{L^2} \leq C( \tau^2 + h^{s} ), 

21: \end{equation}

22: if the exact solution is smooth enough (i.e. belongs to some Sobolev space $H^{s'}$ with $s' > s$ sufficiently large). Note that the proof of the fully discrete scheme in \cite{Faou12} is given only for the Lie-splitting, real initial data (that is $\varphi$ and $\gamma$ real valued functions) and uses function spaces based on the Wiener algebra (the $\ell_s^1$ spaces). However, the rigorous proof of \eqref{eq:umun} is essentially a variation on the same theme and does not present any particular difficulty as soon as the solution is smooth enough. 

23: Using this bound, we obtain that 

24: \begin{equation}\label{eq:boundi2}

25: \Vert z_0(t_n) - z^{n,h}_0\Vert_{L^2} \leq C( \tau^2 + h^{s} ).

26: \end{equation}

27: Plugging the bounds \eqref{eq:boundi1} and \eqref{eq:boundi2} into \eqref{eq:boundi} yields the desired convergence result.

28: \end{proof}

29: