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.
Existence of a Dirichlet process by normalized gamma Poisson random measure
Statement
Assume the Axiom of Choice. Let be a standard Borel space and let be a finite nonzero measure on it. Then there is a measurable random probability measure whose law on the evaluation sigma-algebra of is . For every finite measurable partition , the unnormalized increments are independent with when , and almost surely when . Consequently the normalized masses have the finite-partition Dirichlet laws in Dirichlet process. These laws determine the probability law on uniquely.
The construction uses the Poisson random measure with intensity and normalizes its weighted projection onto . It does not assume a gamma-process existence theorem.
Facts & Assumptions
Given: Full AC, a standard Borel space , and a finite measure with .
The Axiom of Choice is assumed. The Axiom of Choice.
Full AC implies Countable Choice, which is the choice strength required by the local Gamma and Dirichlet normalization interfaces. AC implies DC implies countable choice The Axiom of Countable Choice ().
Countable products of standard Borel coordinate spaces admit the consistent product law under AC, and finite products remain standard Borel. The countable discrete space is standard Borel. Assuming the Axiom of Choice, Kolmogorov extension for arbitrary families of standard Borel coordinate spaces Standard Borel spaces Finite products of standard Borel spaces are standard Borel A countable discrete measurable space is standard Borel.
A Poisson count with finite mean has mass and mean , including the degenerate case. Exposure-parameterized Poisson law Normalization, moments, and generating function of the Poisson count law.
Finite product measures satisfy the rectangle product formula, and Tonelli applies to nonnegative functions on their sigma-finite products. For sigma-finite factors, the product measure exists, has the rectangle formula, is sigma-finite, and is unique Tonelli's theorem for nonnegative measurable functions on a sigma-finite product.
Under Countable Choice, the shape-rate Gamma law has density at rate , normalized for . Shape-rate Gamma distribution The shape-rate Gamma density is normalized.
For nonnegative measurable functions, Lebesgue change of variables holds under Countable Choice. A C^1 diffeomorphism satisfies the change-of-variables formula for nonnegative Lebesgue measurable functions.
The exponential integral and natural logarithm satisfy for and for . The integral exponential is the published exponential function The exponential tends to at and to at The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t.
A finite complex measure on with an exponential moment is determined by its Laplace transform on a real neighborhood of zero under AC. Uniqueness of a multivariate exponential transform.
A countable nonnegative weighted sum of measures is a measure, and each is a probability measure. Nonnegative scalar multiples and countable weighted sums of measures are measures The Dirac set function at a point A Dirac set function is a probability measure.
For positive Dirichlet parameters, the simplex density is normalized; the one-category law is the point mass at one. Dirichlet distribution, including the one-category case Dirichlet simplex density kernel Dirichlet density normalization by iterated Beta integrals.
Finite measures agreeing on a generating pi-system and the whole space are equal by finite-measure uniqueness and Dynkin's pi-lambda theorem. Pi-systems Finite measures agreeing on a generating pi-system and on the whole space are equal Dynkin's pi-lambda theorem.
Expectations of measurable functions are integrals against the random element's law. Change of variables for expectation Law or distribution of a random element Expectation of a nonnegative or integrable random variable.
Measurability of random elements is tested against the target sigma-algebra, and their laws are probability measures. Random elements and real random variables A measurable function between measurable spaces Probability measures and probability spaces.
Finite families of mutually independent random elements have the product joint law. Independent random elements have product joint law.
A finite measure is one with finite total mass, and sigma-finiteness is exhaustion by countably many finite-measure sets. Measures on sigma-algebras Finite, sigma-finite, and semifinite measures.
A law with the finite-partition Dirichlet conditions, when it exists, is denoted , and there is at most one such law. Dirichlet process.
Monotone convergence passes increasing nonnegative limits through the integral, and dominated convergence applies under an integrable bound. Monotone convergence for the integral Dominated convergence.
The Poisson mass formula and the exponential series give for when . Exposure-parameterized Poisson law The real exponential function and the number by a power series The exponential addition formula .
The binomial theorem gives . The binomial theorem in : .
The Euler integral defines and is finite and positive for . The real Gamma function by Euler's integral Euler's Gamma integral converges exactly for positive real parameters.
Independence means mutual factorization on measurable rectangles. Independent random elements.
The usual real line is Polish: the usual metric is complete and the rationals are countable and dense. Polish spaces are separable completely metrizable spaces and for with the Euclidean metric are complete, componentwise from the Cauchy criterion in is countably infinite The rationals embed densely in the reals.
Under Countable Choice, Lebesgue measure is a complete measure and every Borel set is Lebesgue measurable. Restrict it to the Borel sigma-algebra on . The function is nonnegative and Borel measurable because its factors are continuous there, so its integral over Borel sets defines a measure. Assuming countable choice, is a sigma-algebra containing every elementary set and is a complete measure extending elementary volume Assuming countable choice, every Borel subset of is Lebesgue measurable Continuity and derivatives of positive-base real powers The exponential function is smooth and A measurable function between measurable spaces Lebesgue measurable sets, the family , and the restricted set function The indefinite integral of a nonnegative measurable function is a measure.
Every Borel subset of a Polish space, with its trace Borel sigma-algebra, is standard Borel under AC. The set is open in the usual real line, hence Borel; apply [F21]. Borel subspaces admit polish presentations.
Proof
Given: The hypotheses in the Statement.
Put on ; [A2] and [F22] make this a measure on the Borel sigma-algebra with a nonnegative density relative to Lebesgue measure, and partition the mark axis into and for . These disjoint strips cover . For , because and there, while because , , and the interval length is . Also and by restricting to . Thus every strip has finite positive mass. By [F3] and [F14], is sigma-finite and has finite positive total . Let .
Index count coordinates by and mark coordinates by with . Their spaces are and , respectively, hence standard Borel by [F1], [F21], and [F23]. Assign every finite set of coordinates the product of the laws and . These finite-dimensional laws are consistent because coordinate projections of a finite product recover the corresponding marginal products. By [F1] and [A1] they extend to one probability law. The product rectangle formula gives mutual independence of each finite coordinate family by [F20], and [F13] identifies its joint law with the product. Thus it supports mutually independent and .
Define . Each is finite, so this is a countable sum of Dirac measures and is a counting measure by [F8]. For every measurable , its evaluation is the increasing limit of finite sums of measurable functions of the coordinates; hence is measurable. Thus is a random counting measure.
Fix pairwise-disjoint measurable sets with . Within strip , put and . Conditional on , independent marks assign counts with . There are assignments of the mark indices to these cells, and each assignment has probability , so the count vector has mass (with ). Summing over and using the Poisson mass in [F2] gives ; here and . Thus the strip counts are independent Poisson variables with means . The series over is the exponential series [F17].
Define for . This is a measurable nonnegative weighted sum of Dirac measures, hence a measure by [F8]. For each strip, independence of and its marks [F13], expectation against their law [F11], and from [F2] give . Monotone convergence [F16] then gives by [F3] and [F6].
Let be pairwise disjoint and choose . On strip , define . Conditional on , the independent marks give the exponential factor . Summing its Poisson series yields , where sums the first strips. The mark integral is finite on each strip because the strips are bounded away from zero and ; the Poisson series is [F17].
For each finite , the sums over are independent Poisson counts: convolution and [F18] give , and iteration handles . By [F16], their increasing total counts have . Thus the full counts are finite almost surely and the truncated integer counts eventually stabilize. Their joint point probabilities converge both to the point probabilities of the full count vector (by eventual stabilization) and to the product Poisson masses with means (by continuity of the Poisson mass formula in its mean). Hence the full counts are independent Poisson variables with means . Therefore satisfies Poisson random measure on a standard Borel space.
Since , almost surely: if it were infinite on a set of positive probability, its expectation would exceed every finite bound. Also, is measurable for every as a monotone limit of finite coordinate sums.
For , : use , Tonelli on the positive or negative part, and [F6]. In particular , by monotone convergence [F16] on the nonnegative truncations. For general , the truncated exponentials are dominated by ; [F16] therefore gives .
Let . For , [F4], [F5], and the Euler integral [F19], with , give for and . Thus the vector and the product of the corresponding Gamma laws have the same moment-generating transform near zero by step 4.3; [F3] supplies that finite product law, and [F7] identifies the distributions when is nonempty; if is empty this clause is vacuous. For each , step 3.3 gives . If with positive probability, some event has positive probability, forcing its nonnegative expectation to be positive; hence almost surely. Since there are finitely many cells, these zero coordinates are simultaneously zero almost surely. Their events in any measurable rectangle have probability zero or one, so adjoining these constants preserves the product law and independence.
For a partition with positive cells and parameters , the independent Gamma increments have product density . Change variables to and for , with . Its Jacobian has absolute value : factor from each of the proportion columns, then add the first rows of the remaining matrix to its last row, whose first entry becomes and whose other entries become zero. The inverse map is , , so this is a diffeomorphism on the positive orthant and open simplex. The joint density factors as the Gamma density in times on the simplex. Integrating the normalized Gamma factor in , which has total mass one by [F4], leaves the second factor as the marginal density of . By [F9] this is the Dirichlet law. With one positive cell the normalized mass is one, and zero-base cells have zero mass by step 5.1.
The total is Gamma by step 5.1, so it is strictly positive almost surely; step 4.2 gives finiteness. Since , the space is nonempty; choose and set on that probability-one event, assigning on its null complement. The event is measurable and each evaluation is measurable, so [F12] makes a random probability measure with the partition laws from step 6.1.
Finite evaluation cylinders form a generating pi-system for the evaluation sigma-algebra. For any , the nonempty intersections of and form a finite partition, and each is the sum of the corresponding cell masses. Hence its joint law is fixed by step 6.1. Two probability laws with those partition laws therefore agree on the generating pi-system; [F10] gives equality on the entire evaluation sigma-algebra. By [F15], this is uniqueness of .
Depends on
- Dirichlet process
- Poisson random measure on a standard Borel space
- Exposure-parameterized Poisson law
- Normalization, moments, and generating function of the Poisson count law
- The real exponential function and the number $e$ by a power series
- The exponential addition formula $\exp(x+y)=\exp(x)\exp(y)$
- The binomial theorem in $\mathbb{R}$: $(x+y)^{n} = \sum_{k<n+1} \iota\!\binom{n}{k}\, x^{k} y^{\,n-k}$
- Shape-rate Gamma distribution
- The shape-rate Gamma density is normalized
- Standard Borel spaces
- Lebesgue measurable sets, the family $\mathcal{L}(\mathbb{R}^n)$, and the restricted set function $\lambda_n$
- Assuming countable choice, $\mathcal{L}(\mathbb{R}^n)$ is a sigma-algebra containing every elementary set and $\lambda_n$ is a complete measure extending elementary volume
- Assuming countable choice, every Borel subset of $\mathbb{R}^n$ is Lebesgue measurable
- The indefinite integral of a nonnegative measurable function is a measure
- Continuity and derivatives of positive-base real powers
- The exponential function is smooth and $(\exp)'=\exp$
- Polish spaces are separable completely metrizable spaces
- $\mathbb{R}$ and $\mathbb{R}^n$ for $n \ge 1$ with the Euclidean metric are complete, componentwise from the Cauchy criterion in $\mathbb{R}$
- $\mathbb{Q}$ is countably infinite
- The rationals embed densely in the reals
- Finite products of standard Borel spaces are standard Borel
- A countable discrete measurable space is standard Borel
- Borel subspaces admit polish presentations
- Assuming the Axiom of Choice, Kolmogorov extension for arbitrary families of standard Borel coordinate spaces
- The Axiom of Choice
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
- AC implies DC implies countable choice
- Independent random elements
- Independent random elements have product joint law
- Probability measures and probability spaces
- Random elements and real random variables
- Law or distribution of a random element
- A measurable function between measurable spaces
- Measures on sigma-algebras
- Finite, sigma-finite, and semifinite measures
- For sigma-finite factors, the product measure exists, has the rectangle formula, is sigma-finite, and is unique
- Tonelli's theorem for nonnegative measurable functions on a sigma-finite product
- Change of variables for expectation
- Expectation of a nonnegative or integrable random variable
- Monotone convergence for the integral
- Dominated convergence
- Nonnegative scalar multiples and countable weighted sums of measures are measures
- The Dirac set function at a point
- A Dirac set function is a probability measure
- Dirichlet simplex density kernel
- Dirichlet distribution, including the one-category case
- Dirichlet density normalization by iterated Beta integrals
- The real Gamma function by Euler's integral
- Euler's Gamma integral converges exactly for positive real parameters
- A C^1 diffeomorphism satisfies the change-of-variables formula for nonnegative Lebesgue measurable functions
- The integral exponential $E$ is the published exponential function
- The exponential tends to $+\infty$ at $+\infty$ and to $0$ at $-\infty$
- The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t
- Uniqueness of a multivariate exponential transform
- Pi-systems
- Dynkin's pi-lambda theorem
- Finite measures agreeing on a generating pi-system and on the whole space are equal
Used by
- A base-null observation is a prior-predictive null fiber Example
- Finite-partition posterior and Pólya-urn draws Example
- A Dirichlet process assigns exponential mass to a finite-partition simplex neighborhood Lemma
- Dirichlet parameters add under coarsening Lemma
- The mixture prior places local KL and log-square mass near a compact smooth truth Lemma
- The posterior excludes large scales and mixing mass far from compact data Lemma
- Finite-partition conjugacy gives no density-contraction theorem Remark
- Dirichlet normal-mixture posterior contraction Theorem
- Dirichlet-process Pólya-urn predictive law Theorem
- Dirichlet-process posterior update Theorem
Dependency tree · two levels
247 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
- Günter Last and Mathew Penrose, Lectures on the Poisson Process, 2017, Chapters 1 and 3 (standard reference, not scraped)
- Thomas S. Ferguson, A Bayesian Analysis of Some Nonparametric Problems, 1973, Sections 2 and 3 (standard reference, not scraped)