Help with definition of Liouville measure $\require{AMScd}$For a Riemannian manifold $M$, I have read authors talking about a 'Liouville measure' on the unit tangent bundle $\operatorname{T}^1(M)$ and then proceed to claim/prove that it is invariant under the geodesic flow.
See for example Mautner's $1957$ paper 'Geodesic Flows on Symmetric Riemann Spaces.'
This measure is loosely defined as 'the measure on $\operatorname{T}^1(M)$ locally defined by $\omega \wedge \theta$ where $\omega$ is the volume form on $M$ associated to the metric and $\theta$ is an invariant volume form on the sphere' (again, see equation ($17$) of Mautner's paper).
I would like a precise definition/construction of such a measure on a general symmetric space. I have seen the example of the upper half-plane where the unit tangent bundle can be identified with a group and one uses the Haar measure.
Setup:
Assume $(G,\mathfrak{g})$ is a non-compact, real, semi-simple, Lie group with finite center.
Fix a Cartan involution $\sigma: G \to G, d\sigma: \mathfrak{g} \to \mathfrak{g}$ which then induces the decomposition $\mathfrak{g}= \mathfrak{k}\oplus\mathfrak{p}$ into the $\pm 1$ eigenspaces respectively.
Moreover, if $K = G_{\sigma}$ (the fixed point set of $\sigma$), then $\operatorname{Lie}(K)= \mathfrak{k}$ and $K$ is compact since we assumed $G$ to have finite center.
One can also check that $\mathfrak{k}$ and $\mathfrak{p}$ are invariant under  $\operatorname{Ad}(K)$.
By giving $\mathfrak{p}$ an $\operatorname{Ad}(K)$-invariant inner product, one can induce a $G$-invariant Riemannian metric on the tangent bundle of $G/K$.
Additionally, $G/K$ has Riemannian geodesics of form $t\mapsto g\exp(tX)K$, with $X\in \mathfrak{p}$.
Perhaps the example to keep in mind is $\operatorname{SL}_n(\mathbb{R}) \simeq  \exp(\mathfrak{p}) \times \operatorname{SO}(n)$ where $\mathfrak{p}$ are symmetric, trace-zero matrices.
What I want: I would like to define a non-vanishing top form (Liouville measure) on $\operatorname{T}^1(G/K)$ which is 'locally of the type $\omega \wedge \theta$', where $\omega$ is the Riemannian volume form and $\theta$ is a non-vanishing top form on the sphere.
Note that $l_x$, left multiplication by $x\in G$, is an isometry on $G/K$.
And, of course, I would like the Liouville form to be invariant under the maps $dl_x$ so as to pass to the interesting class spaces $\operatorname{T}^1(\Gamma\backslash(G/K)) \simeq \Gamma\backslash \operatorname{T}^1(G/K)$, where $\Gamma$ is taken to be a freely acting lattice.
Lastly, I would like to know if there is some sort of uniqueness statement that can be formulated.
An attempt: A naive attempt would be to say that $\operatorname{T}^1(G/K) \simeq G/K \times S^d$ is a trivial sphere-bundle since $G/K\simeq \mathfrak{p}$ is contractible.
But I don't know how the action of $G$ would translate to $G/K \times S^d$.
Another attempt would be to use the commutative diagram
$$
\begin{CD}
G\times \mathfrak{p}_1 @>>> G \times_{K} \mathfrak{p}_1  \\
@V{\pi_1}VV @VV{\overline{q\circ\pi_1}}V \\
 G @>{q}>> G/K
\end{CD}$$
Here $\mathfrak{p}_1$ are the vectors in $\mathfrak{p}$ of norm $1$, $K$ acts on $G\times \mathfrak{p}_1$ on the right by
$$(g,Y)\cdot k := (gk,\operatorname{Ad}(k^{-1})Y),$$
and $G \times_{K} \mathfrak{p}_1$ is shorthand for the quotient by this action.
Note that $G \times_{K} \mathfrak{p}_1$ can be identified with $\operatorname{T}^1(G/K)$ by using the map
$$(g,Y) \mapsto (g\exp(tY)K)'_{t=0}.$$
Under this identification, the action of $dl_x: \operatorname{T}^1(G/K) \to \operatorname{T}^1(G/K)$ for $x\in G$ is intertwined with the action $x\cdot(g,Y)K := (xg,Y)K$ on the first coordinate.
Thus it perhaps makes sense to try and construct a form $\alpha$ (of appropriate dimension) on $G\times \mathfrak{p}_1$ which is invariant (under both the left action of $G$ on the first component and the right action of $K$ specified above) and is also $K$-horizontal, that is to say that the interior product $\iota_X \alpha =0$ whenever $X$ is a vector field induced by the action of $K$.
I guess such a form would induce a top form on $G\times_K \mathfrak{p}_1$ with the required properties?
Any help/references would be appreciated.
 A: The construction doesn’t really simplify on symmetric spaces. On $TM\cong T^*M$ (using the metric) consider the canonical 1-form $\alpha=“\langle p,dq\rangle”$ and symplectic form $d\alpha$ and hamiltonian vector field $\xi$ of $H=\frac12\|p\|^2$: $\mathrm i_\xi d\alpha=-dH$. Then $\alpha$ and $\xi$ restrict to a contact structure and its Reeb vector field on the level $T^1M$ of $H$:
$$
\mathrm i_\xi d\alpha = 0, \qquad\quad \mathrm i_\xi \alpha=1.
$$
Moreover the geodesic flow is the Reeb flow. (For this Besse cites Weinstein (1974) who cites Berger (1965) who doesn’t cite Reeb (1950).) Now $\mathrm L_\xi\alpha=\mathrm i_\xi d\alpha + d\mathrm i_\xi \alpha=0$, so that flow preserves $\alpha$ and hence the volume form
$$
\alpha\wedge(d\alpha)^{\dim M-1}
$$
of which Besse also gives a base $\times$ fiber description. Finally, any diffeo $g$ of $M$ lifts to a diffeo of $T^*M$ characterized by $\langle g(p),Dg(q)(\delta q)\rangle$ $=$ $\langle p,\delta q\rangle$, which  “by construction” preserves $\alpha$. When $g$ is an isometry, it also preserves $T^1M$ $\subset$ $TM$ $\cong$ $T^*M$ and hence everything in sight.
Added: This “Lie” view of geodesics as produced by a contact flow (1896, pp. 96-102) works directly on $\Gamma{\small\backslash} G/K$; it may not have been that of Mautner, Gelfand-Fomin, or Hopf — they seem closer to the (of course equivalent) idea of putting a canonical (“Sasaki”) metric on $TM$ and $T^1M$ and using the resulting volume form, as in e.g. Paternain (1999, 1.17) or Berger (2003, pp. 195, 359, 472).
