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.
Exact posterior second moment and contraction bound for a Gaussian sequence inverse problem
Statement
Assume the Axiom of Choice and the Axiom of Countable Choice. Let , let be the positive singular values in the Gaussian sequence inverse model, and let a fixed truth belong to . Let satisfy , and let the prior be a Borel probability on whose coordinates are independent variables, independent of the observation noise. Under the prior-predictive law the observations are ; under the fixed truth they are , where the are independent variables. Define and . For fixed-truth-almost every data sequence, a posterior version on is the restriction of . Its expected posterior squared distance from the truth is The identity holds in ; under the stated trace condition its right side is finite. For every , the expected posterior mass outside the radius- ball is at most . In particular, if for a constant and a positive , then is a posterior contraction rate in the sense of the preceding definition.
Statement references
Facts & Assumptions
Given: AC and Countable Choice; the positive-noise Gaussian sequence inverse experiment; a fixed truth ; an independent-coordinate Gaussian prior with and ; and prior/noise independence.
The Axiom of Choice states that every family of nonempty sets has a choice function. The Axiom of Choice
Countable Choice supplies a choice function for every countable family of nonempty sets; this is the branch assumed by the compact-SVD coordinate model. The Axiom of Countable Choice ()
The Gaussian sequence inverse model has parameter , product-Borel data , and coordinates with independent standard normal . Multiplying by gives . Gaussian sequence inverse model
In a finite linear Gaussian model with Gaussian prior and positive-definite observation-noise covariance , the posterior law is multivariate normal with mean and covariance . Finite linear Gaussian inverse posterior with singular prior covariance
Under AC, a consistent family of finite Gaussian laws on countably many real coordinates has a unique probability law on the product cylinder sigma-algebra. A mean and positive-semidefinite kernel define a Gaussian process
Independence of random elements is independence of their generated sigma-algebras; the assumed independent prior and noise coordinates give independent coordinate pairs. Independent random elements
Finite measures that agree on a generating -system and on the whole space agree on its generated sigma-algebra. Finite measures agreeing on a generating pi-system and on the whole space are equal
A -system contained in a Dynkin system has its generated sigma-algebra contained in that Dynkin system. Dynkin's pi-lambda theorem
Increasing nonnegative measurable functions satisfy convergence of their integrals to the integral of their pointwise limit. Monotone convergence for the integral
For a nonnegative measurable function and , . Chebyshev-Markov inequality for the integral
A posterior contraction rate is defined by the expected fixed-truth posterior tail condition in the Statement. Posterior contraction rate in a Gaussian sequence inverse experiment
In a jointly multivariate-normal vector, blocks with zero cross-covariance are independent, including when the covariance is singular. Uncorrelated jointly Gaussian blocks are independent
Given: The hypotheses of the Statement.
Proof
Given: The hypotheses of the Statement.
For each fixed coordinate , apply [F2] with one-dimensional prior variance , observation map , and noise variance . Then , and [F2] gives posterior mean and variance .
For every finite coordinate set , the prior/noise pairs indexed by are independent of the pairs outside : independence of the prior element from the noise element and independence within each coordinate family factor the probabilities of finite coordinate rectangles into the product of the pair marginals, and [F5] extends this factorization from the generating rectangles to the corresponding product-Borel events. Each is a measurable function of its pair , so is independent of . For the finite block, put and . [F2] gives posterior covariance and posterior mean with coordinates . Since each , the Gaussian coordinates have zero cross-covariance, and repeated application of [F10] shows they are independent. Thus the finite-block conditional law is the product of the scalar laws from step 1.1. Independence of the complement makes this also the conditional law given the full data: the conditional identity first holds on data rectangles by finite-block conditioning and independence, and [F5] extends it to all product-Borel data events. The product Gaussian law exists on by [F3]. On finite-coordinate cylinders its evaluations are Borel functions of ; the class of Borel sets for which is measurable is a Dynkin system containing the generating cylinder -system, so [F6] makes a probability kernel. The same finite-block conditional identity holds on data cylinders, and [F5] applied successively in the data and parameter coordinates extends it to all product-Borel events. Thus is the prior-predictive conditional law on the product coordinate space.
Put and . This is Borel because each is coordinate-measurable and . The norm-Borel sigma-algebra of equals the trace of the product Borel sigma-algebra: finite-support rational sequences are countable and dense (truncate a square-summable sequence and approximate the retained coordinates), and for and , . Thus every norm ball, and hence every norm-open set, is trace product-Borel; conversely the coordinate maps on normed are continuous. Therefore the restriction of to is measurable on its norm-Borel sets. Since , [F7] gives on , so there. Under the prior-predictive law, ; under the fixed truth, and . Applying [F7] to the partial sums shows has full measure under both laws. Restrict to on and set it equal to outside ; this is a posterior version on and is defined for fixed-truth-almost every observation.
For , the product posterior has coordinate mean and variance , so its expected squared coordinate error is . The partial sums of these nonnegative errors increase to ; [F7] therefore gives , with the value allowed.
Under the fixed truth, . The noise has mean zero and variance one, so its cross term has expectation zero and . The identity gives . Taking expectations in step 4.1 and applying [F7] to the nonnegative partial sums proves the displayed exact series identity.
For each fixed data sequence, apply [F8] to the posterior probability measure with and threshold . This gives posterior tail mass at most times the posterior second moment. Taking fixed-truth expectation and using step 5.1 yields the stated bound. If , substitute to obtain expected tail mass at most for every ; [F9] identifies as a posterior contraction rate.
Remarks
At , the coordinate posterior is and the prior-predictive law of is . The finite check of this one-coordinate case does not test the infinite product or the support argument.
Depends on
- Gaussian sequence inverse model
- Posterior contraction rate in a Gaussian sequence inverse experiment
- The Axiom of Choice
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
- Independent random elements
- A mean and positive-semidefinite kernel define a Gaussian process
- Finite linear Gaussian inverse posterior with singular prior covariance
- Uncorrelated jointly Gaussian blocks are independent
- Dynkin's pi-lambda theorem
- Finite measures agreeing on a generating pi-system and on the whole space are equal
- Monotone convergence for the integral
- Chebyshev-Markov inequality for the integral
Used by
Dependency tree · two levels
65 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
- B. T. Knapik, A. W. van der Vaart, and J. H. van Zanten, Bayesian inverse problems with Gaussian priors, The Annals of Statistics 39 (2011), 2626–2657 (standard reference, not scraped)
- Iain M. Johnstone, Gaussian estimation: Sequence and wavelet models, 2013 draft (standard reference, not scraped)
- Litao Ding and Peter Mathé, Minimax rates for statistical inverse problems under general source conditions (standard reference, not scraped)