The Metropolized Hamiltonian chain preserves its target

Given: AC, $d,U,Z_U,M,ϵ,L$ as in the Statement and the finite leapfrog HMC procedure.

AC states that every family of nonempty sets has a choice function. The Axiom of Choice

AC implies Countable Choice, as used by the volume-preservation supplier. AC supplies countable selections and prescribed serial paths

Hamiltonian Monte Carlo defines $\pi$, $K$, $H$, and the refreshed momentum law $N_d(0,M)$.

Leapfrog Hamiltonian Monte Carlo uses the flipped deterministic proposal and the acceptance probability $\min \{1,\exp (-H(z^{\ast })+H(z))\}$.

For SPD $M$, $N_d(0,M)$ has Lebesgue density $(2\pi {)}^{-d\mathrm{/}2}\det (M{)}^{-1\mathrm{/}2}\exp (-p^T{M}^{-1}p\mathrm{/}2)$. A positive-definite multivariate normal law has its Gaussian density

The Borel space of finite-dimensional Euclidean phase space is standard Borel. Finite-dimensional Euclidean space with its Borel sigma-algebra is standard Borel

The kick, drift, and momentum flip maps are continuous; their composition $T=R\circ {\mathrm{\Phi }}_{ϵ}^L$ is continuous, involutive, and volume-preserving. One-step leapfrog map as force and drift shears, Leapfrog is reversible and volume-preserving

A measurable map $T$ gives the deterministic probability kernel $Q_T(z,A)={\delta }_{Tz}(A)$; continuous preimages of Borel sets are Borel. Measure kernel and probability kernel, The Dirac set function at a point, A continuous map has Borel preimages of Borel sets

The coordinate swap on a finite product is measurable, so transposing the proposal flow defines a measure. Coordinate maps and permutations are measurable on finite products

For a target probability $\nu$ and proposal kernel $Q$, the general Metropolis-Hastings construction uses the greatest common submeasure of the forward flow and its transpose; its acceptance function is a version of the Radon-Nikodym derivative. Metropolis–Hastings kernel

If two finite measures have densities $f,g$ with respect to one sigma-finite measure, their greatest common submeasure has density $\min \{f,g\}$. The common submeasure of two finite densities

The general Metropolis-Hastings output kernel is reversible and invariant for its target probability. Metropolis–Hastings flow is reversible and invariant

Each ${\lambda }_d$ is Lebesgue measure from Lebesgue measurable sets, the family $\mathcal{L}({\mathbb{R}}^n)$, and the restricted set function ${\lambda }_n$, restricted to Borel sets. Under Countable Choice, the Borel product agrees with Euclidean Lebesgue measure on Borel phase sets; finite products of sigma-finite measures exist, are unique on measurable rectangles, and obey Tonelli, while finite sums of measures are measures. On Borel subsets of R^{m+n}, the product lambda_m times lambda_n agrees with lambda_{m+n}, For sigma-finite factors, the product measure exists, has the rectangle formula, is sigma-finite, and is unique, Tonelli's theorem for nonnegative measurable functions on a sigma-finite product, Nonnegative scalar multiples and countable weighted sums of measures are measures

Scalar multiples, pointwise-defined sums, products, absolute values, and finite maxima and minima of measurable real-valued functions are measurable. Arithmetic and lattice operations preserve measurability whenever they are defined

A probability measure and a probability kernel define a probability measure on their product space by iterated integration. A prior and model kernel define a joint law

A measurable measure-preserving map $T$ satisfies $\int h\circ Td\lambda =\int hd\lambda$ for every nonnegative measurable $h$. Measure-preserving transformations and systems, Integral invariance under measure-preserving maps

Probability kernels compose by integration; the composition is a probability kernel and is associative. Composition of probability kernels, Kernel composition is well defined and associative

For product-measurable $C$, the refresh formula $S(q,C)=\int {\mathbf{1}}_C(q,p)N_d(0,M)(dp)$ defines a probability kernel from positions to phase space: for fixed $q$ the section measure is countably additive with mass one, and kernel integration makes its evaluation measurable in $q$. The product sigma-algebra and its finite iterates, Probability measures and probability spaces, Every section of a product-measurable function is measurable, Measurability of integration against a kernel

The continuous position projection ${\mathrm{pr}}_q(q,p)=q$ defines the deterministic probability kernel $J((q,p),A)={\mathbf{1}}_A(q)$. The Dirac set function at a point, Measure kernel and probability kernel, A continuous map has Borel preimages of Borel sets

The phase density $\rho$ is finite-valued, strictly positive, and Borel on $E={\mathbb{R}}^{2d}$. Write $P_q(q,p)=q$, $P_p(q,p)=p$, and $K(p)=\frac{1}{2}{\sum }_{i,j=1}^d(M^{-1}{)}_{ij}{p}_i{p}_j$. The Euclidean coordinate projections $P_q,P_p$ and scalar coordinate maps $p_i:E\to \mathbb{R}$ are continuous (each projection does not increase Euclidean distance). Since $U$ is continuous, for each Borel $B\subseteq \mathbb{R}$ the set $(U\circ P_q{)}^{-1}(B)=P_q^{-1}(U^{-1}(B))$ is Borel by the continuous-preimage theorem. The finite coordinate formula and [F12] make $K\circ P_p$ Borel. The same inverse-image identity, using continuity of the exponential, shows that $e^{-U\circ P_q}$ and $e^{-K\circ P_p}$ are Borel. Their product with the positive normalizing constant in [F1] and [F3] is $\rho$; it is finite and strictly positive because $U,K$ are real-valued and the exponential is positive. Hamiltonian Monte Carlo, A positive-definite multivariate normal law has its Gaussian density, Arithmetic and lattice operations preserve measurability whenever they are defined, A continuous map has Borel preimages of Borel sets, The exponential function is strictly increasing, The exponential is positive and satisfies $\exp (-x)=1\mathrm{/}\exp (x)$

For a probability measure $m$ and probability kernel $K$, $(mK)(A)=\int K(x,A)m(dx)$; invariance means $mK=m$. Invariant and stationary distribution for a Markov kernel

If $\tau$ is measurable, then $C\mapsto \mu ({\tau }^{-1}C)$ is a measure, since inverse images preserve disjoint unions and countable unions. Measures on sigma-algebras, A measurable function between measurable spaces

Integrating a nonnegative measurable function against a Dirac probability measure evaluates it at the point. Integration against a Dirac measure evaluates at its point

For every product-measurable $C\subseteq E\times E$, the graph map $G_T(z)=(z,Tz)$ is measurable: $z\mapsto z$ and the continuous map $T$ are measurable, so the finite-product coordinate-map lemma applies. Hence $z\mapsto {\mathbf{1}}_C(z,Tz)\rho (Tz)$ is nonnegative Borel by [F12] and [F18]. Also, on $E\times E$, the first-coordinate projection is measurable because the preimage of each Borel $A\subseteq E$ is $A\times E$. It follows that $u(x,y)=\rho (x)$ and $v(x,y)=\rho (Tx)$ are positive Borel functions. Their sum $u+v$ is positive Borel; viewed as a map into the subspace $(0,\mathrm{\infty })$, it is measurable. The one-dimensional continuity-algebra result applied to $1$ and the identity on $(0,\mathrm{\infty })$ makes $t\mapsto 1\mathrm{/}t$ continuous there, so its composition with $u+v$ is Borel. Therefore $u\mathrm{/}(u+v)$ and $v\mathrm{/}(u+v)$ are Borel by multiplication, without using a quotient-closure claim. Coordinate maps and permutations are measurable on finite products, The product sigma-algebra and its finite iterates, Arithmetic and lattice operations preserve measurability whenever they are defined, Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function, A continuous map has Borel preimages of Borel sets