TheoremStatement: 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.

IID posterior contraction by entropy and prior mass

Statement

Let $(X, A, μ)$ be a sample space with a fixed sigma-finite dominating measure. Let $(Θ, T)$ be a measurable parameter space with prior probability measure $Π$ , and let $p_{θ}$ be finite-valued probability densities relative to $μ$ such that $(θ, x) \mapsto p_{θ} (x)$ is jointly measurable. Let $p_{0}$ be a true density relative to $μ$ , and observe $X_{1}, \dots, X_{n}$ IID from $P_{0}$ , the law with density $p_{0}$ . Assume AC for the imported directional KL convention (The Axiom of Choice). The joint density family is explicit input; no arbitrary-index selection of versions is performed in this theorem.

Choose one metric $d$ for both the entropy and conclusion: the root-L2 Hellinger distance $h$ of Root-L2 Hellinger distance between density laws, the full density distance $d_{1} (p, q) = \int ∣ p - q ∣ d μ$ , or the density distance $d_{2} (p, q) = (\int ∣ p - q ∣^{2} d μ)^{1 / 2}$ . In the $d_{2}$ case assume one finite constant $B$ bounds $p_{0}$ and every density $p_{θ}$ in the model by $B$ $μ$ -almost everywhere. For each $n$ , let $Θ_{n} \in T$ be a nonempty measurable parameter sieve and put $F_{n} : = {p_{θ} : θ \in Θ_{n}}$ . Assume $θ \mapsto d (p_{θ}, p_{0})$ is measurable; this follows from the jointly measurable density family by integration of the relevant nonnegative distance integrands. Let $D (r, F_{n}, d)$ be the packing number defined in Sieve metric entropy produces uniform exponential tests. Suppose $C > 0$ , $ϵ_{n} > 0$ , $ϵ_{n} \to 0$ , $n ϵ_{n}^{2} \to \infty$ , and $\log D (ϵ_{n}, F_{n}, d) \leq n ϵ_{n}^{2}, Π (Θ_{n}^{c}) \leq e^{- (C + 4) n ϵ_{n}^{2}},$ while $Π ⁣ {θ : K L (P_{0} ∥ P_{θ}) \leq ϵ_{n}^{2}, \int {[\log \frac{p_{θ}}{p_{0}}]}^{2} p_{0} d μ \leq ϵ_{n}^{2}} \geq e^{- C n ϵ_{n}^{2}} .$ Here $K L (P_{0} ∥ P_{θ})$ has the directional convention of Kullback–Leibler divergence. In the log-square integral, set the weighted integrand to zero on ${p_{0} = 0}$ ; on ${p_{0} > 0, p_{θ} = 0}$ the log ratio is $- \infty$ and its square is $+ \infty$ , as in KL prior mass gives a posterior denominator lower bound in probability. Define the data-indexed posterior by normalizing $\prod_{i} p_{θ} (X_{i})$ against $Π$ on fibers with finite positive evidence. Then for all sufficiently large fixed $M$ , the posterior contracts outside the $M ϵ_{n}$ -ball in the selected metric: $Π {θ : d (p_{θ}, p_{0}) > M ϵ_{n} ∣ X_{1}, \dots, X_{n}} ⟶ 0$ in $P_{0}^{n}$ -probability.

For $d = d_{1}$ , the radius is in the full density L1 norm; by Hellinger distance is a metric and controls L1 and total variation, $d_{1} = 2 ∥ P - Q ∥_{T V}$ under the library event-supremum convention. The theorem asserts only convergence in probability and gives no automatic almost-sure or minimax-optimality conclusion.

Facts & Assumptions

Given: A sigma-finite dominated IID density model with a jointly measurable density evaluation map, a prior $Π$ , a true finite-valued density $p_{0}$ , measurable parameter sieves $Θ_{n}$ , their density images $F_{n}$ , and the displayed entropy, sieve-tail, and local prior-mass conditions.

[A1]

Assume the Axiom of Choice The Axiom of Choice for the imported directional KL convention Kullback–Leibler divergence. The jointly measurable density family is explicitly supplied, so no arbitrary-index selection of these versions is used.

[F1]

KL prior mass gives a posterior denominator lower bound in probability: the local KL/log-square mass condition gives $D_{n} \geq e^{- (C + 2) n ϵ_{n}^{2}}$ with probability at least $1 - 1 / (n ϵ_{n}^{2})$ .

[F2]

Sieve metric entropy produces uniform exponential tests: under the same metric entropy condition on $F_{n}$ , tests exist with null error at most $2 e^{- (c_{d} M^{2} - 1) n ϵ_{n}^{2}}$ and error at most $e^{- c_{d} M^{2} n ϵ_{n}^{2}}$ for every density in $F_{n}$ outside the $M ϵ_{n}$ -ball.

[F3]

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

[F4]

Expectations factor over finite products of independent random variables: for IID observations, expectations of finite products of nonnegative one-observation functions factor.

[F5]

Markov's inequality for random variables: for a nonnegative random variable $Y$ and $a > 0$ , $P (Y > a) \leq E [Y] / a$ .

[F6]

Arithmetic and lattice operations preserve measurability whenever they are defined and Composition with a Borel measurable outer map preserves measurability: arithmetic operations and Borel functions of jointly measurable density maps preserve product measurability, including absolute values, squares, and square roots.

[F7]

Monotonicity and nonnegative homogeneity of the nonnegative integral and Additivity of the nonnegative Lebesgue integral: the nonnegative integral preserves order, is additive, and is homogeneous under positive finite scalars.

[F8]

Independent random elements have product joint law: a finite IID sample has the product joint law. For the supplied one-observation density $p_{θ}$ , Tonelli and The measure with density $f$ relative to $μ$ show that $\prod_{i} p_{θ} (x_{i})$ defines its product-law density relative to $μ^{n}$ : the two measures agree on measurable rectangles, and Measures agreeing on a generating pi-system are equal under an increasing finite-measure exhaustion from that pi-system identifies them on the product sigma-algebra The product sigma-algebra and its finite iterates.

Proof

1.1A1F1given

On the $P_{0}^{n}$ -full event where $0 < \prod_{i} p_{0} (X_{i}) < \infty$ , set $R_{n} (θ) : = \prod_{i = 1}^{n} p_{θ} (X_{i}) / p_{0} (X_{i})$ and $D_{n} : = \int R_{n} (θ) Π (d θ)$ . By [F1], on an event $Ω_{n}$ with $P_{0}^{n} (Ω_{n}^{c}) \leq 1 / (n ϵ_{n}^{2})$ , the scaled denominator $D_{n}$ is finite and at least $e^{- (C + 2) n ϵ_{n}^{2}}$ . The evidence $\int \prod_{i} p_{θ} (X_{i}) Π (d θ) = D_{n} \prod_{i} p_{0} (X_{i})$ is therefore finite and positive, and on this event the posterior is the quotient of these likelihood integrals.

1.2F2F3F6F7givenchoose

Joint measurability of $p_{θ}$ and the arithmetic/Borel-composition rules [F6] make each nonnegative distance integrand $∣ p_{θ} - p_{0} ∣$ , $∣ p_{θ} - p_{0} ∣^{2}$ , or $(\sqrt{p_{θ}} - \sqrt{p_{0}})^{2}$ product-measurable. Tonelli [F3] therefore gives measurability of $θ \mapsto d (p_{θ}, p_{0})$ . Its values are finite: the Hellinger bound follows from the definition remark, $d_{1} \leq 2$ follows from $∣ p_{θ} - p_{0} ∣ \leq p_{θ} + p_{0}$ and [F7], and in the $d_{2}$ case [F7] and the uniform bound give $d_{2}^{2} \leq \int (p_{θ} + p_{0})^{2} d μ \leq 2 B \int (p_{θ} + p_{0}) d μ = 4 B$ . Thus $A_{n}$ is measurable. Apply [F2] with the selected metric and choose $M$ large enough that $c_{d} M^{2} \geq C + 4$ . The resulting test $ϕ_{n}$ has $P_{0}^{n} (ϕ_{n} = 1) \to 0$ and error at most $e^{- c_{d} M^{2} n ϵ_{n}^{2}}$ for every $θ \in Θ_{n}$ with $d (p_{θ}, p_{0}) > M ϵ_{n}$ .

1.3F2F3F6F8given

Put $A_{n} : = {θ : d (p_{θ}, p_{0}) > M ϵ_{n}}$ , $N_{n} : = \int_{A_{n} \cap Θ_{n}} R_{n} (θ) Π (d θ)$ and $T_{n} : = \int_{A_{n} \cap Θ_{n}^{c}} R_{n} (θ) Π (d θ)$ . The piecewise likelihood ratio is jointly measurable: on the measurable set where $p_{0} > 0$ it is a Borel function of $(p_{θ}, p_{0})$ , and it is zero where $p_{0} = 0$ , by [F6]. Thus the product-density identity [F8], joint measurability, and Tonelli [F3] give $E_{P_{0}^{n}} [(1 - ϕ_{n}) N_{n}] \leq \int_{A_{n} \cap Θ_{n}} P_{θ}^{n} (1 - ϕ_{n}) Π (d θ) \leq e^{- c_{d} M^{2} n ϵ_{n}^{2}} .$ The first inequality allows $P_{θ}$ to put mass outside the support of $P_{0}$ , since the likelihood-ratio integral then contains only the $P_{0}$ -support and is no larger than the full $P_{θ}^{n}$ probability.

1.4F3F4givenalgebra

For every fixed $θ$ , $E_{P_{0}} [p_{θ} (X_{1}) / p_{0} (X_{1})] = \int_{{p_{0} > 0}} p_{θ} d μ \leq 1$ . Independence and [F4] therefore give $E_{P_{0}^{n}} R_{n} (θ) \leq 1$ . Tonelli [F3] and the sieve-tail premise yield $E_{P_{0}^{n}} T_{n} \leq Π (Θ_{n}^{c}) \leq e^{- (C + 4) n ϵ_{n}^{2}} .$

2.1F1F2F3F5step 1.1step 1.2step 1.3step 1.4algebra∎

Fix $δ > 0$ . On $Ω_{n} \cap {ϕ_{n} = 0}$ , posterior mass $Π (A_{n} ∣ X^{n}) > δ$ implies $(1 - ϕ_{n}) (N_{n} + T_{n}) > δ e^{- (C + 2) n ϵ_{n}^{2}}$ . Markov's inequality [F5], step 1.1, and [F2]–[F3] give $P_{0}^{n} {Π (A_{n} ∣ X^{n}) > δ} \leq \frac{1}{n ϵ_{n}^{2}} + 2 e^{- (c_{d} M^{2} - 1) n ϵ_{n}^{2}} + \frac{e^{(C + 2) n ϵ_{n}^{2}}}{δ} (e^{- c_{d} M^{2} n ϵ_{n}^{2}} + e^{- (C + 4) n ϵ_{n}^{2}}) .$ By the choice $c_{d} M^{2} \geq C + 4$ and $n ϵ_{n}^{2} \to \infty$ , the right side tends to zero. Since this holds for every $δ > 0$ , the posterior mass outside the stated ball converges to zero in $P_{0}^{n}$ -probability.

Depends on

Used by

Dependency tree · two levels

97 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, Jayanta K. Ghosh and Aad W. van der Vaart, Convergence rates of posterior distributions, Theorem 2.1 and proof (standard reference, not scraped)
B. J. K. Kleijn, Bayesian Statistics for Frequentists, Theorem 6.4.3 and proof (standard reference, not scraped)
Subhashis Ghosal, The Dirichlet Process, Related Priors and Posterior Asymptotics, §2.5.2 (standard reference, not scraped)