OAI/NumberTheory/GaussianMoat/DifferenceSampling.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.GaussianMoat.walkSegment line 7
  2. def OAI.GaussianMoat.differences line 10
  3. theorem OAI.GaussianMoat.mem_walkSegment line 13
  4. theorem OAI.GaussianMoat.mem_differences line 17
  5. theorem OAI.GaussianMoat.card_le_card_differences line 21
  6. theorem OAI.GaussianMoat.walkSegment_dist_le line 33
  7. def OAI.GaussianMoat.joinedPath line 47
  8. theorem OAI.GaussianMoat.joinedPath_zero line 50
  9. theorem OAI.GaussianMoat.joinedPath_end line 53
  10. theorem OAI.GaussianMoat.joinedPath_step line 56
  11. theorem OAI.GaussianMoat.differences_card_of_triangle line 69
  12. def OAI.GaussianMoat.diameterRotation line 97
  13. theorem OAI.GaussianMoat.diameterRotation_norm line 99
  14. theorem OAI.GaussianMoat.diameterRotation_mul line 102
  15. theorem OAI.GaussianMoat.diameter_rectangle line 110
  16. theorem OAI.GaussianMoat.diameter_height line 126
  17. theorem OAI.GaussianMoat.walk_many_differences line 142