ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generatedprecheck pass

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.

Point-null mass under atomic and continuous priors

Example

Let $M_{0}$ have parameter space $Θ_{0} = {0}$ and prior $Π_{0} = δ_{0}$ , and let $M_{1}$ have parameter space $Θ_{1} = [0, 1]$ and uniform prior $Π_{1} = λ ∣_{[0, 1]}$ . Use the common data space $Y = {0, 1}$ with counting measure $μ$ , and specify the jointly measurable Bernoulli density on each parameter space by $f_{i} (θ, 0) = 1 - θ$ and $f_{i} (θ, 1) = θ$ . Give the models prior weights $w_{0}, w_{1} > 0$ with $w_{0} + w_{1} = 1$ . After observing $y = 0$ , model $M_{0}$ has positive posterior probability because it is an explicit model atom with positive prior weight. A single continuous prior on $[0, 1]$ instead assigns $θ = 0$ probability zero.

Facts & Assumptions

Given: The two-model setup in the Example and observed value $y = 0$ .

[A1]

Countable Choice is assumed for the Lebesgue-volume formula used to compute interval and singleton measures. The Axiom of Countable Choice ( ${A C}_{ω}$ )

[F1]

For finitely many models with positive weights and finite positive evidences, posterior model probabilities are proportional to weight times evidence. Finite-model posterior probabilities and Bayes-factor odds

[F2]

Evidence under a proper parameter prior is the integral of the specified likelihood density against that prior. Marginal likelihoods, proper model evidence, and Bayes factors

[F3]

Lebesgue measure of an interval is its length. A box in $R^{n}$ with parameters $a_{i} \leq b_{i}$ is Lebesgue measurable of measure $\prod_{i < n} (b_{i} - a_{i})$ , whichever of its faces are included

[F4]

On $R$ , Lebesgue measure $λ$ is the restriction of Lebesgue outer measure to the Lebesgue measurable sets. Lebesgue measurable sets, the family $L (R^{n})$ , and the restricted set function $λ_{n}$

Verification

Given: The models, weights, and observation in the Example.

1.1A1F1F2F3givenalgebra

By [A1, F3], $λ ([0, 1]) = 1$ , so the uniform prior is proper. Under $M_{0}$ , $m_{0} (0) = 1$ . Under $M_{1}$ , its density is $1$ on $[0, 1]$ , so $m_{1} (0) = \int_{0}^{1} (1 - θ) d θ = 1 / 2$ . Both evidences are finite and positive, and [F1] gives $\Pr (M_{0} ∣ y = 0) = w_{0} / (w_{0} + w_{1} / 2) > 0$ .

2.1A1F3F4step 1.1algebra∎

By [F3], the degenerate closed interval $[0, 0] = {0}$ is Lebesgue measurable and has measure zero; [F4] identifies this measure as $λ$ . Thus the uniform prior assigns the singleton mass $\int_{{0}} 1 d λ = 0$ . The separate model atom in step 1.1 instead gives $θ = 0$ prior weight $w_{0}$ and positive posterior probability.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

32 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

Andrew Gelman et al., Bayesian Data Analysis, 3rd ed., §7.4 (standard reference, not scraped)
Alicia A. Johnson, Miles Q. Ott, and Mine Dogucu, Bayes Rules!, Chapter 8, §8.2.2 (standard reference, not scraped)