Sampling finite populations with and without replacement #
For a random finite population x : κ → α with law ρ, both sampling laws use
samplePopulation: draw an independent selection k : ι → κ and return x ∘ k.
sampleWithoutReplacement uses the uniform law on injective selections;
sampleWithReplacement uses independent uniform indices, equivalently the uniform law on all
selections. Neither construction assumes symmetry of the population law.
For a nonempty population index, sampling with replacement is the mixture over ρ of the finite
product laws of the empirical measures empiricalMeasureOfFintype x. The collision bound gives the
two eventwise comparisons between sampling with and without replacement, with error equal to
the uniform-measure mass of colliding index selections, and hence at most choose |ι| 2 / |κ|.
This mass is a collision probability when the selection space is nonempty.
These comparisons apply to arbitrary probability population laws and feed
quantitative approximation results for finite exchangeable processes.
If no injective selection exists, sampling without replacement is the zero measure. Sampling
with replacement is also zero when the population index is empty and the sample index is not.
Probability preservation is therefore stated with an embedding into the population index for
sampling without replacement, and with a nonempty selection space ι → κ for sampling with
replacement, including when both index types are empty.
Main declarations #
sampleWithoutReplacement,sampleWithReplacement: the two finite sampling laws;pi_empiricalMeasureOfFintype_eq_map_uniformOn: independent empirical draws as uniform selections;sampleWithReplacement_eq_bind_pi_empiricalMeasureOfFintype: the empirical-product mixture;sampleWithoutReplacement_le_sampleWithReplacement_add,sampleWithReplacement_le_sampleWithoutReplacement_add: the eventwise collision bounds.sampleWithoutReplacement_le_sampleWithReplacement_add_collision,sampleWithReplacement_le_sampleWithoutReplacement_add_collision: the stronger bounds that retain the exact collision event, before applying the union bound.
References #
- P. Diaconis and D. Freedman, “Finite exchangeable sequences”, Annals of Probability 8 (1980), 745–764.
The law obtained by sampling a random finite population without replacement.
First draw a population x : κ → α with law ρ; independently and uniformly draw an injective
selection k : ι → κ; then return the sample i ↦ x (k i). This is samplePopulation along the
uniform law on injective index maps. If no injective selection exists, Mathlib's uniformOn
convention makes this the zero measure.
The results below take the population index finite with measurable singletons: uniform counting then distributes mass over finitely many injective selections.
Instances For
Sampling without replacement is samplePopulation along uniform injective selections.
Sampling a deterministic population without replacement is the pushforward of uniform injective selections.
Sampling without replacement preserves probability mass whenever an injective selection exists.
Independently sampling from a finite empirical population is the same as choosing a uniform map into the population and reading the selected entries.
Sampling with replacement from a random finite population.
First draw a population x : κ → α with law ρ; independently draw the indices k i : κ,
i : ι, independently and uniformly; then return the sample i ↦ x (k i). This is
samplePopulation along the ι-fold product of the uniform law on κ, which is the uniform law
on all index maps (sampleWithReplacement_eq_samplePopulation_uniformOn): the same construction
as sampleWithoutReplacement without the injectivity constraint. If κ is empty but ι is not,
no index map exists, and Mathlib's uniformOn convention makes this the zero measure.
The sample index is finite because the selection law is a finite product. Apart from the finite-law instance, the results below take the population index finite with measurable singletons.
Instances For
Sampling with replacement is samplePopulation along independent uniform indices.
Sampling with replacement from a finite population law gives a finite law.
Sampling with replacement is samplePopulation along the uniform law on all index maps.
Sampling a deterministic population with replacement is the pushforward of uniform selections, without an injectivity constraint.
Sampling with replacement from a random population preserves probability mass whenever a selection exists.
Sampling with replacement is the mixture of the finite product measures of the populations' empirical distributions.
Sampling without replacement from a random finite population increases the mass of a measurable event by at most the uniform-measure mass of colliding index selections. This mass is a collision probability when the selection space is nonempty.
Sampling with replacement from a random finite population increases the mass of a measurable event by at most the uniform-measure mass of colliding index selections. This mass is a collision probability when the selection space is nonempty.
Finite sampling bound, without replacement to with replacement. For every measurable
event, sampling without replacement from a random finite population has mass at most its
with-replacement mass plus the collision bound choose |ι| 2 / |κ|.
Finite sampling bound, with replacement to without replacement. For every measurable
event, sampling with replacement from a random finite population has mass at most its
without-replacement mass plus the collision bound choose |ι| 2 / |κ|.