Uniform sampling with and without replacement

This file gives the finite sampling estimate underlying quantitative finite de Finetti theorems. When the finite function space ι → κ is nonempty, a uniform random map x : ι → κ has two coordinates collide with probability at most

(Fintype.card ι).choose 2 / Fintype.card κ.

When the function space is empty, Mathlib's uniformOn is instead the zero measure, and the same inequality remains valid under that convention.

When injective maps exist, conditioning the random map to be injective is uniform sampling without replacement. The main results compare every event under the uniform measures on all maps and on injective maps, with the collision bound as error. These inequalities remain valid when no injective map exists (when Mathlib's uniformOn is the zero measure); in the feasible case they are the coupling step used to compare a finite exchangeable law with the product of its empirical measure.

The proof is the classical union bound over the unordered pairs of coordinates. It uses Mathlib's ProbabilityTheory.uniformOn, measure_biUnion_finset_le, and Fintype.card_product_filter_lt; no sampling distribution is redefined here.

Main results

• uniformOn_not_injective_le bounds the probability of a collision;
• uniformOn_le_univ_add_compl and uniformOn_univ_le_add_compl give the general conditioning comparison;
• uniformOn_injective_le_add and uniformOn_univ_le_injective_add compare arbitrary events under sampling without and with replacement;
• uniformOn_injective_le_add_choose_two_div and uniformOn_univ_le_injective_add_choose_two_div give the quantitative forms.

This advances Layer 8, "finite de Finetti bounds", of the Exchangeability roadmap.

theorem TauCeti.Probability.uniformOn_toReal {Ω : Type u_3} [Finite Ω] [MeasurableSpace Ω] [MeasurableSingletonClass Ω] (S T : Set Ω) : ((ProbabilityTheory.uniformOn S) T).toReal = ↑(Nat.card { x : Ω // x ∈ S ∩ T }) / ↑(Nat.card { x : Ω // x ∈ S })

The real-valued probability of an event under a finite uniform sample is the ratio of its cardinality to the cardinality of the sampling set.

@[simp]

theorem TauCeti.Probability.uniformOn_apply_eq_apply {ι : Type u_1} {κ : Type u_2} [Fintype κ] [Finite ι] [MeasurableSpace κ] [MeasurableSingletonClass κ] [Nonempty κ] (i j : ι) (hij : i ≠ j) : (ProbabilityTheory.uniformOn Set.univ) {x : ι → κ | x i = x j} = 1 / ↑(Fintype.card κ)

Under uniform sampling with replacement, two distinct coordinates agree with probability 1 / Fintype.card κ.

The result is stated for arbitrary finite index and value types. The only measurable structure needed is discreteness of finite sets, expressed by MeasurableSingletonClass.

theorem TauCeti.Probability.uniformOn_not_injective_le {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] [MeasurableSpace κ] [MeasurableSingletonClass κ] : (ProbabilityTheory.uniformOn Set.univ) {x : ι → κ | ¬Function.Injective x} ≤ ↑((Fintype.card ι).choose 2) / ↑(Fintype.card κ)

Collision bound for uniform sampling. When the function space ι → κ is nonempty, a uniform map from ι to κ fails to be injective with probability at most (Fintype.card ι).choose 2 / Fintype.card κ. When the function space is empty, uniformOn is the zero measure and the inequality remains valid under that convention.

This is the union bound over the unordered pairs of coordinates. It remains valid when the right-hand side exceeds one, avoiding an unnecessary size assumption on the sample.

theorem TauCeti.Probability.uniformOn_le_univ_add_compl {Ω : Type u_3} [Finite Ω] [MeasurableSpace Ω] [MeasurableSingletonClass Ω] (E A : Set Ω) : (ProbabilityTheory.uniformOn E) A ≤ (ProbabilityTheory.uniformOn Set.univ) A + (ProbabilityTheory.uniformOn Set.univ) Eᶜ

Conditioning a finite uniform sample on an event E can increase the probability of an event A by at most the original probability of Eᶜ, provided E is nonempty. When E is empty, Mathlib's uniformOn E is the zero measure and the inequality remains valid under that convention.

This is the upper half of the elementary coupling bound between a uniform law and its conditioning.

theorem TauCeti.Probability.uniformOn_univ_le_add_compl {Ω : Type u_3} [Finite Ω] [MeasurableSpace Ω] [MeasurableSingletonClass Ω] (E A : Set Ω) : (ProbabilityTheory.uniformOn Set.univ) A ≤ (ProbabilityTheory.uniformOn E) A + (ProbabilityTheory.uniformOn Set.univ) Eᶜ

Conditioning a finite uniform sample on an event E can decrease the probability of an event A by at most the original probability of Eᶜ, provided E is nonempty. When E is empty, Mathlib's uniformOn E is the zero measure and the inequality remains valid under that convention.

This is the lower half of the elementary coupling bound between a uniform law and its conditioning.

theorem TauCeti.Probability.uniformOn_injective_le_add {ι : Type u_1} {κ : Type u_2} [Finite ι] [Finite κ] [MeasurableSpace κ] [MeasurableSingletonClass κ] (A : Set (ι → κ)) : (ProbabilityTheory.uniformOn {x : ι → κ | Function.Injective x}) A ≤ (ProbabilityTheory.uniformOn Set.univ) A + (ProbabilityTheory.uniformOn Set.univ) {x : ι → κ | ¬Function.Injective x}

The uniform measure on injective maps differs from the uniform measure on all maps only on the collision event: for every event A, the former is at most the latter plus the collision measure.

When an injective map ι → κ exists, these are the probabilities for uniform sampling without and with replacement, respectively. The inequality also holds when the set of injective maps is empty, in which case its uniformOn measure is zero.

theorem TauCeti.Probability.uniformOn_univ_le_injective_add {ι : Type u_1} {κ : Type u_2} [Finite ι] [Finite κ] [MeasurableSpace κ] [MeasurableSingletonClass κ] (A : Set (ι → κ)) : (ProbabilityTheory.uniformOn Set.univ) A ≤ (ProbabilityTheory.uniformOn {x : ι → κ | Function.Injective x}) A + (ProbabilityTheory.uniformOn Set.univ) {x : ι → κ | ¬Function.Injective x}

The uniform measure on all maps differs from the uniform measure on injective maps only on the collision event: for every event A, the former is at most the latter plus the collision measure.

When an injective map ι → κ exists, these are the probabilities for uniform sampling with and without replacement, respectively. The inequality also holds when the set of injective maps is empty, in which case its uniformOn measure is zero.

theorem TauCeti.Probability.uniformOn_injective_le_add_choose_two_div {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] [MeasurableSpace κ] [MeasurableSingletonClass κ] (A : Set (ι → κ)) : (ProbabilityTheory.uniformOn {x : ι → κ | Function.Injective x}) A ≤ (ProbabilityTheory.uniformOn Set.univ) A + ↑((Fintype.card ι).choose 2) / ↑(Fintype.card κ)

Quantitative finite-sampling bound, injective maps to all maps. For every event A, its uniform measure among injective maps is at most its uniform measure among all maps plus (Fintype.card ι).choose 2 / Fintype.card κ.

When an injective map ι → κ exists, this compares uniform sampling without replacement to uniform sampling with replacement. The inequality also holds in the degenerate case.

theorem TauCeti.Probability.uniformOn_univ_le_injective_add_choose_two_div {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] [MeasurableSpace κ] [MeasurableSingletonClass κ] (A : Set (ι → κ)) : (ProbabilityTheory.uniformOn Set.univ) A ≤ (ProbabilityTheory.uniformOn {x : ι → κ | Function.Injective x}) A + ↑((Fintype.card ι).choose 2) / ↑(Fintype.card κ)

Quantitative finite-sampling bound, all maps to injective maps. For every event A, its uniform measure among all maps is at most its uniform measure among injective maps plus (Fintype.card ι).choose 2 / Fintype.card κ.

When an injective map ι → κ exists, this compares uniform sampling with replacement to uniform sampling without replacement. The inequality also holds in the degenerate case.