OAI/NumberTheory/GaussianMoat/SieveCertificate.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.GaussianMoat.SieveCertificate line 8
  2. def OAI.GaussianMoat.SieveCertificate.primes line 25
  3. lemma OAI.GaussianMoat.SieveCertificate.primes_spec line 28
  4. def OAI.GaussianMoat.SieveCertificate.sieve line 34
  5. lemma OAI.GaussianMoat.SieveCertificate.avoiding_batch line 37
  6. theorem OAI.GaussianMoat.SieveCertificate.sound line 43
  7. theorem OAI.GaussianMoat.finiteSieve_of_certificates line 52
  8. theorem OAI.GaussianMoat.entropyBand_from_suffix line 58
  9. lemma OAI.GaussianMoat.bandLength_le_exp_start line 102
  10. lemma OAI.GaussianMoat.bandLength_le_exp_at line 109