LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge 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.

Gaussian normal-prior posterior

Statement

Assume AC. Let $d \geq 1$ , $σ > 0$ , and $n \geq 1$ . Let $Θ \sim N_{d} (0, I_{d})$ , and, conditional on $Θ$ , let $Z_{1}, \dots, Z_{n}$ be independent with law $N_{d} (Θ, σ^{2} I_{d})$ . Let $Y_{1}, \dots, Y_{n}$ be independent uniform signs, independent of $(Θ, Z_{1}, \dots, Z_{n})$ . Put $\overset{ˉ}{Z} = n^{- 1} \sum_{i = 1}^{n} Z_{i}$ . The conditional law of $Θ$ given $(Z_{1}, \dots, Z_{n}, Y_{1}, \dots, Y_{n})$ is $N_{d} ⁣ (\frac{n}{σ^{2} + n} \overset{ˉ}{Z}, \frac{σ^{2}}{σ^{2} + n} I_{d}) .$ For $n = 0$ , with no observations, the conditional law is the prior $N_{d} (0, I_{d})$ .

Statement references

Multivariate normal law, including singular covariance: the finite-dimensional Gaussian laws and their singular-covariance convention.

A positive-definite multivariate normal law has its Gaussian density: the Lebesgue density formula for each positive-definite Gaussian law used here.

Schmidt et al., Appendix A.2, proof of Theorem 11, PDF pp. 27–29.

Facts & Assumptions

Given: Assume AC and the Gaussian prior, conditionally independent observations, and independent labels in the Statement.

[A1]

AC supplies the finite-dimensional multivariate-normal law construction and its positive-definite density formula. The Axiom of Choice, Multivariate normal law, including singular covariance, A positive-definite multivariate normal law has its Gaussian density.

[F1]

Independent random elements have the finite product joint law. Independent random elements, Independent random elements have product joint law.

[F2]

A positive-definite $N_{d} (m, Σ)$ law has density proportional to $\det (Σ)^{- 1 / 2} \exp (- \frac{1}{2} (x - m)^{T} Σ^{- 1} (x - m))$ . A positive-definite multivariate normal law has its Gaussian density.

[F3]

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

Proof

1.1A1F1F2algebra

For $n \geq 1$ , the joint density of $(Θ, Z_{1}, \dots, Z_{n})$ is proportional to $\exp ⁣ (- \frac{1}{2} ∥ θ ∥_{2}^{2} - \frac{1}{2 σ^{2}} \sum_{i = 1}^{n} ∥ z_{i} - θ ∥_{2}^{2})$ . Indeed, the prior density and each conditional Gaussian density are given by [F2], and their product is the joint density by conditional independence and [F1]. The independent labels contribute a constant factor $2^{- n}$ , so conditioning on their observed values does not change the $θ$ -dependent factor.

2.1step 1.1F2algebra

Write $\overset{ˉ}{z} = n^{- 1} \sum_{i} z_{i}$ . Expanding squares gives $\sum_{i} ∥ z_{i} - θ ∥_{2}^{2} = \sum_{i} ∥ z_{i} - \overset{ˉ}{z} ∥_{2}^{2} + n ∥ θ - \overset{ˉ}{z} ∥_{2}^{2}$ . Completing the remaining square in $θ$ yields $∥ θ ∥_{2}^{2} + \frac{n}{σ^{2}} ∥ θ - \overset{ˉ}{z} ∥_{2}^{2} = \frac{σ^{2} + n}{σ^{2}} {∥ θ - \frac{n}{σ^{2} + n} \overset{ˉ}{z} ∥}_{2}^{2} + \frac{n}{σ^{2} + n} ∥ \overset{ˉ}{z} ∥_{2}^{2}$ . The final term is independent of $θ$ . The normalized conditional density is therefore the Gaussian density in the Statement, with positive covariance $\frac{σ^{2}}{σ^{2} + n} I_{d}$ .

3.1step 2.1F1F2F3

The density ratio in step 2.1 defines a measurable probability kernel in the observed vectors because its mean is linear in $\overset{ˉ}{z}$ and its covariance is fixed; [F2] gives unit mass. Applying [F3] to the nonnegative joint density verifies the conditional-law identity on every pair of Borel sets. Since the labels are independent of $(Θ, Z_{1}, \dots, Z_{n})$ , the same kernel is the conditional law after adjoining the labels.

4.1givenF1∎

When $n = 0$ , the observed sigma-algebra contains no data, so conditioning leaves the prior law unchanged; the labels, if supplied, are independent of $Θ$ .

References

The Axiom of Choice: AC is used by the Gaussian construction and density supplier.

Independent random elements have product joint law: finite independent samples have product joint law.

Tonelli's theorem for nonnegative measurable functions on a sigma-finite product: justifies the density integrations defining the conditional kernel.

Depends on

Used by

Robust sample lower bound in the Gaussian model Theorem

Dependency tree · two levels

46 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

Ludwig Schmidt, Shibani Santurkar, Dimitris Tsipras, Kunal Talwar, and Aleksander Madry, Adversarially Robust Generalization Requires More Data, arXiv:1804.11285v2, Appendix A.2, proof of Theorem 11 (standard reference, not scraped)