A Proper Mapping Theorem for coadmissible D-cap-modules

We study the behaviour of D-cap-modules on rigid analytic varieties under
pushforward along a proper morphism. We prove a D-cap-module analogue of
Kiehl's Proper Mapping Theorem, considering the derived sheaf-theoretic
pushforward from $\mathcal{D}_X$-cap-modules to $f_*\mathcal{D}_X$-cap-modules
for proper morphisms $f: X\to Y$. Under assumptions which can be naturally
interpreted as a certain properness condition on the cotangent bundle, we show
that any coadmissible $\mathcal{D}_X$-cap-module has coadmissible higher direct
images. This implies among other things a purely geometric justification of the
fact that the global sections functor in the rigid analytic
Beilinson--Bernstein correspondence preserves coadmissibility, and we are able
to extend this result to twisted D-cap-modules on analytified partial flag
varieties.