Lipschitz regularity of sub-elliptic harmonic maps into CAT(0) spaces

We prove the local Lipschitz continuity of sub-elliptic harmonic maps between certain singular spaces, more specifically from the $n$-dimensional Heisenberg group into $CAT(0)$ spaces. Our main theorem establishes that these maps have the desired Lipschitz regularity, extending the H\"older regularity in this setting proven by Y. Gui et. al and obtaining same regularity as in the work of H-C. Zhang and X-P. Zhu for certain sub-Riemannian geometries, see also the works of A. Mondino and D. Semola, as well as N. Gigli, for generalisations to RCD spaces. The present result paves the way for a general regularity theory of sub-elliptic harmonic maps, providing a versatile approach applicable beyond the Heisenberg group.