LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-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.

Posterior quantiles are measurable and bracket their probability level

Statement

Write $Q$ for the canonical image of the rationals in $R$ under the embedding of The rationals embed densely in the reals.

Let $y \mapsto Π_{y}$ be a probability kernel on $R$ . For $u \in (0, 1)$ put $F_{y} (t) = Π_{y} ((- \infty, t]), q_{u} (y) = \inf {r \in Q : F_{y} (r) \geq u} .$ The infimum is taken in $R$ ; Every nonempty set bounded below has an infimum supplies it once the defining set is shown nonempty and bounded below. Then $q_{u} : Y \to R$ is measurable, and $Π_{y} ((- \infty, q_{u} (y))) \leq u \leq Π_{y} ((- \infty, q_{u} (y)]) .$

Facts & Assumptions

Given: The posterior probability kernel $Π$ and a fixed $u \in (0, 1)$ .

[F1]

Every event evaluation of a probability kernel is measurable, and each section is a probability measure. Measure kernel and probability kernel

[F2]

For increasing measurable sets, the measure of their union is the supremum of their measures. Continuity from below for measures

[F3]

For decreasing sets whose first member has finite measure, the measure of their intersection is the infimum of their measures. Continuity from above when one set has finite measure

[F4]

The rationals are dense in the reals. Both $Q$ and $R ∖ Q$ are dense in $R$ , and every nonempty open subset of $R$ is uncountable

[F5]

The rationals are countable and their injective embedding into $R$ restricts to a bijection onto this canonical image, so the union over $Q$ is countable. $Q$ is countably infinite, The rationals embed densely in the reals

[F6]

Every nonempty subset of $R$ that is bounded below has a real infimum; an infimum is a lower bound that is at least every other lower bound. Every nonempty set bounded below has an infimum, Greatest lower bound (infimum)

[F7]

A probability measure is monotone on nested measurable sets. Measures are monotone

[F8]

The canonical natural numbers are cofinal in the complete ordered field $R$ . Every complete ordered field is Archimedean

[F9]

For every real $ε > 0$ there is a natural $n \geq 1$ with $1 / n < ε$ ; for all $m \geq n$ , $1 / m \leq 1 / n$ , so $1 / m < ε$ . Thus $1 / n$ decreases to zero. For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ , Canonical naturals are positive and strictly increasing, Inverses of positives are positive, and reciprocation reverses order

[F10]

The Cauchy-sequence real field has the least-upper-bound property and is a complete ordered field, so the infimum and Archimedean results above apply to $R$ . The Cauchy-sequence reals have the least-upper-bound property

Proof

Given: The hypotheses in the Statement.

1.1givenF1F2F3F4F6F7F8F10choose

Fix $y$ . By [F8, F10], the sets $(- \infty, n]$ increase to $R$ , so [F2] gives $F_{y} (n) ↑ 1$ and some natural $n$ satisfies $F_{y} (n) \geq u$ . By [F4] choose a rational $r > n$ ; then [F7] gives $F_{y} (r) \geq u$ , so $S_{y} = {r \in Q : F_{y} (r) \geq u}$ is nonempty. Again by [F8, F10], the sets $(- \infty, - n]$ decrease to the empty set; [F3] gives some natural $m$ with $F_{y} (- m) < u$ . Choose a rational $s < - m$ by [F4]. For any rational $r \leq s$ , [F7] gives $F_{y} (r) \leq F_{y} (- m) < u$ , so every member of $S_{y}$ exceeds $s$ and $S_{y}$ is bounded below. Hence [F6, F10] gives its real infimum $q_{u} (y)$ .

2.1step 1.1F1F5F6F10

For each $c \in R$ , the infimum definition and nonemptiness give ${y : q_{u} (y) < c} = ⋃_{\begin{array}{c} r \in Q \\ r < c \end{array}} {y : F_{y} (r) \geq u} .$ Each set on the right is measurable by [F1], and the union is countable by [F5], so $q_{u}$ is measurable.

2.2givenF1F3F4F6F7F9algebrachoosestep 1.1

Suppose $Π_{y} ((- \infty, q_{u} (y)]) < u$ . By [F9], the sets $(- \infty, q_{u} (y) + 1 / n]$ decrease to $(- \infty, q_{u} (y)]$ ; they have finite measure by [F1], so [F3] gives an $n$ with $F_{y} (q_{u} (y) + 1 / n) < u$ . By [F4], choose rational $r$ with $q_{u} (y) < r < q_{u} (y) + 1 / n$ . Then [F7] gives $F_{y} (r) \leq F_{y} (q_{u} (y) + 1 / n) < u$ . Consequently no member of $S_{y}$ is at most $r$ , so $r$ is a lower bound of $S_{y}$ . Then $q_{u} (y) = \inf S_{y} \geq r > q_{u} (y)$ , a contradiction; therefore $u \leq Π_{y} ((- \infty, q_{u} (y)])$ .

3.1givenF1F2F4F6F7F9step 2.2choosestep 1.1∎

Suppose $Π_{y} ((- \infty, q_{u} (y))) > u$ . By [F9], the sets $(- \infty, q_{u} (y) - 1 / n]$ increase to $(- \infty, q_{u} (y))$ , so [F2] gives an $n$ with $F_{y} (q_{u} (y) - 1 / n) > u$ . By [F4], choose rational $r$ with $q_{u} (y) - 1 / n < r < q_{u} (y)$ . Then [F7] gives $F_{y} (r) \geq F_{y} (q_{u} (y) - 1 / n) > u$ , so $r \in S_{y}$ , contradicting that $q_{u} (y)$ is a lower bound of $S_{y}$ . Thus $Π_{y} ((- \infty, q_{u} (y))) \leq u$ . Combining with step 2.2 proves the CDF bracket.

Depends on

Used by

Dependency tree · two levels

69 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., §2.5 (standard reference, not scraped)
Alicia A. Johnson, Miles Q. Ott, and Mine Dogucu, Bayes Rules!, Chapter 8 §8.1 (standard reference, not scraped)