LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generated

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Supremum distance controls local log-Gaussian density distances

Statement

Let $(X, A, ν)$ be a measure space, and let $w, w_{0} : X \to R$ be measurable with finite positive normalizers $Z_{w} = \int e^{w} d ν$ and $Z_{0} = \int e^{w_{0}} d ν$ . Set $p_{w} = e^{w} / Z_{w}$ , $p_{0} = e^{w_{0}} / Z_{0}$ , and $r = ∥ w - w_{0} ∥_{\infty} \leq 1$ . With root-L2 Hellinger distance as in Root-L2 Hellinger distance between density laws, and the directional convention of Kullback–Leibler divergence, $h (P_{w}, P_{0}) \leq e^{r} r, K L (P_{0} ∥ P_{w}) \leq \frac{1}{2} e^{2 r} r^{2}, \int {(\log \frac{p_{w}}{p_{0}})}^{2} p_{0} d ν \leq 4 r^{2} .$

Facts & Assumptions

Given: The stated measurable functions, finite positive normalizers and supremum-distance bound.

[A1]

Assume AC for the imported directional KL convention The Axiom of Choice.

[F1]

Root-L2 Hellinger distance between density laws: $h^{2} (P_{w}, P_{0}) = \int (\sqrt{p_{w}} - \sqrt{p_{0}})^{2} d ν$ .

[F2]

A uniform derivative bound gives a uniform Taylor remainder bound: if a scalar function has derivatives through order two on the closed interval between the two inputs, with the usual endpoint continuity, its first-order Taylor remainder is bounded by half a bound on the absolute second derivative times the squared increment.

[F3]

The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ : for a scalar function continuous on the closed interval between distinct inputs and differentiable on its interior, the increment equals its derivative at an intermediate point times the input increment. By The exponential function is smooth and $(\exp)^{'} = \exp$ , the exponential is $C^{\infty}$ with derivative equal to itself, so it satisfies these hypotheses on every compact interval.

[F4]

The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t: $\log x = \int_{1}^{x} d t / t$ for $x > 0$ ; hence $\log (1 + x) \leq x$ for $x \geq 0$ .

Proof

1.1givenalgebra

Put $g = w - w_{0}$ , $c = \log \int e^{g} p_{0} d ν$ . Since $e^{- r} \leq e^{g} \leq e^{r}$ , we have $∣ c ∣ \leq r$ and $\log (p_{w} / p_{0}) = g - c$ , so $∣ \log (p_{w} / p_{0}) ∣ \leq 2 r$ . Squaring and integrating against the probability density $p_{0}$ proves the log-square bound.

1.2A1F2F3F4givenalgebra

The directional divergence is $K L (P_{0} ∥ P_{w}) = c - \int g p_{0} d ν = \log \int e^{g - \int g p_{0} d ν} p_{0} d ν$ . Let $U = g - \int g p_{0} d ν$ . Then $E_{0} U = 0$ , $∣ U ∣ \leq 2 r$ , and $E_{0} U^{2} \leq E_{0} g^{2} \leq r^{2}$ . Taylor's remainder [F2], applied to $e^{u}$ at zero, gives $e^{U} \leq 1 + U + \frac{1}{2} e^{2 r} U^{2}$ ; hence $E_{0} e^{U} \leq 1 + \frac{1}{2} e^{2 r} r^{2}$ . The integral formula in [F4] gives $\log (1 + x) \leq x$ for $x \geq 0$ , so the KL bound follows.

2.1F1F3step 1.1givenalgebra∎

Write $R = p_{w} / p_{0} = e^{g - c}$ . Then $∣ \sqrt{R} - 1 ∣ = ∣ e^{(g - c) / 2} - 1 ∣ \leq e^{r} ∣ g - c ∣ / 2 \leq e^{r} r$ , by [F3]. Therefore $h^{2} (P_{w}, P_{0}) = E_{0} (\sqrt{R} - 1)^{2} \leq e^{2 r} r^{2}$ , which yields the Hellinger bound.

Source notes

The cited treatments compare Hellinger, directional KL and log-likelihood variance to the supremum norm. The displayed constants here are derived directly under the finite-normalizer hypotheses.

Depends on

Used by

Gaussian-process posterior contraction in density and regression models Theorem

Dependency tree · two levels

53 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

A. W. van der Vaart and J. H. van Zanten, Rates of contraction of posterior distributions based on Gaussian process priors, Lemma 3.1 (standard reference, not scraped)
Bas J. K. Kleijn, Aad W. van der Vaart and Harry van Zanten, Lectures on Nonparametric Bayesian Statistics, Lemma 12.2 (standard reference, not scraped)