The integrand is invariant under \(A_{G,H}(F)\) (germs are translation invariant), continuous on the open set \(T_\natural \) and \(0\) off it; so its descent to the quotient is measurable.

Let \(x=t_0\in T_\natural \), so \(T=T_x\), and \(t\in T\) near \(x\). The kernel dimension of a continuous family of linear maps is upper semicontinuous. Since \(W'_x\subseteq W'_t=\ker (v\mapsto t\iota (v)-\iota (v)t)\), this gives \(W'_t=W'_x\). Likewise the moved part \(\mathfrak l_t\) of \(\mathfrak g_t\) contains \(\mathfrak l_x\) (for \(Z\in \mathfrak l_x\) and small \(c\neq 0\), \(e^{cZ}\in T_x\) commutes with \(t\)), so \(\mathfrak l_t=\mathfrak l_x\) is abelian. The element \(t\) is semisimple (elements of \(T_x\) are, by the next lemma), so Steinberg’s description of centralizers gives \(T_t\subseteq T_x\), and \(T_x\subseteq T_t\) because \(T_x\) is commutative.

Write \(x=s+n\) (Jordan–Chevalley decomposition of left multiplication, \(s,n\in K[x]\)). Conjugation by \(x\) is \(c_s+N\) with \(c_s=\mathrm{Ad}(s)\) semisimple and \(N\) nilpotent, so by uniqueness \(N\) is a polynomial in \(\mathrm{Ad}(x)\); on \(\iota (V)\) it is that polynomial in \(P(x)\), nilpotent and semisimple, hence \(0\). So \(s^{-1}x\) is even and commutes with \(\iota (V)\), hence is a scalar, and \(x\) is a scalar multiple of \(s\). It is used for \(t\in T_x\), \(x\in \Gamma (G,H)\), whose image \(P(t)\) is semisimple (\(P(t)\) is scalar on the eigenlines of \(P(x)\) and an isometry of the nondegenerate plane \(E_{-1}\)).

The integrand is the product of \(D^G(t)^{1/2}c_{\theta ,\mathcal O_t}(t)\) (next lemma) and \(\Delta (t)^{s-1/2}\). On \(T_\natural \), \(W''_t=W''_x\) (\(P(t)\) is \(1\) on \(W'_x\) and preserves \(W''_x\), and dimensions agree), so \(\Delta (t)=|\det (P(t)-1)|_{W''_x}|_F\), continuous and nonzero; and \(|\cdot |_F\) is locally constant on \(F^\times \).

Product of the next two lemmas.

Fix \(x\in T_\natural \) and let \(N_t=1-\mathrm{Ad}(t)\) on \(\mathfrak g\), \(L=\ker N_x=\mathfrak g_x\), \(C=\mathrm{im}\, N_x\). As \(N_x\) is semisimple, \(\mathfrak g=L\oplus C\), and both are \(N_t\)-stable for \(t\in T\). On \(T_\natural \) the centralizers in \(G(F)\) of \(t\) and \(x\) agree (by the centralizer theorem over \(\bar F\)), hence so do the Lie centralizers (exponentiate), so \(\ker N_t=L\), \(N_t|_C\) is invertible and \(D^G(t)=|\det (N_t|_C)|_F\), continuous in \(t\).

Near \(t_0\in T_\natural \) write \(t=t_0e^Y\) with \(Y=\log (t_0^{-1}t)\) small (a local logarithm from the inverse function theorem). \(Y\) lies in \(\mathfrak g\), is semisimple and central in \(\mathfrak g_{t_0}=\mathfrak g_t\), so \(\theta (te^X)=\theta (t_0e^{X+Y})=\sum c_{\mathcal O}\hat{j}(\mathcal O,X+Y)=\sum c_{\mathcal O}\hat{j}(\mathcal O,X)\): the trace form is nondegenerate on \(\mathfrak g_{t_0}\), \(b(Y,N)=0\) for nilpotent \(N\in \mathfrak g_{t_0}\), and the regular set of \(\mathfrak g_{t_0}\) is open. The expansion at \(t_0\) is one at \(t\), and \(\mathcal O_t=\mathcal O_{t_0}\).

Near a regular semisimple \(Z_0\), \(\dim \ker (\operatorname {ad}Z)^D\le \dim \ker (\operatorname {ad}Z_0)^D=\dim \mathfrak g_{x,Z_0}=\ell \) (semicontinuity of the rank). For the Jordan decomposition \(Z=s+n\) in \(\mathfrak g_x\), \(\mathfrak g_{x,s}\subseteq \ker (\operatorname {ad}Z)^D\), so \(\dim \mathfrak g_{x,s}=\ell \); by the rank clauses for \(\mathrm{GSpin}\) (the pair version of the bound \(\dim \mathfrak {so}(V)_N\ge \lfloor \dim V/2\rfloor \)), \(\mathfrak g_{x,s}\) is then abelian and its only nilpotent element is \(0\), so \(n=0\) and \(Z=s\) is regular semisimple.

Not yet formalized. [ 5 ] Prop. 4.5.1 for the individual germs, and compactness of \(T(F)/A_{G,H}(F)\).

Not verbatim in the literature (adapted from, or derived from, published results); not yet formalized. Ingredients: [ 5 ] , Lemma B.1.2(i), applied as in Thesis Prop. 12.1.1(i).

Bounded germs times the integrable \(\Delta ^{s-1/2}\).

Not yet formalized. Induction on \(\dim G\): semisimple descent away from \(1\), descent to the Lie algebra and homogeneity near \(1\).

Linearity of \(m_{\mathrm{geom},s}\) for \(s{\gt}0\) and the limit for each \(\chi \).

From convergence.

Not verbatim in the literature (adapted from, or derived from, published results); not yet formalized. Ingredients: [ 10 ] , Part I; [ 5 ] , Prop. 3.1.1(i) (= Thesis Prop. 3.5.1(i)), adapted.

\(\Gamma (G,H)\) is a finite union of images of tori compact modulo \(A_{G,H}(F)\); take \(\Omega \) around them; germs only depend on \(\theta \) near the point.