Hellinger error bound for posterior potential discretization

Given: A Borel prior concentrated on the forward domain, finite continuous potentials $\mathrm{\Phi },{\mathrm{\Phi }}_N$, a shared lower envelope, a pointwise error envelope $M_2{\psi }_N$, and the weighted integrability condition in the Statement.

Each finite continuous potential has a continuous section; under a common integrable lower envelope on a Borel full-measure forward domain in a separable Banach space, its fixed-data evidence is positive and finite and the normalized update is a probability measure. Continuity of a map of topological spaces at a point and globally, Banach space, Separability: the existence of an at most countable dense subset, The Borel sigma-algebra of a topological space, Probability measures and probability spaces, Function-space posterior propriety from a common lower envelope

For a finite potential $\mathrm{\Phi }$, the fixed-data evidence is $Z={\int }_D{e}^{-\mathrm{\Phi }}d{\mu }_0$ and the posterior density relative to ${\mu }_0$ is $e^{-\mathrm{\Phi }}\mathrm{/}Z$ when $0<Z<\mathrm{\infty }$. A Borel prior concentrated on a forward-map domain, Misfit evidence and the potential posterior law

For supplied densities $p,p_N$ relative to ${\mu }_0$, the library distance is $h(\mathrm{\Pi },{\mathrm{\Pi }}_N)=\mathrm{\parallel }\sqrt{p}-\sqrt{p_N}{\mathrm{\parallel }}_{L^2({\mu }_0)}$, with no factor $1\mathrm{/}\sqrt{2}$. Root-L2 Hellinger distance for dominated laws

Assume the Axiom of Choice only for the optional generic density/TV comparison branch. The Axiom of Choice

Under [A1], for two probability laws with a common sigma-finite dominator, $\mathrm{\parallel }P-Q{\mathrm{\parallel }}_{\mathrm{T}\mathrm{V}}={\sup }_A\mathrm{\mid }P(A)-Q(A)\mathrm{\mid }\le h(P,Q)$ in the library conventions. Hellinger invariance and comparison with library total variation, Total variation distance for probability laws

The derivatives of $t\mapsto e^{-t\mathrm{/}2}$ and $t\mapsto e^{-t}$ are $-\frac{1}{2}{e}^{-t\mathrm{/}2}$ and $-e^{-t}$; the real mean value theorem bounds their increments by derivative magnitude times interval length. The exponential function is smooth and $(\exp {)}^{\mathrm{\prime }}=\exp$, The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g(c)$, then $f\circ g$ is differentiable at $c$ with $(f\circ g{)}^{\mathrm{\prime }}(c)=f^{\mathrm{\prime }}(g(c))g^{\mathrm{\prime }}(c)$, Mean value theorem on a closed real interval

The nonnegative integral is monotone and positively homogeneous. Monotonicity and nonnegative homogeneity of the nonnegative integral

Continuous finite potentials on the Borel subspace $D$ are Borel; via the real-line inclusion they are measurable as extended-real-valued potentials. The norm map and real exponential are continuous, so composing Borel radius envelopes with them gives measurable integrands. A continuous map has Borel preimages of Borel sets, The Borel sigma-algebra of a topological space, The extended real line $\bar{\mathbb{R}}=\mathbb{R}\cup \{-\mathrm{\infty },+\mathrm{\infty }\}$, its order, and the arithmetic that is left undefined, The Borel sigma-algebra on the extended real line, A measurable function between measurable spaces, A norm on a real vector space, the induced metric, and the dictionary with the metric axioms, The reverse triangle inequality $\mathrm{\mid }d(x,z)-d(y,z)\mathrm{\mid }\le d(x,y)$ in any metric space, The exponential function is strictly increasing, Composition with a Borel measurable outer map preserves measurability

Sums, differences, and absolute values of measurable real-valued functions are measurable. Arithmetic and lattice operations preserve measurability whenever they are defined

The nonnegative integral is additive, monotone, and positively homogeneous. Additivity of the nonnegative Lebesgue integral, Monotonicity and nonnegative homogeneity of the nonnegative integral

For square-integrable real functions, the root integral of the square is the $L^2$ norm and satisfies the triangle inequality. The function space ${\mathcal{L}}^p(\mu )$ for $0<p<\mathrm{\infty }$, Minkowski's inequality for integrals, including $p=\mathrm{\infty }$