Formal geometric quantisation for proper actions

We define formal geometric quantisation for proper Hamiltonian actions by possibly noncompact groups on possibly noncompact, prequantised symplectic manifolds, generalising work of Weitsman and Paradan. We study the functorial properties of this version of formal geometric quantisation, and relate it to a recent result by the authors via a version of the shifting trick. For (pre)symplectic manifolds of a certain form, quantisation commutes with reduction, in the sense that formal quantisation equals a more direct version of quantisation.