Geometric ergodicity of a random-walk metorpolis algorithm via variable transformation and computer aided reasoning in statistics.

Abstract

With the steady increase of affordable computing, more and more often analysts are turning to computationally intensive techniques like Markov chain Monte Carlo (MCMC). To properly quantify the quality of their MCMC estimates, analysts need to know how quickly the Markov chain converges. Geometric ergodicity is a very useful benchmark for how quickly a Markov chain converges. If a Markov chain is geometrically ergodic, there are easy to use consistent estimators of the Monte Carlo standard errors (MCSEs) for the MCMC estimates, and an easy to use Central Limit Theorem for the MCMC estimates. We provide a method for finding geometrically ergodic Markov chains for classes of target densities. This method uses variable transformation to induce a proxy target distribution, and a random-walk Metropolis algorithm for the proxy target distribution will be geometrically ergodic. Because the transformations we use are one-to-one, Markov chains generated for the proxy target density can be transformed back to a sample from the original target density without loss of inference. Furthermore, because the Markov chain for the proxy distribution is geometrically ergodic, the consistent MCSEs and the CLT apply to the sample on the scale of original target density. We provide example applications of this technique to multinomial logit regression and a multivariate T distribution. Computer Aided Reasoning (CAR) uses a computer program to assist with mathematical reasoning. Proofs done in a proof assistant program are done formally, every step and inference is validated back to the axioms and rules of inference. Thus we have higher confidence in the correctness of a formally verified proof than one done with the traditional paper-and-pencil technique. Computers can track many more details than can be done by hand, so more complicated proofs with more cases and details can be done in CAR than can be done by hand, and proof assistant programs can help fill in the gaps in a proof. We give a brief overview of the proof assistant program HOL Light, and use it to formally prove the Markov inequality with an expectation based approach.