Smooth singular value decomposition on the symplectic group and Lyapunov exponents approximation

We give a constructive argument to establish existence of a smooth singular value decomposition (SVD) for a generic $C^k$ symplectic function X. We rely on the explicit structure of the polar factorization of X in order to justify the form of the SVD. Our construction gives a new algorithm to find the SVD of X, which we have used to approximate the Lyapunov exponents of a Hamiltonian differential system. Algorithmic details and an example are given.