LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

Finite-coordinate posterior total-variation limit

Statement

Assume countable choice for the $L^{2}$ prior construction, with the full posterior kernel supplied as in The product-prior posterior factors by coordinates. Fix a finite set $J$ of wavelet coordinates in the product white-noise model of The product-prior posterior factors by coordinates. Suppose $φ$ is bounded and continuous at each normalized truth coefficient $r_{j} = θ_{0, j} / σ_{j}$ , with $φ (r_{j}) > 0$ . Let ${\tilde{Π}}_{n, J}$ be the conditional posterior law of $\sqrt{n} (θ_{J} - X_{J})$ given the full data. If $J = \emptyset$ , both laws are the unique probability on the zero-dimensional one-point space. For nonempty $J$ , the posterior and Gaussian densities $p_{n, J}$ and $ϕ_{J}$ on $R^{∣ J ∣}$ satisfy

$\int_{R^{∣ J ∣}} ∣ p_{n, J} (u ∣ X) - ϕ_{J} (u) ∣ d u ⟶ 0$

in probability under the true white-noise law. Consequently $d_{T V} ({\tilde{Π}}_{n, J}, N_{∣ J ∣} (0, I)) \to 0$ , where $d_{T V} (μ, ν) : = \sup_{A} ∣ μ (A) - ν (A) ∣$ and $N_{∣ J ∣} (0, I)$ is the product of $∣ J ∣$ standard normal laws.

Facts & Assumptions

[F1]

The product-prior posterior factors by coordinates: The posterior marginal on every finite coordinate set is the product of the coordinate Bayes densities.

[F2]

Dominated convergence: Pointwise convergence under an integrable dominating function gives convergence of the integrals.

[F3]

Finite and countable subadditivity of measures: The probability of a countable union of events is at most the sum of their probabilities.

[A1]

The Axiom of Countable Choice ( ${A C}_{ω}$ ): Countable choice is used for the $L^{2}$ prior construction; the full posterior kernel is supplied as model input in [F1], and the finite-dimensional density limit is choice-free.

Given: Countable choice, a fixed finite coordinate set $J$ , the coordinate prior densities and white-noise observations, boundedness of $φ$ , and its continuity and strict positivity at each $r_{j}$ .

Proof

1.1A1F1F2givenalgebra

Fix one coordinate $j = (l, k)$ and write $r = θ_{0, j} / σ_{j}$ . Under the true law, $X_{j} / σ_{j} = r + Z_{j} / (\sqrt{n} σ_{j}) \to r$ in probability, and $b_{n} = (\sqrt{n} σ_{j})^{- 1} \to 0$ . By [F1], under [A1], the posterior density of $U_{n} = \sqrt{n} (θ_{j} - X_{j})$ is $p_{n} (u ∣ X_{j}) = \frac{e^{- u^{2} / 2} φ (X_{j} / σ_{j} + b_{n} u)}{c_{n} (X_{j})}, c_{n} (X_{j}) = \int_{R} e^{- v^{2} / 2} φ (X_{j} / σ_{j} + b_{n} v) d v .$ For any deterministic sequence $x_{n} / σ_{j} \to r$ , boundedness of $φ$ and [F2] give $c_{n} (x_{n}) \to φ (r) \sqrt{2 π} > 0$ .

2.1F2F3step 1.1choosealgebra

Along such a deterministic sequence, $p_{n} (u ∣ x_{n}) \to (2 π)^{- 1 / 2} e^{- u^{2} / 2}$ pointwise and is eventually bounded by a constant multiple of $e^{- u^{2} / 2}$ . A second application of [F2] gives convergence in $L^{1} (d u)$ , hence convergence in total variation. Since $X_{j} / σ_{j} \to r$ in probability, if the total-variation convergence in probability failed, some subsequence would have error probability bounded below. Select a further subsequence for which $P (∣ X_{j} / σ_{j} - r ∣ > 2^{- q}) \leq 2^{- q}$ at its $q$ th term; [F3] bounds each union of tail events by the corresponding geometric tail, which tends to zero, so the further subsequence converges almost surely to $r$ , contradicting the deterministic conclusion.

3.1F1step 2.1algebra∎

For finite nonempty $J$ , [F1] makes the scaled posterior and its Gaussian target product measures. Telescope the difference of their product densities one coordinate at a time. Integrating the absolute value of each term gives the $L^{1}$ distance of that coordinate pair, since every other coordinate density integrates to $1$ . Thus the joint $L^{1}$ distance is at most the sum of the finitely many coordinate $L^{1}$ distances, which tends to zero in probability by step 2.1. For each measurable event $A$ , the absolute difference of its probabilities is at most this $L^{1}$ distance, so the total-variation conclusion follows.

Depends on

Used by

Weak nonparametric Bernstein–von Mises theorem for product priors Theorem

Dependency tree · two levels

29 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

Castillo and Nickl, Nonparametric Bernstein–von Mises theorems in Gaussian white noise, Theorem 7 and discussion, printed p. 2017 (standard reference, not scraped)
Giné and Nickl, Mathematical Foundations of Infinite-Dimensional Statistical Models, Theorem 7.3.18 and proof, printed pp. 593–594 (standard reference, not scraped)
Ray, Adaptive Bernstein–von Mises theorems in Gaussian white noise, §7.1, printed pp. 23–24 (standard reference, not scraped)