Hamiltonian Monte Carlo and leapfrog correction

Given: Countable Choice, $d$, $U$, $M$, the stated complete Hamiltonian vector field, and, for the sufficient condition, a global Lipschitz constant $L$ for $\mathrm{\nabla }U$.

Countable Choice is the set-theoretic assumption used by the C1 change-of-variables theorem. The Axiom of Countable Choice (${\mathrm{A}\mathrm{C}}_{\omega }$)

A $C^1$ Euclidean vector field has a unique maximal flow that is jointly $C^1$; its time slices have inverse given by the negative-time flow, and its derivative in initial data solves the variational equation. C¹ Euclidean maximal flows, variational dependence and the finite C² upgrade

The total-derivative chain rule gives $\frac{d}{dt}H(z(t))=DH(z(t))z^{\mathrm{\prime }}(t)$ and differentiates compositions by $D(g\circ f)=Dg(f)Df$. The chain rule for total derivatives: $D(g\circ f)(a)=Dg(f(a))\circ Df(a)$

For an invertible differentiable matrix curve $A(t)$, Jacobi's formula is $(\det A{)}^{\mathrm{\prime }}=\det (A)\mathrm{tr}(A^{-1}{A}^{\mathrm{\prime }})$. The determinant differential is $D\det (A)[H]=\mathrm{tr}(\mathrm{adj}(A)H)$ at every matrix, and Jacobi's formula holds on the invertible locus

A continuous vector field on $\mathbb{R}\times {\mathbb{R}}^n$ with one global state-Lipschitz constant has a unique global solution for every initial condition. A globally state-Lipschitz vector field on $\mathbb{R}\times {\mathbb{R}}^n$ has global solutions

Two solutions for a state-Lipschitz field with constant $C$ obey $\mathrm{\parallel }x(t)-y(t){\mathrm{\parallel }}_2\le e^{C\mathrm{\mid }t-t_0\mathrm{\mid }}\mathrm{\parallel }x(t_0)-y(t_0){\mathrm{\parallel }}_2$. The Grönwall estimate for two solutions of a Lipschitz ODE

For a real matrix $A$, $\mathrm{\parallel }Ax{\mathrm{\parallel }}_2\le \mathrm{\parallel }A{\mathrm{\parallel }}_F\mathrm{\parallel }x{\mathrm{\parallel }}_2$. Cauchy-Schwarz $\mid ⟨x,y⟩\mid \le \parallel x{\parallel }_2\parallel y{\parallel }_2$ with its equality case, the triangle inequality for $\parallel \cdot {\parallel }_2$, the parallelogram law and polarisation

SPD $M$ has a Cholesky factor $M=L{L}^T$ with positive diagonal (Hermitian positive-definite matrices and Cholesky factorisation A = LL* with positive diagonal, A matrix admits a Cholesky factorisation with positive diagonal exactly when it is Hermitian positive definite, and that factor is unique); triangular determinants multiply the diagonal entries, determinants are multiplicative, and a real square matrix with nonzero determinant is invertible (The determinant of a triangular matrix is the product of its diagonal entries, For same-sized finite square matrices over a commutative ring, $\det (AB)=\det (A)\det (B)$, A finite square real matrix is invertible if and only if its determinant is nonzero).

Under Countable Choice, a $C^1$ diffeomorphism between open Euclidean sets satisfies the change-of-variables formula for every nonnegative Lebesgue-measurable function. A C^1 diffeomorphism satisfies the change-of-variables formula for nonnegative Lebesgue measurable functions

The Euclidean gradient is the transpose-Jacobian convention, so $U\in C^2$ makes $F$ a $C^1$ field with $DF(q,p)=\left(\begin{array}{cc}0& M^{-1}\\ -{\mathrm{\nabla }}^{2}U(q)& 0\end{array}\right)$. The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case

Given: Countable Choice, the natural numbers $\mathbb{N}$, and the function $f(x)=\exp (-\mathrm{\mid }x\mathrm{\mid })$.

Countable Choice is the set-theoretic assumption used by the continuous-to-Borel and box-measure results. The Axiom of Countable Choice (${\mathrm{A}\mathrm{C}}_{\omega }$)

The exponential is continuous, positive and strictly increasing, and satisfies $\exp (-x)=1\mathrm{/}\exp (x)$ for every real $x$. Continuous real functions on $\mathbb{R}$ are Borel measurable under Countable Choice. The exponential is positive and satisfies $\exp (-x)=1\mathrm{/}\exp (x)$, The exponential function is strictly increasing, Continuous functions on Euclidean spaces are Borel measurable

Every half-open interval $[a,b)$ is Lebesgue measurable with measure $b-a$. A box in ${\mathbb{R}}^n$ with parameters $a_i\le b_i$ is Lebesgue measurable of measure ${\prod }_{i<n}(b_i-a_i)$, whichever of its faces are included

The nonnegative Lebesgue integral is monotone, additive on nonnegative measurable functions, and satisfies monotone convergence. Monotonicity and nonnegative homogeneity of the nonnegative integral, Additivity of the nonnegative Lebesgue integral, Monotone convergence for the integral

If $0<r<1$, then ${\sum }_{k=0}^{\mathrm{\infty }}{r}^k=1\mathrm{/}(1-r)<\mathrm{\infty }$. For $\mathrm{\mid }r\mathrm{\mid }<1$, ${\sum }_{k\ge 0}{r}^k=1\mathrm{/}(1-r)$, and for $\mathrm{\mid }r\mathrm{\mid }\ge 1$ the series diverges

Arithmetic combinations of measurable real functions are measurable. Arithmetic and lattice operations preserve measurability whenever they are defined

The exponential addition formula, induction, and recursive integer-power definition give $\exp (-k)=\exp (-1{)}^k$ for every natural $k$. The exponential addition formula $\exp (x+y)=\exp (x)\exp (y)$, The principle of mathematical induction, Integer powers $a^m$

The nonnegative Lebesgue integral of a nonnegative measurable function is the supremum of the integrals of its nonnegative simple minorants. The nonnegative Lebesgue integral

The natural numbers $\mathbb{N}$ start at $0$ and are closed under successor. The natural numbers $\mathbb{N}$ (von Neumann)

A natural index used as a real endpoint is read through its canonical embedding into $\mathbb{R}$. The canonical natural $\iota (n)=n\cdot 1_F$ of a field

For a nonnegative measurable function and a measurable set $E$, ${\int }_{E}fd\lambda$ means $\int f{\mathbf{1}}_{E}d\lambda$. Integral over a measurable subset

Under Countable Choice, every Borel subset of $\mathbb{R}$ is Lebesgue measurable. Assuming countable choice, every Borel subset of ${\mathbb{R}}^n$ is Lebesgue measurable

The canonical naturals are cofinal in $\mathbb{R}$. Every complete ordered field is Archimedean

A nonnegative simple function has the same nonnegative Lebesgue and simple integrals; in particular, $\int c{\mathbf{1}}_{E}d{\lambda }_1=c{\lambda }_1(E)$ for $c\ge 0$ and measurable $E$ of finite measure. The integral of a nonnegative simple function, The nonnegative integral agrees with the simple integral on simple functions

Given: The inputs and maps in One-step leapfrog map as force and drift shears, finite $L\ge 1$, and Countable Choice for the stated Lebesgue-measure supplier.

Countable Choice supplies the measure construction used by the cited reflection result. The Axiom of Countable Choice (${\mathrm{A}\mathrm{C}}_{\omega }$)

For $U\in C^1$, the kick and drift have the formulas in One-step leapfrog map as force and drift shears; $\mathrm{\nabla }U$ is continuous, and their inverses are $K_{-a}$ and $D_{-b}$.

Translating a Lebesgue-measurable set preserves its Lebesgue measure. Lebesgue outer measure, Lebesgue measurability and Lebesgue measure are unchanged by translation

Sections of product-measurable sets are measurable; a continuous map pulls Borel sets back to Borel sets. Every section of a product-measurable function is measurable, A continuous map has Borel preimages of Borel sets

Under Countable Choice, Lebesgue measure is sigma-finite: the increasing finite boxes $(-n,n{]}^d$ cover ${\mathbb{R}}^d$, and Borel sets are Lebesgue measurable. A box in ${\mathbb{R}}^n$ with parameters $a_i\le b_i$ is Lebesgue measurable of measure ${\prod }_{i<n}(b_i-a_i)$, whichever of its faces are included, Assuming countable choice, every Borel subset of ${\mathbb{R}}^n$ is Lebesgue measurable

The product of sigma-finite Lebesgue measures exists with the rectangle formula, and Tonelli applies to nonnegative product-measurable functions. 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

Reflection $p\mapsto -p$ preserves Lebesgue measure on ${\mathbb{R}}^d$ under Countable Choice. For a nonzero real $c$, dilation by $c$ multiplies Lebesgue outer measure by $\mathrm{\mid }c{\mathrm{\mid }}^n$, and reflection in the origin preserves it

The determinant of a triangular matrix is the product of its diagonal entries. The determinant of a triangular matrix is the product of its diagonal entries

Under Countable Choice, the Borel sigma-algebra of ${\mathbb{R}}^{2d}$ is the product of the Borel sigma-algebras of the two factors, and the product of their Borel-restricted Lebesgue measures agrees with full Euclidean measure ${\lambda }_{2d}$. The Borel product of R^m and R^n is the Borel sigma-algebra of R^{m+n}, On Borel subsets of R^{m+n}, the product lambda_m times lambda_n agrees with lambda_{m+n}

Under Countable Choice, every Lebesgue-measurable subset of ${\mathbb{R}}^{2d}$ differs from a Borel set by a subset of a Borel null set, and ${\lambda }_{2d}$ is the completion of its Borel restriction. $\mathcal{L}({\mathbb{R}}^n)$ is exactly the completion of the restriction of ${\lambda }_n$ to the Borel sets

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