Posterior credible set

Let $(\mathrm{\Theta },\mathcal{T})$ and $(\mathsf{Y},\mathcal{Y})$ be measurable spaces and let $y\mapsto {\mathrm{\Pi }}_y$ be a supplied posterior probability kernel. For $\alpha \in [0,1]$, a set-valued rule $C$ is graph-measurable when $\{(y,\theta )\in \mathsf{Y}\times \mathrm{\Theta }:\theta \in C(y)\}\in \mathcal{Y}\otimes \mathcal{T}\mathrm{.}$ It is a posterior credible set at level $1-\alpha$ when it is graph-measurable and ${\mathrm{\Pi }}_y(C(y))\ge 1-\alpha \text{for every }y\text{ in its declared data domain}\mathrm{.}$ The posterior-mass function is measurable by integration of the indicator of the membership graph against the kernel. If a density is available relative to a specified dominating measure, a highest-posterior-density region selects parameter values with largest density; such regions need not be intervals and may be disconnected or nonunique.

On a real parameter space, equal-tailed intervals formed from posterior quantiles are one choice; Equal-tailed posterior quantile intervals are credible proves their mass bound.