OAI/Combinatorics/LowSpaceSubsetSum/Counting/PrimeHashCollision.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Prime hashing supplies the finite collision interface

This connects the actual finite uniform prime sampler to the previously proved collision-to-occupancy theorem. Integer differences may have polynomially many bits; the parameter u remains explicit.

  1. def OAI.LowSpaceSubsetSum.primeProbability line 19
  2. theorem OAI.LowSpaceSubsetSum.primeRange_nonempty line 22
  3. theorem OAI.LowSpaceSubsetSum.primeProbability_sum line 29
  4. theorem OAI.LowSpaceSubsetSum.prime_pairwise_collision_bound line 35
  5. theorem OAI.LowSpaceSubsetSum.prime_occupied_probability line 56

    Source documentation

    The abstract occupancy result now has a proved prime-hashing input.

    theorem prime_occupied_probability (X : Finset ℤ) {ell u : ℕ}
    (hell : 4 ≤ ell) (hellu : ell ≤ u)
    (hbits : ∀ x ∈ X, ∀ y ∈ X, (x - y).natAbs < 2 ^ (2 * u))
    {T : ℝ} (hT : 0 < T) :
    1 - ((X.card : ℝ) + (8 * (u : ℝ) ^ 2 / (2 : ℝ) ^ ell) * (X.card : ℝ) ^ 2) / T ≤
      ∑ p ∈ (primeRange ell).filter
        (fun p : ℕ => (X.card : ℝ) ^ 2 / T ≤ ((X.image (fun x => x % (p : ℤ))).card : ℝ)),
          primeProbability ell p := by
…

    Mentions: OAI.LowSpaceSubsetSum.primeRange, OAI.LowSpaceSubsetSum.primeProbability