PrimeHash.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

The bit-length dependence in prime hashing

The prime range has an explicit cardinality lower bound. Counting distinct prime divisors of a nonzero weight difference then gives the manuscript's lem:prime, with the full dependence on the bit-length parameter.

def OAI.LowSpaceSubsetSum.primeRange line 20
Source documentation
The finite prime range used by all modular filters.
```
def primeRange (ell : ℕ) : Finset ℕ :=
…
```
theorem OAI.LowSpaceSubsetSum.primeRange_prime line 23
theorem OAI.LowSpaceSubsetSum.primeRange_lt line 26
theorem OAI.LowSpaceSubsetSum.two_mul_succ_le_pow line 34
theorem OAI.LowSpaceSubsetSum.primeCounting_power_two_lower line 45
Source documentation
The elementary prime-counting lower bound needed for the sampling range.
```
theorem primeCounting_power_two_lower {ell : ℕ} (hell : 4 ≤ ell) :
    2 ^ ell ≤ 2 * ell * (2 ^ ell).primeCounting := by
…
```
theorem OAI.LowSpaceSubsetSum.primeRange_card_lower line 74
Source documentation
At least 2^ell/(4 ell) primes lie in the manuscript's finite range.
```
theorem primeRange_card_lower {ell : ℕ} (hell : 4 ≤ ell) :
    2 ^ ell ≤ 4 * ell * (primeRange ell).card := by
…
```
Mentions: OAI.LowSpaceSubsetSum.primeRange
theorem OAI.LowSpaceSubsetSum.two_pow_card_primeFactors_le line 95
theorem OAI.LowSpaceSubsetSum.card_primeFactors_lt line 106
Source documentation
A nonzero K-bit integer has fewer than K distinct prime divisors.
```
theorem card_primeFactors_lt {d K : ℕ} (hd : 0 < d) (hbits : d < 2 ^ K) :
    d.primeFactors.card < K := by
…
```

theorem OAI.LowSpaceSubsetSum.card_sampled_prime_divisors_le line 112

Source documentation

All sampled divisors are among the distinct prime factors of the difference.

theorem card_sampled_prime_divisors_le (P : Finset ℕ)
    (hP : ∀ p ∈ P, p.Prime) {d K : ℕ} (hd : 0 < d) (hbits : d < 2 ^ K) :
    (P.filter fun p => p ∣ d).card ≤ K := by
…

theorem OAI.LowSpaceSubsetSum.prime_divisor_probability_le line 122

Source documentation

Uniform prime hashing with its explicit polynomial-bit loss.

theorem prime_divisor_probability_le {ell u d : ℕ}
    (hell : 4 ≤ ell) (hellu : ell ≤ u) (hd : 0 < d) (hbits : d < 2 ^ (2 * u)) :
    (((primeRange ell).filter fun p => p ∣ d).card : ℝ) / (primeRange ell).card ≤
      8 * (u : ℝ) ^ 2 / (2 : ℝ) ^ ell := by
…

Mentions: OAI.LowSpaceSubsetSum.primeRange