OAI/Combinatorics/EditDistance/PrimePool.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Finite pools of distinct primes from central binomial estimates

  1. def OAI.EditPrimes.pool line 13
  2. lemma OAI.EditPrimes.centralBinom_le_with_primes line 15
  3. lemma OAI.EditPrimes.binomial_log_bound line 87
  4. lemma OAI.EditPrimes.pool_square_large line 109
  5. theorem OAI.EditPrimes.eventually_pool_square line 142
  6. theorem OAI.EditPrimes.primes_of_pool line 154