OAI/NumberTheory/GaussianMoat/AccurateScales.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.GaussianMoat.bandConstant line 10
  2. lemma OAI.GaussianMoat.bandConstant_pos line 13
  3. theorem OAI.GaussianMoat.entropyBand_from_margin line 17
  4. theorem OAI.GaussianMoat.eventually_poly_le_exp line 78
  5. theorem OAI.GaussianMoat.eventually_linear_le_square line 90
  6. def OAI.GaussianMoat.accurateGrid line 99
  7. def OAI.GaussianMoat.accurateIterations line 100
  8. lemma OAI.GaussianMoat.accurateGrid_pos line 102
  9. lemma OAI.GaussianMoat.accurateGrid_le_one line 104
  10. lemma OAI.GaussianMoat.accurateIterations_error line 107
  11. lemma OAI.GaussianMoat.accurateGrid_scale line 121
  12. theorem OAI.GaussianMoat.eventually_accurate_scale line 130
  13. theorem OAI.GaussianMoat.eventually_accurate_error line 145
  14. lemma OAI.GaussianMoat.eventually_const_le_exp_mul line 173
  15. lemma OAI.GaussianMoat.eventually_mul_le_double_exp line 179
  16. lemma OAI.GaussianMoat.eventually_accurate_small line 188
  17. lemma OAI.GaussianMoat.dense_sieve_cap line 198
  18. theorem OAI.GaussianMoat.eventually_accurate_band line 219
  19. lemma OAI.GaussianMoat.EntropyBand.size_cap line 284
  20. lemma OAI.GaussianMoat.EntropyBand.size_lower line 293
  21. lemma OAI.GaussianMoat.EntropyBand.size_pos line 308
  22. lemma OAI.GaussianMoat.bandSize_lower_of_scale line 318