TheoremStatement: 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.

Fixed-temperature generalized Bayes updates are sequentially coherent

Statement

Let $π_{0}$ be a probability prior on the parameter space of Generalized Bayes loss update and temperature, let $w > 0$ be fixed, and let $x_{1}, \dots, x_{n}$ be any finite sequence of observations with measurable real loss sections $ℓ_{i} (θ) : = ℓ (θ, x_{i})$ . Set $π_{i} : = G_{w, π_{i - 1}, x_{i}}$ recursively, and assume each sequential normalizer $z_{i} : = \int e^{- w ℓ_{i} (θ)} π_{i - 1} (d θ)$ is finite and positive. Then, for every measurable $A$ , $π_{n} (A) = \frac{\int_{A} e^{- w \sum_{i = 1}^{n} ℓ_{i} (θ)} π_{0} (d θ)}{\int e^{- w \sum_{i = 1}^{n} ℓ_{i} (θ)} π_{0} (d θ)}, \int e^{- w \sum_{i = 1}^{n} ℓ_{i} (θ)} π_{0} (d θ) = \prod_{i = 1}^{n} z_{i} .$ For $n = 0$ , the empty sum is zero, the empty product is one, and $π_{n} = π_{0}$ . Thus sequential updating at a fixed temperature agrees with one update using the sum of the observed losses. No independence or sampling-model assumption is asserted.

Facts & Assumptions

Given: A probability prior $π_{0}$ , a fixed temperature $w > 0$ , measurable real loss sections $ℓ_{1}, \dots, ℓ_{n}$ , and finite-positive sequential normalizers $z_{i}$ .

[F1]

Generalized Bayes loss update and temperature: when a prior, observation, temperature, and finite-positive normalizer are supplied, $G_{w, π, x} (A) = Z_{w} (π, x)^{- 1} \int_{A} e^{- w ℓ_{x}} d π .$

[F2]

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

[F3]

Integrating against a density agrees with integrating the product: for nonnegative measurable $f, g$ , $\int g d (f d π) = \int g f d π .$

[F4]

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

[F5]

The measure with density $f$ relative to $μ$ : $f d π$ is the measure $A \mapsto \int_{A} f d π$ for a nonnegative measurable $f$ .

[F6]

The principle of mathematical induction: if a property holds at a natural number and each case implies the next, it holds for every later natural number.

[F7]

Arithmetic and lattice operations preserve measurability whenever they are defined: sums and real scalar multiples of measurable real functions are measurable.

[F8]

The exponential addition formula $\exp (x + y) = \exp (x) \exp (y)$ : for all real $u, v$ , $e^{u + v} = e^{u} e^{v}$ .

[F9]

The real exponential function and the number $e$ by a power series: the power series definition gives $e^{0} = 1$ .

Proof

1.1F9F4givenalgebra

For $n = 0$ , the cumulative loss is the empty sum zero. In the power series definition [F9] at zero, the zeroth term is $1$ and every positive-degree term vanishes, so its exponential weight is $1$ . By [F4], $\int 1 d π_{0} = π_{0} (Θ) = 1$ . Thus the empty normalizer is the empty product one and the displayed formula is $π_{0} (A) = π_{0} (A)$ .

1.2F1F2givenbase

For $n = 1$ , the claim is exactly the update definition [F1], with $z_{1} = \int e^{- w ℓ_{1}} d π_{0}$ . This normalizer is finite positive by hypothesis, so the update is a probability by [F2].

1.3F7F1F8F3F5givenih

For $n \geq 2$ , suppose the formula holds at $n - 1$ , with cumulative normalizer $c_{n - 1} = \prod_{i = 1}^{n - 1} z_{i}$ and density $f_{n - 1} (θ) = e^{- w \sum_{i = 1}^{n - 1} ℓ_{i} (θ)}$ relative to $π_{0}$ . The finite cumulative loss is measurable by repeated use of [F7], so [F1] gives measurability of $f_{n - 1}$ and of $e^{- w ℓ_{n}}$ . Algebra and [F8] factor the cumulative exponential into $f_{n - 1} e^{- w ℓ_{n}}$ . Then [F3] gives $z_{n} = \int e^{- w ℓ_{n}} d π_{n - 1} = c_{n - 1}^{- 1} \int e^{- w \sum_{i = 1}^{n} ℓ_{i}} d π_{0} .$ Thus the cumulative normalizer is $c_{n} = c_{n - 1} z_{n} = \prod_{i = 1}^{n} z_{i}$ , which is finite and positive.

2.1F1F3F8F7step 1.3algebra

By [F1], [F3], and the same factorization [F8], for every measurable $A$ , $π_{n} (A) = z_{n}^{- 1} \int_{A} e^{- w ℓ_{n}} d π_{n - 1} = c_{n}^{- 1} \int_{A} e^{- w \sum_{i = 1}^{n} ℓ_{i}} d π_{0} .$ This proves the induction step.

3.1step 1.2step 1.3step 2.1F6step 1.1F4F2discharge-induction: step 2.1∎

Define $Q (m)$ to be the claimed formula at $n = m + 1$ . Step 1.2 proves $Q (0)$ . For any $m \in N$ , set $n = m + 2 \geq 2$ ; steps 1.3–2.1 prove that the formula at $n - 1 = m + 1$ implies it at $n = m + 2$ , hence $Q (m)$ implies $Q (m + 1)$ . Therefore [F6] gives the formula for every $n \geq 1$ ; step 1.1 covers $n = 0$ . The initial $π_{0}$ is a probability by [F4], and every later $π_{i}$ is a probability by [F2]. The proof uses only fixed-temperature updates and the stated normalizers.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

47 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)