Birthday bound

DefinitionThe collision experiment#✓fully proved

For a nonempty finite set \(\alpha\) and a natural number \(q\), the collision experiment is the probability distribution on \(\{\mathrm{true}, \mathrm{false}\}\) obtained by drawing a function \(s \colon \{0, \dots, q - 1\} \to \alpha\) uniformly at random (equivalently, \(q\) independent uniform samples \(s(0), \dots, s(q - 1)\) from \(\alpha\)) and outputting true exactly when \(s\) is not injective, that is, when \(s(i) = s(j)\) for some \(i \ne j\).

noncomputable def collisionGame : PMF Bool :=
  (Cslib.Probability.PMF.uniformOfFintype (Fin q → α)).map fun s => !decide (Function.Injective s)

Used by 2

Used byCollision probability · The exact collision probability

DefinitionCollision probability#✓fully proved

For a nonempty finite set \(\alpha\) and a natural number \(q\), the collision probability is the probability, as a real number, that the collision experiment with \(q\) samples from \(\alpha\) outputs true, that is, that \(q\) independent uniform samples from \(\alpha\) contain two equal samples at distinct positions.

noncomputable def collisionProb : ℝ := (collisionGame α q true).toReal

Uses 1 · Used by 8

Statement usesThe collision experiment

Used byThe exact collision probability · Birthday lower bound · Birthday lower bound as stated in Katz and Lindell · Birthday lower bound for at most square-root many samples · Birthday upper bound · Birthday lower bound, rational form · Even odds of a collision · Birthday lower bound, exponential form

TheoremThe exact collision probability#✓fully proved

Let \(\alpha\) be a nonempty finite set with \(N\) elements and \(q\) a natural number. The probability that \(q\) independent uniform samples from \(\alpha\) contain a collision equals \(1 - N (N - 1) \cdots (N - q + 1) / N^q\), where the product \(N (N - 1) \cdots (N - q + 1)\) has \(q\) factors (it is \(1\) for \(q = 0\) and \(0\) for \(q > N\)).

theorem collisionProb_eq :
    collisionProb α q =
      1 - ((Fintype.card α).descFactorial q : ℝ) / (Fintype.card α : ℝ) ^ q

Uses 2 · Used by 2

Statement usesCollision probability

Proof usesThe collision experiment

Used byBirthday upper bound · Birthday lower bound, exponential form

TheoremBirthday upper bound#✓fully proved

Let \(\alpha\) be a nonempty finite set with \(N\) elements and \(q\) a natural number. The probability that \(q\) independent uniform samples from \(\alpha\) contain a collision is at most \(q (q - 1) / (2 N)\).

This implies Katz and Lindell's Lemma A.15, which states the bound \(q^2 / (2 N)\).

theorem collisionProb_le :
    collisionProb α q ≤ q * (q - 1) / (2 * Fintype.card α)

Uses 2

Statement usesCollision probability

Proof usesThe exact collision probability

TheoremBirthday lower bound, exponential form#✓fully proved

Let \(\alpha\) be a nonempty finite set with \(N\) elements and \(q\) a natural number. The probability that \(q\) independent uniform samples from \(\alpha\) contain a collision is at least \(1 - \exp(-q (q - 1) / (2 N))\).

theorem one_sub_exp_le_collisionProb :
    1 - Real.exp (-(q * (q - 1) / (2 * Fintype.card α))) ≤ collisionProb α q

Uses 2 · Used by 1

Statement usesCollision probability

Proof usesThe exact collision probability

Used byBirthday lower bound, rational form

TheoremBirthday lower bound, rational form#✓fully proved

Let \(\alpha\) be a nonempty finite set with \(N\) elements, \(q\) a natural number, and \(x = q (q - 1) / (2 N)\). The probability that \(q\) independent uniform samples from \(\alpha\) contain a collision is at least \(x / (1 + x)\).

theorem div_one_add_le_collisionProb :
    (q * (q - 1) / (2 * Fintype.card α)) / (1 + q * (q - 1) / (2 * Fintype.card α)) ≤
      collisionProb α q

Uses 2 · Used by 2

Statement usesCollision probability

Proof usesBirthday lower bound, exponential form

Used byBirthday lower bound · Even odds of a collision

TheoremBirthday lower bound#✓fully proved

Let \(\alpha\) be a nonempty finite set with \(N\) elements and \(q\) a natural number with \(q (q - 1) \le 2 N\). The probability that \(q\) independent uniform samples from \(\alpha\) contain a collision is at least \(q (q - 1) / (4 N)\).

This strengthens Katz and Lindell's Lemma A.16, whose hypothesis \(q \le \sqrt{2 N}\) implies \(q (q - 1) \le 2 N\).

theorem collisionProb_ge (h : (q : ℝ) * (q - 1) ≤ 2 * Fintype.card α) :
    q * (q - 1) / (4 * Fintype.card α) ≤ collisionProb α q

Uses 2 · Used by 1

Statement usesCollision probability

Proof usesBirthday lower bound, rational form

Used byBirthday lower bound as stated in Katz and Lindell

TheoremBirthday lower bound as stated in Katz and Lindell#✓fully proved

Let \(\alpha\) be a nonempty finite set with \(N\) elements and \(q\) a natural number with \(q \le \sqrt{2 N}\). The probability that \(q\) independent uniform samples from \(\alpha\) contain a collision is at least \(q (q - 1) / (4 N)\).

This is Lemma A.16 of Katz and Lindell (2nd ed.): "say \(q \le \sqrt{2N}\) elements are chosen uniformly and independently ... at least \(q (q - 1) / (4N)\)".

theorem collisionProb_ge_of_le_sqrt (h : (q : ℝ) ≤ Real.sqrt (2 * Fintype.card α)) :
    q * (q - 1) / (4 * Fintype.card α) ≤ collisionProb α q

Uses 2 · Used by 1

Statement usesCollision probability

Proof usesBirthday lower bound

Used byBirthday lower bound for at most square-root many samples

TheoremBirthday lower bound for at most square-root many samples#✓fully proved

Let \(\alpha\) be a nonempty finite set with \(N\) elements and \(q\) a natural number with \(q \le \sqrt{N}\). The probability that \(q\) independent uniform samples from \(\alpha\) contain a collision is at least \(q (q - 1) / (4 N)\).

theorem collisionProb_ge_of_le_sqrt_card (h : (q : ℝ) ≤ Real.sqrt (Fintype.card α)) :
    q * (q - 1) / (4 * Fintype.card α) ≤ collisionProb α q

Uses 2

Statement usesCollision probability

Proof usesBirthday lower bound as stated in Katz and Lindell

TheoremEven odds of a collision#✓fully proved

Let \(\alpha\) be a nonempty finite set with \(N\) elements and \(q\) a natural number with \(2 N \le q (q - 1)\). The probability that \(q\) independent uniform samples from \(\alpha\) contain a collision is at least \(1/2\).

theorem half_le_collisionProb (h : 2 * (Fintype.card α : ℝ) ≤ q * (q - 1)) :
    1 / 2 ≤ collisionProb α q

Uses 2

Statement usesCollision probability

Proof usesBirthday lower bound, rational form

10 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.