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.

A finite-normalizer loss update is a probability measure

Statement

Let $G_{w, π, x}$ be the update of Generalized Bayes loss update and temperature, with prior probability $π$ and normalizer $0 < Z_{w} (π, x) < \infty$ . Then $G_{w, π, x}$ is a probability measure on $(Θ, T)$ .

Facts & Assumptions

Given: A prior probability $π$ , a fixed observation $x$ , a temperature $w > 0$ , and $0 < Z_{w} (π, x) < \infty$ .

[F1]

Generalized Bayes loss update and temperature: for each measurable $A \subseteq Θ$ , $G_{w, π, x} (A) = Z_{w} (π, x)^{- 1} \int_{A} e^{- w ℓ_{x} (θ)} π (d θ) .$

[F2]

The measure with density $f$ relative to $μ$ : if $f \geq 0$ is measurable, then $A \mapsto \int_{A} f d π$ is a measure.

[F3]

Nonnegative scalar multiples and countable weighted sums of measures are measures: a nonnegative scalar multiple of a measure is a measure.

[F4]

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

[F5]

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

Proof

1.1F1F2given

Put $f (θ) = e^{- w ℓ_{x} (θ)}$ and $μ (A) = \int_{A} f d π$ . By [F1]–[F2], $μ$ is the measure with density $f$ relative to $π$ .

2.1F1F3F4step 1.1given

Since $Z_{w} (π, x) > 0$ , [F1] gives $G_{w, π, x} = Z_{w} (π, x)^{- 1} μ$ , which is a measure by [F3]. Also [F4] gives $μ (Θ) = \int_{Θ} 1 d (f d π) = \int_{Θ} f d π = Z_{w} (π, x),$ so $G_{w, π, x} (Θ) = 1$ .

3.1F5step 2.1∎

By [F5], the measure in step 2.1 with total mass one is a probability measure.

Depends on

Used by

Dependency tree · two levels

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