Smoothness and compact support of an affine-family integral

Let $E$ and $F$ be finite-dimensional real normed spaces, and let $\Psi : F \to \mathbb{C}$ be $C^\infty$ (in the sense of ContDiff ℝ ⊤) with compact support. Let $P$ be a topological space carrying a measurable structure that is the Borel structure of its topology, and let $\mu$ be a finite measure on $P$. Suppose $K \subseteq P$ is compact with $\mu(K^{c}) = 0$, so that $\mu$ is carried by $K$. Let $c : P \to \mathbb{C}$ be continuous, let $A : P \to (E \to_{L[\mathbb{R}]} F)$ be a continuous family of continuous $\mathbb{R}$-linear maps, and let $b : P \to F$ be continuous. Assume there is a real constant $C$ with the uniform properness bound $\|e\| \le C\,(\|A(p)e\| + 1)$ for all $p \in K$ and all $e \in E$. Then the function

on $E$ is $C^\infty$ and has compact support; both assertions are delivered as a conjunction.

This is differentiation under the integral sign, in a form adapted to an affinely parametrised family of arguments of a fixed smooth compactly supported test function, with the uniform properness hypothesis supplying the compactness of the support of the resulting integral. It serves as the abstract regularity statement for archimedean factors of integrated kernels, and is used in the treatment of twisted unipotent terms, in particular by AutomorphicForm.TwistedBruhat.continuous_and_hasCompactSupport_and_contDiff_integral_archWord and AutomorphicForm.TwistedBruhat.exists_forall_integral_transversal_eq_indicator_mul_prod_unipotentOrbitalFn_unram.