ProductHash.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Independent product-modulus collisions

Sample identities, rather than distinct numerical products, form the finite probability space. The factors are allowed to repeat. Product divisibility implies each factor divides the difference, which is all the upper bound needs.

theorem OAI.LowSpaceSubsetSum.product_divisor_count_le line 18

theorem OAI.LowSpaceSubsetSum.product_divisor_probability_le line 36

Source documentation

Independent uniform sampling multiplies the individual collision bounds. No coprimality or distinctness of the sampled factors is assumed.

theorem product_divisor_probability_le (A : Finset α) (B : Finset β)
    (f : α → ℕ) (g : β → ℕ) (d : ℕ) (hA : A.Nonempty) (hB : B.Nonempty)
    {deltaA deltaB : ℝ} (hdeltaA : 0 ≤ deltaA)
    (ha : ((A.filter fun a => f a ∣ d).card : ℝ) / A.card ≤ deltaA)
    (hb : ((B.filter fun b => g b ∣ d).card : ℝ) / B.card ≤ deltaB) :
    (((A ×ˢ B).filter fun z => f z.1 * g z.2 ∣ d).card : ℝ) /
      (A ×ˢ B).card ≤ deltaA * deltaB := by
…