ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-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.

The unit-temperature likelihood update is ordinary Bayes in a finite model

Example

Let $Θ = {0, 1}$ have prior masses $π (0) = 1 / 3$ and $π (1) = 2 / 3$ . Let the observation space be $X = {0, 1}$ and define sampling laws by $P_{0} (Y = 1) = 1 / 4$ , $P_{0} (Y = 0) = 3 / 4$ , $P_{1} (Y = 1) = 3 / 4$ , and $P_{1} (Y = 0) = 1 / 4$ . These finite spaces with power-set sigma-algebras are standard Borel, and the displayed laws define a statistical experiment. Take $ℓ (θ, y) = - \log P_{θ} (Y = y)$ for every $(θ, y) \in Θ \times X$ . For observed $y = 1$ at $w = 1$ , the unnormalized masses are $1 / 12$ and $1 / 2$ , so the update is $(1 / 7, 6 / 7)$ . The same values follow by conditioning the joint prior-sampling law on $Y = 1$ .

Facts & Assumptions

Given: The parameter and observation spaces ${0, 1}$ with power-set sigma-algebras, prior $(1 / 3, 2 / 3)$ , and the four displayed sampling probabilities.

[F1]

A countable discrete measurable space is standard Borel: a nonempty at-most-countable set with its power-set sigma-algebra is standard Borel.

[F2]

Probability measures and probability spaces: a probability measure has total mass one.

[F3]

Statistical experiments: a statistical experiment consists of a sample measurable space, a parameter set, and a probability law on the sample space for each parameter.

[F4]

Generalized Bayes loss update and temperature: at $w = 1$ the update weights are proportional to $e^{- ℓ (θ, y)}$ and are normalized by their integral against the prior.

[F5]

A finite-normalizer loss update is a probability measure: a finite-positive-normalizer update is a probability measure.

[F6]

The natural logarithm as the inverse of the exponential function: $\log$ is the inverse of $\exp$ on $(0, \infty)$ .

[F7]

Conditional probability $P (A ∣ B)$ for $P (B) > 0$ : in a finite probability space, $\Pr (A ∣ B) = \Pr (A \cap B) / \Pr (B)$ when $\Pr (B) > 0$ .

Verification

1.1F1F2F3givenalgebra

Both parameter and sample spaces are nonempty finite sets, so [F1] makes them standard Borel. The prior masses are nonnegative and sum to one; each pair of sampling probabilities is nonnegative and sums to one. By [F2] these are probability measures, and [F3] therefore gives the stated finite statistical experiment.

2.1F6F4step 1.1algebra

All four likelihoods are positive, so [F6] makes $ℓ$ real-valued on $Θ \times X$ . Each parameter section is measurable because the parameter sigma-algebra is the power set, satisfying the loss hypotheses of [F4] for every $y \in X$ . At $y = 1$ , the inverse relation in [F6] gives $e^{- ℓ (θ, 1)} = e^{\log P_{θ} (Y = 1)} = P_{θ} (Y = 1)$ . Hence the unnormalized weights are $π (0) P_{0} (Y = 1) = \frac{1}{12}, π (1) P_{1} (Y = 1) = \frac{1}{2},$ and their normalizer is $Z = 1 / 12 + 1 / 2 = 7 / 12$ , finite and positive.

3.1F4F5step 2.1algebra

By [F4]–[F5], the update is a probability measure with $q (0) = \frac{1 / 12}{7 / 12} = \frac{1}{7}, q (1) = \frac{1 / 2}{7 / 12} = \frac{6}{7} .$ .

4.1F7step 1.1step 2.1step 3.1algebra∎

Define the joint masses by $\Pr (θ, y) = π (θ) P_{θ} (Y = y)$ . The four masses are $1 / 4, 1 / 12, 1 / 6, 1 / 2$ at $(0, 0), (0, 1), (1, 0), (1, 1)$ , respectively; they sum to one, and $\Pr (Y = 1) = 7 / 12 > 0$ . Applying [F7] to each parameter singleton gives $\Pr (θ = 0 ∣ Y = 1) = \frac{1 / 12}{7 / 12} = \frac{1}{7}, \Pr (θ = 1 ∣ Y = 1) = \frac{1 / 2}{7 / 12} = \frac{6}{7} .$ Thus the loss update equals the ordinary finite-model posterior at $y = 1$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

30 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

P. G. Bissiri, C. C. Holmes, and S. G. Walker, A general framework for updating belief distributions, JRSS B 78(5), 2016 (standard reference, not scraped)
J. Knoblauch, J. Jewson, and T. Damoulas, An Optimization-centric View on Bayes’ Rule: Reviewing and Generalizing Variational Inference, JMLR 23(132), 2022 (standard reference, not scraped)