# Showing calibration of Bayesian credible intervals

I'd like to try and understand how one can prove that a particular strategy for assessing correctness of computational methods for Bayesian inference is sound.

For a number $$M$$ of simulations, simulate \begin{align} \theta^{(i)} &\sim \pi(\cdot) \\ y^{(i)} \mid \theta^{(i)} &\sim f(\cdot \mid \theta^{(i)}) \end{align} Now compute a $$\gamma\%$$ credibility interval $$C^{(i)} := \left(a^{(i)}, b^{(i)})\right)$$ with $$a^{(i)} < b^{(i)}$$ such that $$Q\left(b^{(i)} \mid y^{(i)}\right) - Q\left(a^{(i)} \mid y^{(i)}\right) = p_1 - p_2 = \gamma,$$ where $$Q_{y}(x) = \frac{\int_{-\infty}^x f(y \mid t) \pi(t)\,dt}{\int_{-\infty}^\infty f(y \mid t) \pi(t)\,dt},$$ is the posterior CDF. A natural quantity to compute is $$S_M = M^{-1}\sum_{i=1}^M \mathbb{I}\left(\theta^{(i)} \in C^{(i)} \right)$$

Now, we are prepared to state the

Claim: If your method of drawing from $$p(\cdot \mid y)$$ is correct, then $$\lim_{M \to \infty} S_M = \gamma$$.

Here's a flimsy attempt at a proof: Let $$F_U(x) = x$$ be the CDF of a $$\operatorname{Uniform(0, 1)}$$ random variable. We may re-write the limit as \begin{align} \lim_{M \to \infty} S_M &= \lim_{M \to \infty} M^{-1}\sum_{i=1}^M \mathbb{I}\left(\theta^{(i)} \in C^{(i)} \right),\\ &= \lim_{M \to \infty} M^{-1}\sum_{i=1}^M \left\{ \mathbb{I}\left(\theta^{(i)} \leq b^{(i)} \right) - \mathbb{I}\left(\theta^{(i)} \leq a^{(i)} \right) \right\},\\ &= \lim_{M \to \infty} M^{-1}\sum_{i=1}^M \mathbb{I}\left(\theta^{(i)} \leq b^{(i)} \right) - M^{-1}\sum_{i=1}^M\mathbb{I}\left(\theta^{(i)} \leq a^{(i)} \right),\\ &= \lim_{M \to \infty} M^{-1}\sum_{i=1}^M \mathbb{I}\left(Q_{y^{(i)}}^{-1}(\theta^{(i)}) \leq p_1 \right) - M^{-1}\sum_{i=1}^M\mathbb{I}\left(Q_{y^{(i)}}^{-1}(\theta^{(i)}) \leq p_2 \right),\\ &= F_U(p_1) - F_U(p_2) = \gamma, \end{align} where the last line follows from the fact that the CDF of $$\theta^{(i)}$$ is uniformly distributed on $$(0, 1$$) (Theorem 1 in Cook et al. 2006) and almost sure convergence of the ECDF to the true CDF (Glivenko-Cantelli).

Questions: is this "proof" in the right direction? If not, can it be patched to get there? Are there any hidden assumptions (such as identifiability of the model) lurking in there?

I'm confident there is a simpler argument here, but I'm also quite interested in the identifiability thing: does this still hold when the model is not identified?

This could be seen as kind of/sort of follow-up of this question. This is also intimately related to Simulation-based Calibration (SBC), see this.