Given E\in A(n,q), q\in\{0,\ldots,n\}, we will write \operatorname{lin}(E) for the linear subspace in G(n,q) parallel to E. In other words, \operatorname{lin}(E)=E-x for all x\in E.
For the proof of Theorem 4.1, fix n\geq 1, q\in\{1,\ldots,n-1\} and \gamma\in\{0,\ldots,q-1\}, and let f: A(n, \gamma)\to [0,\infty) be a measurable function. Due to Lemma 3.1, we may assume without loss of generality that f is rotation invariant. The integral of interest is
I=
\int_{G(n,q)}\int_{A(n,n-q+\gamma)} f(E \cap L) H(E) \ \mu_{n-q+\gamma}(dE) \ \nu_{q}(dL).
First note that I is indeed well-defined as for \nu_q-almost all L \in G(n,q) and \mu_{n-q+\gamma}-almost all E \in A(n,n-q+\gamma) we have \dim (E \cap L)=\gamma. This follows from [SchWeil2008, Lem. 13.2.1], applied to L and L'=\operatorname{lin}(E).
Define the function g: A(n,q) \times A(n,n-q+\gamma) \to \mathbb{R} by
\begin{aligned}
g(E_1,E_2) = f\big(\operatorname{lin} (E_1) \cap E_2\big) 1_{\{d(o,E_1)\leq 1 \}}H(E_2),
\end{aligned}
where we let f(\operatorname{lin} (E_1) \cap E_2)=0 if \dim (\operatorname{lin} (E_1) \cap E_2)\ne \gamma. Definition (?) implies
I=\frac{1}{\kappa_{n-q}}
\int_{A(n,q)}\int_{A(n,n-q+\gamma)} g(E_1,E_2) \, \mu_{n-q+\gamma}(dE_2) \mu_{q}(dE_1).
Applying [SchWeil2008, Thm. 7.2.8] with s_1=q and s_2 = n-q+\gamma yields
\begin{aligned}
I
=
\frac{\Bar{b}}{\kappa_{n-q} }
\int_{A(n,\gamma)}
\int_{A(E,q)}
\int_{A(E,n-q+\gamma)}
& g(E_1,E_2) [\operatorname{lin}(E_1), \operatorname{lin}(E_2)]^{\gamma+1}
\\& \times \ \mu_{n-q+\gamma}^E (dE_2) \ \mu_{q}^E(dE_1) \ \mu_\gamma(dE),
\end{aligned}
with the constant \Bar{b} given by
\Bar{b}
=
b_{n,n-\gamma} \frac{
b_{n-\gamma,n-q}
b_{n-\gamma, q-\gamma}
}{
b_{n,n-q}
b_{n,q-\gamma}},\qquad b_{i,j} = {\omega_{i-j+1}\cdots\omega_{i}\over\omega_1\cdots\omega_j},\ i\in \mathbb{N},j\in\{1,\ldots,i\}.
Expanding (?) by decomposing the measure \mu_{\gamma} according to (?), applying [SchWeil2008, Eq. (13.14)] and Tonelli’s theorem yields
I
=
\frac{\Bar{b}}{\kappa_{n-q} }
\int_{G(n, \gamma)}
I_1(L_0,f) \ \nu_\gamma(dL_0)
with
\begin{aligned}
I_1(L_0,f)
& =
\int_{G(L_0,q)}
\int_{G(L_0,n-q+\gamma)}
\int_{L_0^\perp }
f((M+t)\cap L)
1_{\{d(o,L+t) \leq 1\}} H(M+t)
\\&
\hspace{4cm} \times \ \lambda_{L_0^\perp}(dt) [M, L]^{\gamma+1}\ \nu_{n-q+\gamma}^{L_0} (dM)
\ \nu_{q}^{L_0}(dL).
\end{aligned}
Since
\int_{G(L_0,p)} h(L) \ \nu_p^{L_0}(dL)
=
\int_{G(L_0^\perp, p-\gamma)} h(L_0+L) \ \nu_{p-\gamma}^{L_0^\perp}(dL)
for all L_0 \in G(n, \gamma) and for any measurable function h:G(L_0,p)\to[0,\infty) and integers \gamma < p <n, we conclude
\begin{split}
I_1(L_0,f) & =
\int_{G(L_0^\perp,q-\gamma)}
\int_{G(L_0^\perp,n-q)}
\int_{L_0^\perp }
f\Big(\big((M+t)\cap L\big)+ L_0 \Big) 1_{\{d(o,L+t) \leq 1\}} \\&
\qquad \qquad \times H(M+L_0+t) \ \lambda_{L_0^\perp}(dt)
[M, L]^{\gamma+1}
\ \nu_{n-q}^{L_0^\perp} (dM)
\ \nu_{q-\gamma}^{L_0^\perp}(dL),
\end{split}
where we also have used (M+L_0+t) \cap (L+L_0) = \big( (M+t) \cap L \big)+L_0, d(o,L+L_0+t)=d(o,L+t) and [M+L_0, L+L_0]= [M,L].
Now consider (?) for fixed L_0 \in G(n, \gamma), M \in G(L_0^\perp, n-q) and L \in G(L_0^\perp, q-\gamma). As f and H are both rotation invariant, we may write
\begin{aligned}
f\big(((M+t)\cap L)+ L_0\big)
&=
f_I\big( d(o, (M+t) \cap L) \big),
\\
H(M+L_0+t)&= H_I(\|t|M^\perp \|),
\end{aligned}
with f_I and H_I satisfying (?). Thus, we may identify L_0^\perp with \mathbb{R}^{n-\gamma} and conclude that
\begin{aligned}
I_1(L_0,f)
&=
\int_{G(n-\gamma,q-\gamma)}
\int_{G(n-\gamma,n-q)} I_2(L,M)
[M,L]^{\gamma+1} \nu_{n-q} (dM)
\ \nu_{q-\gamma}(dL),
\end{aligned}
with
\begin{aligned}
I_2(M,L)
&=
\int_{\mathbb{R}^{n-\gamma}}
f_I(d(o,(M+t)\cap L)) 1_{\{d(o,L+t) \leq 1\}} H_I(\|t|M^\perp \|)
\ \lambda_{ {n-\gamma}}(dt)
\\
&=
\int_{M} \int_{M^\perp}
f_I( d(o,(M+x)\cap L))
H_I(\|x \|) 1_{\{d(o,L+x+y) \leq 1\}} \
\ \lambda_{M^\perp}(dx) \ \lambda_M(dy)
\end{aligned}
for M \in G(n-\gamma, n-q) and L \in G(n-\gamma,q-\gamma). Applying (?) to the Lebesgue integral over M^\perp we get
\begin{aligned}
I_2(M,L) &= [M,L]
\int_{M} \int_{L}
f_I( d(o,(M+t)\cap L))
H_I(\|t|M^\perp \|) 1_{\{d(o,L+t|M^\perp+y) \leq 1\}} \
\ \lambda_{L}(dt) \ \lambda_M(dy)
\\
&
= \int_{L} f_I( d(o,(M+t)\cap L)) H_I(\|t|M^\perp \|) I_3(M,L,t) \ \lambda_{L}(dt),
\end{aligned}
where we first used the fact that M+t|M^\perp=M+t holds for any t \in L, and then Tonelli’s theorem. Here,
I_3(M,L,t) =[M,L]
\int_{M}
1_{\{\|(t| M^\perp)|L^\perp+y|L^\perp \| \leq 1\}} \
\lambda_M(dy).
Another application of (?) reveals that
I_3(M,L,t) = \int_{L^\perp}
1_{\{\|(t| M^\perp)|L^\perp+z \| \leq 1\}} \
\lambda_{L^\perp}(dz)=\kappa_{n-q}
is the volume of a unit ball in L^\perp, centered at (t| M^\perp)|L^\perp. Inserting this into I_2 gives
I_2(M,L)
= \kappa_{n-q} \int_{L} f_I( d(o,(M+t)\cap L)) H_I(\|t|M^\perp \|) \ \lambda_{L}(dt) .
Since t\in L and M\cap L=\{o\} for almost all L and M, we have
d(o,(M+t) \cap L)=
d(o,\{t\})=\|t\|.
This, and the use of spherical coordinates in L give
I_2(M,L)
=\kappa_{n-q}
\int_0^\infty f_I(r) r^{q-\gamma-1}
\int_{S^{n-\gamma-1}\cap L}
H_I(r [u,M])
\ \mathcal{H}^{q-\gamma-1}(du) \ dr.
Inserting this into (?) and the result into (?), we get after an application of Tonelli’s theorem that
\begin{aligned}
I
&=\bar{b}
\int_0^\infty f_I(r) r^{q-\gamma-1} \int_{G(n-\gamma,n-q)} J_H(M,r)
\ \nu_{n-q} (dM)
\ dr,
\end{aligned}
with
\begin{aligned}
J_H(M,r)=
\int_{G(n-\gamma,q-\gamma)}
\int_{S^{n-\gamma-1}\cap L}
H_I(r [u,M])\mathcal{H}^{q-\gamma-1}(du)
[M,L]^{\gamma+1}
\ \nu_{q-\gamma}(dL).
\end{aligned}
An invariance argument and [SchWeil2008, Thm. 7.1.1] imply
\begin{aligned}
J_H(M,r)=\frac{\omega_{q-\gamma}}{\omega_{n-\gamma}}
\int_{S^{n-\gamma-1}}
H_I(r [u,M])
\int_{G(\operatorname{span} u, q-\gamma)}
[M,L]^{\gamma+1}
\ \nu_{q-\gamma}^{\operatorname{span} u}(dL)
\ \mathcal{H}^{n-\gamma-1}(du) .
\end{aligned}
Applying Lemma 3.2 in \mathbb{R}^{n-\gamma} to the innermost integral in J_H(M,r) yields
J_H(M,r)
=
c_1\int_{S^{n-\gamma-1}}
H_I(r[u,M])
[u,M]^{\gamma+1}
\ \mathcal{H}^{n-\gamma-1}(du)
with the constant c_1=a(n-\gamma,n-q,q- \gamma,\gamma+1)\frac{\omega_{q-\gamma}}{\omega_{n-\gamma}}. To simplify J_H(M,r) further, we use the fact that [u,M]=\|u|M^\perp\| and apply [Auneau2010, Lem. 1] with B_p= M^\perp, p=q-\gamma and d= n-\gamma. This yields
\begin{aligned}
J_H(M,r)
&
= \frac{c_1}{2} \omega_{n-q} \omega_{q-\gamma}
\int_0^1
H_I(r t^{\frac{1}{2}}) t^{ \frac{q-1}{2}}(1-t)^{ \frac{n-q}{2}-1}
\ dt
\\
&=
c_1\omega_{n-q} \omega_{q-\gamma}
\int_0^1
H_I(r z) z^{ q}(1-z^2)^{ \frac{n-q}{2}-1}
\ dz,
\end{aligned}
using the substitution z= \sqrt{t} in the last step. A comparison with (4.1) gives J_H(M,r)=c_1\omega_{n-q} \omega_{q-\gamma} J_H(r), so abbreviating
c_2=\bar{b}c_1\frac{\omega_{n-q} \omega_{q-\gamma}}{\omega_{n-\gamma}},
(?) becomes
\begin{aligned}
I
&=c_2\omega_{n-\gamma}
\int_0^\infty f_I(r) r^{q-\gamma-1}J_H(r)\ dr
\\
&= c_2\int_{A(n, \gamma)}
f( E) d(o,E)^{-(n-q)} J_H(d(o,E)) \ \mu_\gamma(dE),
\end{aligned}
where we used (?) and spherical coordinates in \operatorname{lin}(E). Hence, the theorem is shown once we have confirmed that
c_2=D(n,q,\gamma).
We have
c_1
=\frac{\omega_{q-\gamma}}{\omega_{n-\gamma}}
\prod_{i=1}^{n-q}
\frac{\Gamma(\frac{n-\gamma-i}{2})
\Gamma(\frac{n-q-i+\gamma}{2}+1)
}
{
\Gamma( \frac{n-i+1}{2})
\Gamma( \frac{n-q-i+1}{2})
}
=
\frac{\omega_{q-\gamma}}{\omega_{n-\gamma}}
\prod_{i=1}^{n-q}
\frac{
\omega_{n-i+1}
\omega_{n-q-i+1}
}
{
\omega_{n-\gamma-i}
\omega_{n-q+\gamma+2-i}
},
so direct insertion gives
\begin{aligned}
\bar{b}c_1
&=
\Bigg(
\frac{
\omega_{\gamma+1}\cdots \omega_n
}
{
\omega_1 \cdots \omega_{n-\gamma}
}
\cdot
\frac{
\omega_{q-\gamma+1} \cdots \omega_{n-\gamma}
}
{
\omega_{q+1}\cdots \omega_{n}
}
\cdot
\frac{
\omega_{n-q+1}\cdots \omega_{n-\gamma}
}
{
\omega_{n-(q-\gamma)+1}\cdots \omega_{n}
}
\Bigg)
\\
&\hspace{4cm}\times
\Bigg(
\frac{
\omega_{q+1}\cdots \omega_n
}
{
\omega_{q-\gamma}
\cdots \omega_{n-\gamma-1}
}
\cdot
\frac{
\omega_{1}\cdots \omega_{n-q}
}
{
\omega_{\gamma+2}
\cdots
\omega_{n-(q-\gamma)+1}
}
\Bigg)\frac{\omega_{q-\gamma}}{\omega_{n-\gamma}}
\\
&=
\Bigg(
\frac{\omega_{q+1}\cdots \omega_{n}
}
{
\omega_{q+1}\cdots \omega_{n}
}
\cdot
\frac{
\omega_{\gamma+1}\cdots \omega_n
}
{
\omega_{\gamma+2}\cdots \omega_{n}
}
\cdot
\frac{1}{
\omega_{n-(q-\gamma)+1}
}
\Bigg)\\
&\hspace{4cm}\times
\Bigg(
\frac{
\omega_{q-\gamma} \cdots \omega_{n-\gamma}
}{
\omega_{q-\gamma}
\cdots \omega_{n-\gamma}}
\cdot\frac{
\omega_{1} \cdots \omega_{n-\gamma}
}
{
\omega_{1} \cdots \omega_{n-\gamma}
}
\Bigg)
\\
&=
\frac{\omega_{\gamma+1}}
{\omega_{n-(q-\gamma)+1}},
\end{aligned}
where the products were suitably sorted at the second equality sign, and simplified at the third equality sign. We thus get
c_2=\frac{\omega_{\gamma+1} \omega_{q-\gamma}\omega_{n-q}}{\omega_{n-(q-\gamma)-1}\omega_{n-\gamma}} =D(n,q,\gamma).
This shows (?) and completes the proof.