Pipeline-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.

✓ 1 result · all verified · 1 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full by a delegated reviewing agent on the owner's instruction; the judge is an additional, independent cross-model AI review of the proofs; all 1 also cleared it.

Learned reconstruction targets and risk

1 · Prerequisites

2 · Logical flowchart

3 · Definitions, theorems and proofs

PropositionStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)verified 2026-10-22 (gpt-6.1-sol)Open item page →

The posterior mean is the unique squared-loss Bayes action in a Hilbert target

Statement

Assume the Axiom of Choice. Let $(Y, Y)$ be a measurable data space, let $H$ be a separable real Hilbert space, and fix a complete orthonormal basis $(e_{j})_{j \in J}$ , where $J$ is either finite with its supplied ordering or $J = N$ . A complex Hilbert signal space is included by viewing it as a real Hilbert space with inner product the real part of its complex inner product and supplying a real orthonormal basis. Let $Π$ be a probability kernel from $Y$ to $H$ with its norm Borel sigma-algebra. Define $D_{2} : = {y \in Y : \int_{H} ∥ h ∥_{H}^{2} Π_{y} (d h) < \infty} .$ For every $y \in D_{2}$ and $j \in J$ , define $m_{j} (y) : = \int_{H} ⟨ h, e_{j} ⟩_{H} Π_{y} (d h), μ (y) : = \sum_{j \in J} m_{j} (y) e_{j},$ where the last sum is the norm limit of its finite partial sums. Then $D_{2} \in Y$ , the sum defining $μ (y)$ exists for every $y \in D_{2}$ , and $μ : D_{2} \to H$ is measurable. For every $y \in D_{2}$ and every action $a \in H$ , $\int_{H} ∥ h - a ∥_{H}^{2} Π_{y} (d h) = \int_{H} ∥ h - μ (y) ∥_{H}^{2} Π_{y} (d h) + ∥ a - μ (y) ∥_{H}^{2} .$ Thus $μ (y)$ is the unique finite-risk action minimizing posterior squared-error risk over all of $H$ , and it is a measurable Bayes action rule on $D_{2}$ . The minimization is over the full Hilbert space: the mean need not belong to a nonconvex admissible signal subset, and no perceptual-representativeness claim is made. For a probability space $(Ω, F, P)$ , let $Y : Ω \to (Y, Y)$ and $T : Ω \to H$ be measurable random elements with $E ∥ T ∥_{H}^{2} < \infty$ . If the same $Π$ is a supplied regular conditional law of $T$ given $Y$ , write $P_{Y} (B) = P (Y \in B)$ for the law of $Y$ . Then $D_{2}$ has full $P_{Y}$ -measure. Extend $μ$ by zero to a measurable map $\overset{ˉ}{μ} : Y \to H$ ; the coordinates of $\overset{ˉ}{μ} (Y)$ are versions of $E [⟨ T, e_{j} ⟩_{H} ∣ σ (Y)]$ , and $\overset{ˉ}{μ} (Y)$ is square-integrable. Any square-integrable $H$ -valued random variable whose basis coordinates are versions of those same conditional expectations equals $\overset{ˉ}{μ} (Y)$ almost surely. The RCD's values on $P_{Y}$ -null data sets remain version choices.

For this measurability assertion, equip $D_{2}$ with the trace sigma-algebra $Y ∣_{D_{2}} : = {A \cap D_{2} : A \in Y}$ inherited from $(Y, Y)$ .

Statement references

A measurable data space is a set with a specified sigma-algebra.

A probability kernel has measurable evaluations and probability-measure sections.

Kernel integrands are measurable on the product sigma-algebra.

A real Hilbert space is complete for its inner-product norm.

Separability supplies a countable dense subset.

The inner product induces the Hilbert norm and scalar coordinate functionals.

Cauchy–Schwarz bounds each fixed basis-coordinate functional by the Hilbert norm, giving its continuity.

A Hilbert basis is a complete orthonormal family.

Under Countable Choice, basis coordinates satisfy Parseval's identity.

Under AC, scalar conditional expectation is the unique L2 projection.

A measurable rule with finite posterior risk attaining the minimum is a Bayes action rule.

A conditional law is a probability kernel, and changes on marginal-null data sets preserve its conditional identities.

Kernel integrals of scalar tests give conditional-expectation versions.

Scalar conditional-expectation versions agree almost surely.

Martin, §5.3.1, complete lecture notes

Daras et al., Lemma A.1, full diffusion survey

Dashti and Stuart, §3.2 and §4.1, full lecture notes

Facts & Assumptions

Given: AC; a measurable data space; a separable real Hilbert target $H$ with a supplied finite or countable complete orthonormal basis; and a supplied probability kernel $Π_{y}$ on $H$ . The theorem is applied on the data domain $D_{2}$ of finite posterior second moment.

[A1]

The Axiom of Choice gives a choice function for every family of nonempty sets. The Axiom of Choice

[A2]

Countable Choice is the restriction of AC to countable families; it is assumed by the Parseval supplier below. The Axiom of Countable Choice ( ${A C}_{ω}$ )

[F1]

A probability kernel has a measurable evaluation for every Borel target set and a probability measure at every data point. Measure kernel and probability kernel

[F2]

The product sigma-algebra makes the continuous norm and coordinate functions into product-measurable kernel integrands. The product sigma-algebra and its finite iterates, Real and complex inner-product spaces and their induced length, Cauchy–Schwarz: $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥ ∥ y ∥$ , with equality exactly for dependent pairs

[F3]

Separability supplies an at-most-countable dense subset of $H$ . Separability: the existence of an at most countable dense subset

[F4]

A real Hilbert space is complete for its inner-product norm, and a Hilbert basis is a complete orthonormal family. Hilbert space, Orthonormal families, complete orthonormal systems and Hilbert bases

[F5]

For a complete orthonormal family, Parseval's identity equates the squared norm with the sum of squared coordinates; this supplier assumes Countable Choice. Parseval equivalences for an orthonormal family

[F6]

A scalar conditional-expectation version is integrable, measurable with respect to its conditioning sigma-algebra, and satisfies the conditioning-event integral identities. Conditional expectation given a sigma algebra

[F7]

Under AC, a scalar conditional expectation of an $L^{2}$ input is its orthogonal projection onto $L^{2} (G)$ ; in particular its residual is orthogonal to constant random variables. Conditional expectation is the l2 orthogonal projection

[F8]

Integrating a product-measurable nonnegative function against a probability kernel gives a measurable function; signed integrals are measurable on their absolute-integrability domain. Measurability of integration against a kernel

[F9]

Increasing nonnegative measurable functions pass through their integrals by monotone convergence. Monotone convergence for the integral

[F10]

A measurable action rule with finite posterior risk attaining the pointwise minimum is a Bayes action rule. Finite posterior risk and Bayes action rule

[F11]

A conditional law is a probability kernel indexed by the conditioning random element; changing its values on a marginal-null set preserves the conditional identities. Conditional law given a random element

[F12]

Integrals of measurable nonnegative or integrable scalar tests against an RCD are conditional-expectation versions. Conditional integration through a regular conditional law

[F13]

Two integrable scalar versions of the same conditional expectation agree almost surely. Conditional expectation is unique almost surely

[F14]

A product of two at-most-countable sets is at most countable. A product of two at most countable sets is at most countable

[F15]

Cauchy–Schwarz gives $∣ ⟨ x, e_{j} ⟩_{H} ∣ \leq ∥ x ∥_{H}$ for each unit basis vector $e_{j}$ , so each coordinate functional is continuous; it also gives continuity of the inner product in either argument. Cauchy–Schwarz: $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥ ∥ y ∥$ , with equality exactly for dependent pairs

[F16]

A measurable space $(Y, Y)$ has a sigma-algebra $Y$ of measurable subsets. Measurable spaces and measurable sets

Proof

1.1F1F2F4F8F15F16givenalgebra

The function $(y, h) \mapsto ∥ h ∥_{H}^{2}$ is product-measurable because the norm is continuous, so kernel integration [F8] makes $s_{2} (y) = \int_{H} ∥ h ∥_{H}^{2} Π_{y} (d h)$ measurable and $D_{2} = {s_{2} < \infty}$ measurable. For each $j$ , $X_{j} (h) = ⟨ h, e_{j} ⟩_{H}$ is continuous by [F15] and $∥ e_{j} ∥_{H} = 1$ . The decomposition $h = X_{j} (h) e_{j} + (h - X_{j} (h) e_{j})$ is orthogonal, so $X_{j} (h)^{2} \leq ∥ h ∥_{H}^{2}$ ; hence $2 ∣ X_{j} (h) ∣ \leq 1 + ∥ h ∥_{H}^{2}$ . Thus each signed coordinate integral defining $m_{j} (y)$ is finite on $D_{2}$ , and the signed-kernel clause of [F8] makes $m_{j}$ measurable there.

2.1A1A2F1F4F5F6F7F9F15step 1.1construct

Fix $y \in D_{2}$ . Under the probability space $(H, B (H), Π_{y})$ , each $X_{j}$ is square-integrable. The constant $m_{j} (y) = \int X_{j} d Π_{y}$ satisfies the conditional-expectation identities for the trivial sigma-algebra by [F6], so [F7] makes it the projection of $X_{j}$ onto constants and gives $\int_{H} (X_{j} - m_{j} (y)) d Π_{y} = 0$ . For every real $b$ , expand $X_{j} - b = (X_{j} - m_{j} (y)) + (m_{j} (y) - b)$ ; the cross term integrates to zero, yielding $\int_{H} (X_{j} - b)^{2} d Π_{y} = \int_{H} (X_{j} - m_{j} (y))^{2} d Π_{y} + (b - m_{j} (y))^{2}$ . Taking $b = 0$ gives $m_{j} (y)^{2} \leq \int_{H} X_{j}^{2} d Π_{y}$ . Let $J_{N}$ be the first $N$ basis indices, taking all indices once $N$ reaches the finite endpoint when $J$ is finite. Summing over $J_{N}$ and applying Parseval [F5] pointwise, followed by monotone convergence [F9], yields $\sum_{j \in J} m_{j} (y)^{2} \leq \int_{H} \sum_{j \in J} X_{j} (h)^{2} Π_{y} (d h) = \int_{H} ∥ h ∥_{H}^{2} Π_{y} (d h) < \infty$ . Orthonormality gives $∥ \sum_{j \in J_{N}} m_{j} (y) e_{j} ∥_{H}^{2} = \sum_{j \in J_{N}} m_{j} (y)^{2}$ ; for $M > N$ , the squared norm of the difference of the two partial sums is $\sum_{j \in J_{M} ∖ J_{N}} m_{j} (y)^{2}$ , which tends to zero as $M, N \to \infty$ because the series converges. Thus the partial sums are Cauchy, and completeness [F4] gives their norm limit $μ (y)$ . Since the sum in the statement is over those same initial segments, it is this norm limit. By continuity of the inner product [F15], $⟨ μ (y), e_{j} ⟩_{H} = m_{j} (y)$ for every $j$ .

3.1F3F5F14step 1.1step 2.1construct

Let $C$ be a countable dense subset of $H$ from [F3]. The balls with centers in $C$ and radii $1 / n$ form a countable base by [F14]: for any point in an open set, choose $n$ with $3 / (2 n)$ smaller than the radius of a ball about that point contained in the open set, then choose a center in $C$ within $1 / (2 n)$ of the point. The resulting radius- $1 / n$ ball contains the point and lies in the open set. For $c \in C$ and a basis ball radius $r = 1 / n$ , the finite sums $s_{N} (y) = \sum_{j \in J_{N}} (m_{j} (y) - ⟨ c, e_{j} ⟩_{H})^{2}$ are measurable by step 1.1. By Parseval [F5] and step 2.1, $∥ μ (y) - c ∥_{H}^{2} = \sup_{N} s_{N} (y)$ , where finite bases use the full sum once all coordinates are included. The preimage of the open ball is the countable union $⋃_{k \geq 2} ⋂_{N} {s_{N} < r^{2} (1 - 1 / k)}$ ; this equals ${\sup_{N} s_{N} < r^{2}}$ . Hence every basis-ball preimage is measurable, and the countable base makes $μ$ measurable on $D_{2}$ .

4.1F4F5F9F10step 2.1step 3.1algebra

Fix $y \in D_{2}$ and $a \in H$ . Write $a_{j} = ⟨ a, e_{j} ⟩_{H}$ . Applying the scalar identity established in step 2.1 with $b = a_{j}$ gives $\int_{H} (X_{j} - a_{j})^{2} d Π_{y} = \int_{H} (X_{j} - m_{j} (y))^{2} d Π_{y} + (a_{j} - m_{j} (y))^{2}$ . Sum over the initial segments $J_{N}$ from step 2.1 and pass to their increasing limits with [F9]; Parseval [F5] identifies the three sums as $\int_{H} ∥ h - a ∥_{H}^{2} d Π_{y}$ , $\int_{H} ∥ h - μ (y) ∥_{H}^{2} d Π_{y}$ , and $∥ a - μ (y) ∥_{H}^{2}$ , respectively. The first integral is finite because $∥ h - a ∥_{H}^{2} \leq 2 ∥ h ∥_{H}^{2} + 2 ∥ a ∥_{H}^{2}$ ; the same bound with $μ (y)$ gives finite risk at the mean. The resulting identity proves that only $a = μ (y)$ attains the minimum. By [F10] and step 3.1, $μ$ is a measurable Bayes action rule on $D_{2}$ .

5.1F4F11F12F13F15F16step 1.1step 3.1step 4.1construct∎

Now suppose $Π$ is a supplied RCD of the measurable random element $T : Ω \to H$ given $Y : Ω \to Y$ , with $E ∥ T ∥_{H}^{2} < \infty$ . Applying [F12] to $h \mapsto ∥ h ∥_{H}^{2}$ shows that $s_{2} (Y)$ has finite expectation $E ∥ T ∥_{H}^{2}$ ; a nonnegative random variable with finite expectation is finite almost surely, so $P_{Y} (D_{2}) = 1$ . By [F15], $∣ ⟨ T, e_{j} ⟩_{H} ∣ \leq ∥ T ∥_{H}$ , and $2 ∥ T ∥_{H} \leq 1 + ∥ T ∥_{H}^{2}$ , so every coordinate is integrable. For every $j$ , [F12] now identifies $m_{j} (Y)$ as a version of $E [⟨ T, e_{j} ⟩_{H} ∣ σ (Y)]$ . Extend $μ$ by zero outside $D_{2}$ ; because $D_{2}$ is measurable by step 1.1 and $μ$ is measurable on $D_{2}$ by step 3.1, this piecewise extension is measurable, and step 4.1 at $a = 0$ gives $∥ μ (y) ∥_{H}^{2} \leq s_{2} (y)$ on $D_{2}$ , so the extension evaluated at $Y$ is square-integrable. If another square-integrable $H$ -valued random variable has each basis coordinate as a version of the corresponding scalar conditional expectation, [F13] makes each coordinate equal to $m_{j} (Y)$ outside a null set. There are at most countably many coordinates, so the union of these exceptional null sets is null; completeness of the basis [F4] then makes the two vectors equal there. The RCD's values on $P_{Y}$ -null data sets remain version choices by [F11].

DefinitionDefinition: AI-adaptedProof: Not applicableverified 2026-10-22 (gpt-6.1-sol)Open item page →

Learned inverse estimators and reconstruction targets

Definition

Let $(X, d_{X})$ and $(Y, d_{Y})$ be metric parameter and data spaces, let $U \subseteq X$ be a nonempty admissible truth class, let $F : U \to Y$ be a forward map, and let $(Q, d_{Q})$ be a metric target space. All metric spaces in this definition carry their Borel sigma-algebras. Give $U$ the subspace Borel sigma-algebra $B (U) : = {U \cap A : A \in B (X)}$ , and assume that $q : U \to Q$ is measurable from $(U, B (U))$ to $(Q, B (Q))$ . The target $q (x)$ is the recovery object assigned to truth $x$ ; $Q$ may be the parameter space itself or a quotient solution-class space. A point reconstruction rule is a Borel map $g : Y \to Q$ , and its output at data $y$ is $g (y)$ . A learned point estimator is such a map ${\hat{q}}_{ϕ}$ with a fitted parameter $ϕ$ in a specified parameter set. A complete training description names the probability law $P_{f i t}$ of all variables used to fit $ϕ$ ; those variables may be paired or unpaired. A complete test description names a probability law $P_{t e s t}$ for evaluation pairs $(Y, q (X))$ . No equality between fitting and test laws is assumed.

A finite unrolled learned update consists of an integer $K \geq 1$ , a Borel initialization $u_{0} : Y \to Q$ , and maps $T_{ϕ, k} : Q \times Y \to Q$ measurable from $(Q \times Y, B (Q) \otimes B (Y))$ to $(Q, B (Q))$ for $0 \leq k < K$ , with $u_{k + 1} (y) = T_{ϕ, k} (u_{k} (y), y)$ . Here the layer domain uses the product sigma-algebra, not an assumed identification with the Borel sigma-algebra of the product topology. Its output $u_{K} : Y \to Q$ is a point reconstruction rule: if $u_{k}$ is Borel, the preimage of a measurable rectangle $A \times C$ under $y \mapsto (u_{k} (y), y)$ is $u_{k}^{- 1} (A) \cap C$ , so this pairing is product-measurable; composing it with $T_{ϕ, k}$ and applying finite induction proves that every $u_{k}$ is Borel. An amortized inverse map is a learned point estimator applied to multiple data inputs after a single fit; this term adds a reuse convention, not an accuracy guarantee.

For a real Hilbert signal space $H$ , a denoiser is a Borel map $D_{ϕ} : H \to H$ trained under a specified signal-corruption law and used to transform a corrupted signal into a signal estimate or an update. A denoiser is the exact minimum mean-square error map only when it equals the conditional mean for the specified signal and corruption laws. A learned prior is a supplied Borel probability measure $ρ_{ϕ}$ on $H$ ; one construction is the pushforward law $ρ_{ϕ} (A) = ν (G_{ϕ}^{- 1} (A))$ for $A \in B (H)$ , where $ν$ is a specified probability measure on a measurable source space $(Z, Z)$ and $G_{ϕ} : (Z, Z) \to (H, B (H))$ is measurable. The law or generator alone is not a data-to-target estimator.

For a finite horizon $T > 0$ , a specified parameter set $Φ$ , and $ϕ \in Φ$ , a score field model in a finite-dimensional signal space $R^{d}$ is a Borel map $s_{ϕ} : [0, T] \times R^{d} \to R^{d}$ intended to approximate the target field $s^{*} (t, x) = \nabla_{x} \log p_{t} (x)$ for a specified family $(p_{t})_{t \in [0, T]}$ of positive continuously differentiable probability densities for which $s^{*}$ is jointly Borel. Its complete description names a probability law $P_{f i t}$ for all variables used to fit $ϕ$ and a probability law $P_{t e s t}$ on $[0, T] \times R^{d}$ for evaluation inputs $(t, x)$ ; the target on those inputs is $s^{*} (t, x)$ . These laws need not agree, and no approximation guarantee under either law is implied. A score field is not itself a posterior law, posterior sample, or point reconstruction rule. A posterior sampler is a probability kernel $S : Y \to Q$ ; relative to a supplied posterior target kernel $Π_{y}$ , it is exact on a data domain $D$ when $S_{y} = Π_{y}$ as probability measures for every $y \in D$ . A draw from $S_{y}$ is random; obtaining a point estimate from it requires an additional summary rule. The name “learned” by itself asserts no exact recovery, stability, convergence, calibration, or train-to-test guarantee.

Definition references

Metric parameter/data model, admissible truths, forward map, and target-class map

Deterministic data-only estimator interface and its exactness convention

Evidence-normalized inverse posterior and data-indexed kernel convention

Real Hilbert signal spaces are complete real inner-product spaces

Measurable spaces and their sigma-algebras

Probability measures used for fitting and signal laws

Borel measurability of reconstruction maps

Probability kernels for posterior samplers

Product-measurable layer inputs for finite unrolling

Ongie et al., §§3.1 and 4.1–4.2.1, full paper

Daras et al., §§1.2 and 2.4.2–2.4.3, full survey

Dashti and Stuart, §3.2, full lecture notes

DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (gpt-6-luna)verified 2026-10-22 (gpt-6.1-sol)Open item page →

Inverse reconstruction risk under train and test laws

Definition

Let $(Y, Y)$ and $(Q, Q)$ be measurable data and target spaces, with $Q$ the Borel sigma-algebra of the target metric space. Let $P$ be a probability measure on the product space $(Y \times Q, Y \otimes Q)$ , and let $ℓ : Q \times Q \to [0, + \infty]$ be product-measurable, where $ℓ (t, a)$ is the loss for target $t$ and action $a$ . For a point reconstruction rule $g : (Y, Y) \to (Q, Q)$ measurable with respect to the stated sigma-algebras, its risk under $P$ is the extended nonnegative integral $R_{P} (g) : = \int_{Y \times Q} ℓ (t, g (y)) P (d y, d t) .$ For a randomized reconstruction rule given by a probability kernel $K$ from $Y$ to $Q$ , define $R_{P} (K) : = \int_{Y \times Q} ⁣ (\int_{Q} ℓ (t, a) K (y, d a)) P (d y, d t) .$ The inner integral is measurable in $(y, t)$ by kernel integration; a deterministic rule is the special case $K_{y} = δ_{g (y)}$ . When $P_{t r a i n}$ and $P_{t e s t}$ are specified joint laws on the same input-target space, the corresponding training-law risk and test-law risk are $R_{P_{t r a i n}} (K)$ and $R_{P_{t e s t}} (K)$ . Either value may be $+ \infty$ . This definition imposes no inequality between the two risks: any such comparison requires an additional assumption relating the joint laws or the rule's behavior under them.