OAI/NumberTheory/GaussianMoat/WindowParameters.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.GaussianMoat.topParameter line 13
  2. def OAI.GaussianMoat.topIterations line 14
  3. def OAI.GaussianMoat.topCoefficient line 15
  4. lemma OAI.GaussianMoat.topParameter_pos line 17
  5. lemma OAI.GaussianMoat.topParameter_small line 18
  6. lemma OAI.GaussianMoat.topCoefficient_pos line 19
  7. lemma OAI.GaussianMoat.top_deficit line 21
  8. theorem OAI.GaussianMoat.eventually_top_band line 24
  9. def OAI.GaussianMoat.topBlock line 88
  10. def OAI.GaussianMoat.topBlocks line 91
  11. def OAI.GaussianMoat.accurateBlock line 94
  12. lemma OAI.GaussianMoat.topBlocks_length line 98
  13. lemma OAI.GaussianMoat.topBlock_bound line 105
  14. lemma OAI.GaussianMoat.accurateBlock_bound line 114
  15. lemma OAI.GaussianMoat.sorted_split line 122
  16. lemma OAI.GaussianMoat.topBlocks_split line 138
  17. def OAI.GaussianMoat.windowBlocks line 153
  18. lemma OAI.GaussianMoat.windowBlocks_succ line 157
  19. lemma OAI.GaussianMoat.windowBlocks_split line 163
  20. lemma OAI.GaussianMoat.windowBlocks_mem line 176
  21. theorem OAI.GaussianMoat.separated_power_sum line 182
  22. lemma OAI.GaussianMoat.residueWeight_union_le line 207
  23. lemma OAI.GaussianMoat.residueWeight_biUnion_le line 214
  24. lemma OAI.GaussianMoat.separated_factor_cost line 222
  25. lemma OAI.GaussianMoat.log_two_lower line 239
  26. lemma OAI.GaussianMoat.narrow_bins_card line 244
  27. lemma OAI.GaussianMoat.topBlock_separated line 260
  28. theorem OAI.GaussianMoat.eventually_window_top line 271