OAI/NumberTheory/GaussianMoat/BatchCertificate.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.GaussianMoat.BatchCertificate line 10
  2. theorem OAI.GaussianMoat.BatchCertificate.sound line 43
  3. theorem OAI.GaussianMoat.greedy_finite_selection line 71
  4. def OAI.GaussianMoat.precedingFactors line 92
  5. lemma OAI.GaussianMoat.precedingFactors_mono line 95
  6. lemma OAI.GaussianMoat.precedingFactors_succ line 102
  7. lemma OAI.GaussianMoat.precedingFactors_ne_zero line 106
  8. theorem OAI.GaussianMoat.certificate_no_walk line 111
  9. theorem OAI.GaussianMoat.thin_bins line 151
  10. theorem OAI.GaussianMoat.eventually_separated_split_bins line 171
  11. lemma OAI.GaussianMoat.dyadicSieve_available_weight line 188
  12. lemma OAI.GaussianMoat.bandScale_add line 204
  13. lemma OAI.GaussianMoat.bandLength_add line 210
  14. lemma OAI.GaussianMoat.bandList_split line 215
  15. theorem OAI.GaussianMoat.band_first_crossing line 223
  16. lemma OAI.GaussianMoat.bandScale_log line 241
  17. theorem OAI.GaussianMoat.schedule_log_bound line 247