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.

Local KL and log-square mass bounds a non-IID posterior denominator

Statement

Assume AC. Let $C \geq 0$ , and for each integer $n \geq 1$ let $ϵ_{n} > 0$ . Let $Y_{1}, \dots, Y_{n}$ be independent, with true densities $p_{i 0}$ and candidate densities $p_{i θ}$ relative to supplied sigma-finite measures $μ_{i}$ . Assume $(θ, y) \mapsto p_{i θ} (y)$ is jointly measurable and let $Π$ be a prior. If a measurable set $K_{n}$ satisfies $Π (K_{n}) \geq e^{- C n ϵ_{n}^{2}}, \sup_{θ \in K_{n}} \frac{1}{n} \sum_{i = 1}^{n} K L (P_{i 0} ∥ P_{i θ}) \leq ϵ_{n}^{2}, \sup_{θ \in K_{n}} \frac{1}{n} \sum_{i = 1}^{n} E_{i 0} ⁣ [{(\log \frac{p_{i θ} (Y_{i})}{p_{i 0} (Y_{i})})}^{2}] \leq ϵ_{n}^{2},$ then the denominator $D_{n} = \int \prod_{i = 1}^{n} \frac{p_{i θ} (Y_{i})}{p_{i 0} (Y_{i})} Π (d θ)$ is finite $P_{0}^{(n)}$ -almost surely and satisfies $P_{0}^{(n)} {D_{n} \geq e^{- (C + 2) n ϵ_{n}^{2}}} \geq 1 - \frac{1}{n ϵ_{n}^{2}} .$

Facts & Assumptions

Given: A jointly measurable dominated independent-observation model, prior $Π$ , the measurable local set $K_{n}$ , and its displayed average directional KL/log-square bounds.

[A1]

Assume AC for Kullback–Leibler divergence and finite-valued density representatives.

[F1]

Independent random elements and Measurable coordinatewise functions preserve independence: measurable functions of distinct independent observations remain independent.

[F2]

Expectations factor over finite products of independent random variables: expectations of nonnegative products of independent functions factor.

[F3]

Jensen's integral inequality for a probability measure: for a probability average, the square of the average is at most the average of the square, and the average of a logarithm is at most the logarithm of the average.

[F4]

Variance of a finite sum as the sum of all variances and covariances: the variance of a sum of independent square-integrable variables is the sum of their variances.

[F5]

Chebyshev's inequality for random variables: if $X$ has finite variance, $\Pr (∣ X - E X ∣ \geq t) \leq Var (X) / t^{2}$ .

[F6]

Tonelli's theorem for nonnegative measurable functions on a sigma-finite product: nonnegative product-measurable functions may be integrated in either order.

Proof

1.1A1F1F2F6given

On the $P_{0}^{(n)}$ -full set where every $p_{i 0} (Y_{i})$ is positive and finite, put $R_{n} (θ) = \prod_{i} p_{i θ} (Y_{i}) / p_{i 0} (Y_{i})$ . For fixed $θ$ , independence [F1]–[F2] gives $E_{0} R_{n} (θ) = \prod_{i} \int_{{p_{i 0} > 0}} p_{i θ} d μ_{i} \leq 1.$ Tonelli [F6] then gives $E_{0} D_{n} \leq 1$ , so $D_{n} < \infty$ almost surely.

1.2A1F1F3F4F6givenalgebra

Let $Π_{K_{n}}$ be $Π$ conditioned on $K_{n}$ and set $Z_{n} = \int_{K_{n}} \sum_{i} \log \frac{p_{i θ} (Y_{i})}{p_{i 0} (Y_{i})} Π_{K_{n}} (d θ) .$ Tonelli [F6] applied to the log-ratio squares gives integrability over the conditional prior and sample space; the inequality $∣ u ∣ \leq 1 + u^{2}$ also makes the log ratios jointly integrable. Thus their conditional-prior integrals have measurable finite versions almost surely, and Jensen [F3] makes them square-integrable. Directional KL gives $E_{0} Z_{n} \geq - n ϵ_{n}^{2}$ . Writing $Z_{n} = \sum_{i} V_{i} (Y_{i})$ , independence [F1] and [F4] give ${Var}_{0} Z_{n} \leq \sum_{i} E_{0} V_{i} (Y_{i})^{2}$ . Jensen [F3] applied to the conditional prior integral yields $E_{0} V_{i} (Y_{i})^{2} \leq \int_{K_{n}} E_{i 0} ⁣ [{(\log \frac{p_{i θ} (Y_{i})}{p_{i 0} (Y_{i})})}^{2}] Π_{K_{n}} (d θ),$ so ${Var}_{0} Z_{n} \leq n ϵ_{n}^{2}$ .

2.1F3F5step 1.1step 1.2givenalgebra∎

Chebyshev [F5] implies $P_{0}^{(n)} {Z_{n} < - 2 n ϵ_{n}^{2}} \leq 1 / (n ϵ_{n}^{2})$ , since $E_{0} Z_{n} \geq - n ϵ_{n}^{2}$ and ${Var}_{0} Z_{n} \leq n ϵ_{n}^{2}$ . Jensen for $\log$ gives $D_{n} \geq \int_{K_{n}} R_{n} (θ) Π (d θ) \geq Π (K_{n}) \exp (Z_{n}) .$ On the complementary event, this is at least $e^{- (C + 2) n ϵ_{n}^{2}}$ . Together with step 1.1 this proves the claim.

Depends on

Used by

Gaussian-process posterior contraction in density and regression models Theorem

Dependency tree · two levels

64 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

Subhashis Ghosal and Aad W. van der Vaart, Convergence rates of posterior distributions for noniid observations, §3, Theorem 4 (standard reference, not scraped)
A. W. van der Vaart and J. H. van Zanten, Rates of contraction of posterior distributions based on Gaussian process priors, §3.3 (standard reference, not scraped)