Collision probability

The collision probability of a discrete distribution is the probability that two independent samples agree, equivalently the sum of the squared masses. This quantity lets extraction bounds avoid logarithms: a pointwise mass bound also bounds collision probability. The ambient type may be infinite, including the type of binary words used by the computational definitions.

The distance-to-uniform estimate is the Cauchy–Schwarz step in the leftover hash lemma.

Main definitions

• Cslib.Probability.PMF.collisionProbability: sum of squared probability masses.

Main results

• Cslib.Probability.PMF.collisionProbability_eq_probability: independent-sample experiment.
• Cslib.Probability.PMF.collisionProbability_le_of_mass_le: pointwise mass upper bounds.
• Cslib.Probability.PMF.collisionProbability_pos, collisionProbability_le_one, toReal_le_sqrt_of_collisionProbability_le: elementary bounds.
• Cslib.Probability.PMF.collisionProbability_sq_le_sum_pow_three: Jensen, ‖p‖₂⁴ ≤ ‖p‖₃³.
• Cslib.Probability.PMF.four_mul_dist_sq_le_card_mul_sum_sq: Cauchy–Schwarz between statistical distance and ℓ₂ distance.
• Cslib.Probability.PMF.dist_uniform_le: distance to uniform from excess collisions.

References

• T. Holenstein, Pseudorandom Generators from One-Way Functions: A Simple Construction for Any Hardness, Section 3.3, proof of Lemma 1, equation (2).

Adapted from Probability/Collision.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using the upstream statistical-distance metric.

noncomputable def Cslib.Probability.PMF.collisionProbability {α : Type u_1} (p : PMF α) : ℝ

The probability that two independent samples from a discrete distribution agree.

theorem Cslib.Probability.PMF.collisionProbability_eq_sum {α : Type u_1} [Fintype α] (p : PMF α) : collisionProbability p = ∑ a : α, (p a).toReal ^ 2

For a finite ambient type, collision probability is a finite sum.

theorem Cslib.Probability.PMF.collisionProbability_nonneg {α : Type u_1} (p : PMF α) : 0 ≤ collisionProbability p

The collision probability is nonnegative.

theorem Cslib.Probability.PMF.summable_collision {α : Type u_1} (p : PMF α) : Summable fun (a : α) => (p a).toReal ^ 2

The squared probability masses of a PMF are summable.

theorem Cslib.Probability.PMF.collisionProbability_eq_probability {α : Type u_1} [DecidableEq α] (p : PMF α) : collisionProbability p = ((p.bind fun (a : α) => PMF.map (fun (b : α) => decide (a = b)) p) true).toReal

The sum of squared masses is exactly the success probability of comparing independent draws, using any equality decision procedure.

@[simp]

theorem Cslib.Probability.PMF.collisionProbability_uniform {α : Type u_1} [Fintype α] [Nonempty α] : collisionProbability (uniformOfFintype α) = (↑(Fintype.card α))⁻¹

The collision probability of a uniform source is its reciprocal cardinality.

theorem Cslib.Probability.PMF.collisionProbability_prod {α : Type u_1} {β : Type u_2} [Finite α] [Finite β] (p : PMF α) (q : PMF β) : collisionProbability (p.bind fun (a : α) => PMF.map (fun (x : β) => (a, x)) q) = collisionProbability p * collisionProbability q

Independent sources multiply their collision probabilities.

theorem Cslib.Probability.PMF.collisionProbability_le_of_mass_le {α : Type u_1} (p : PMF α) {bound : ℝ} (h : ∀ (a : α), (p a).toReal ≤ bound) : collisionProbability p ≤ bound

A bound on each individual mass also bounds the probability of a collision.

theorem Cslib.Probability.PMF.collisionProbability_le_one {α : Type u_1} (p : PMF α) : collisionProbability p ≤ 1

The collision probability is at most 1.

theorem Cslib.Probability.PMF.toReal_sq_le_collisionProbability {α : Type u_1} (p : PMF α) (a : α) : (p a).toReal ^ 2 ≤ collisionProbability p

The squared mass of each point is at most the collision probability.

theorem Cslib.Probability.PMF.toReal_le_sqrt_of_collisionProbability_le {α : Type u_1} (p : PMF α) {b : ℝ} (hb : collisionProbability p ≤ b) (a : α) : (p a).toReal ≤ √b

Every mass is at most the square root of a bound on the collision probability.

theorem Cslib.Probability.PMF.collisionProbability_pos {α : Type u_1} (p : PMF α) : 0 < collisionProbability p

The collision probability is positive.

theorem Cslib.Probability.PMF.collisionProbability_sq_le_sum_pow_three {α : Type u_1} [Fintype α] (p : PMF α) : collisionProbability p ^ 2 ≤ ∑ a : α, (p a).toReal ^ 3

Jensen's inequality for the collision probability: ‖p‖₂⁴ ≤ ‖p‖₃³, since the variance of p(a) for a drawn from p is nonnegative.

theorem Cslib.Probability.PMF.collisionProbability_map {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] (p : PMF α) (f : α → β) : collisionProbability (PMF.map f p) = ∑ a : α, ∑ b : α, if f a = f b then (p a).toReal * (p b).toReal else 0

A deterministic image collides exactly when the original samples have the same image.

theorem Cslib.Probability.PMF.collisionProbability_map_of_injective {α : Type u_1} {β : Type u_2} (p : PMF α) (f : α → β) (hf : Function.Injective f) : collisionProbability (PMF.map f p) = collisionProbability p

An injective encoding does not change collision probability. Both types may be infinite.

theorem Cslib.Probability.PMF.collisionProbability_conditionalSnd_uniform_map {α : Type u_1} {β : Type u_2} [Fintype α] [Nonempty α] (f : α → β) (b : β) [Nonempty { a : α // f a = b }] : collisionProbability (conditionalSnd (PMF.map (fun (a : α) => (f a, a)) (uniformOfFintype α)) b) = (↑(Nat.card { a : α // f a = b }))⁻¹

A uniform input conditioned on its image has collision probability reciprocal to the size of that image's fiber, even when different images have different fiber sizes.

theorem Cslib.Probability.PMF.four_mul_dist_sq_le_card_mul_sum_sq {α : Type u_1} [Fintype α] (p q : PMF α) : 4 * dist p q ^ 2 ≤ ↑(Fintype.card α) * ∑ a : α, ((p a).toReal - (q a).toReal) ^ 2

Cauchy–Schwarz between ℓ₁ and ℓ₂. On n points, 4 dist(p, q)² ≤ n ‖p - q‖₂².

theorem Cslib.Probability.PMF.dist_uniform_sq_le {α : Type u_1} [Fintype α] [Nonempty α] (p : PMF α) : 4 * dist p (uniformOfFintype α) ^ 2 ≤ ↑(Fintype.card α) * collisionProbability p - 1

Squared distance to uniform is controlled by the excess collision probability.

theorem Cslib.Probability.PMF.dist_uniform_le {α : Type u_1} [Fintype α] [Nonempty α] (p : PMF α) : dist p (uniformOfFintype α) ≤ √(↑(Fintype.card α) * collisionProbability p - 1) / 2

Cauchy–Schwarz bounds distance to uniform by the square root of excess collisions.