Documentation

Complexity.Probability.Collision

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 #

Main results #

References #

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

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

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

Instances For
    source
    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.

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

    The collision probability is nonnegative.

    source
    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.

    source
    @[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.

    source
    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.

    source
    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.

    source
    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.

    source
    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.

    source
    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.

    source
    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.

    source
    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.