OAI/NumberTheory/ShortEgyptian/ScaleGeometry.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ShortEgyptian.dimM line 10
  2. def OAI.ShortEgyptian.dimX line 11
  3. def OAI.ShortEgyptian.dimC line 12
  4. def OAI.ShortEgyptian.scaleM line 13
  5. def OAI.ShortEgyptian.scaleRho line 14
  6. def OAI.ShortEgyptian.level line 15
  7. def OAI.ShortEgyptian.depth line 17
  8. def OAI.ShortEgyptian.levelMultiplier line 19
  9. def OAI.ShortEgyptian.binaryExponent line 21
  10. lemma OAI.ShortEgyptian.scaleM_bounds line 23
  11. lemma OAI.ShortEgyptian.level_pos line 37
  12. lemma OAI.ShortEgyptian.scaleRho_pos line 38
  13. lemma OAI.ShortEgyptian.scaleRho_le_one line 39
  14. lemma OAI.ShortEgyptian.level_succ line 42
  15. lemma OAI.ShortEgyptian.level_antitone line 49
  16. lemma OAI.ShortEgyptian.level_zero line 55
  17. lemma OAI.ShortEgyptian.level_before_depth line 57
  18. lemma OAI.ShortEgyptian.depth_level line 65
  19. lemma OAI.ShortEgyptian.depth_bound line 78
  20. lemma OAI.ShortEgyptian.levelMultiplier_pos line 94
  21. lemma OAI.ShortEgyptian.levelMultiplier_dvd line 98
  22. lemma OAI.ShortEgyptian.levelMultiplier_last line 107
  23. lemma OAI.ShortEgyptian.binary_power_lower line 112
  24. lemma OAI.ShortEgyptian.binary_power_upper line 121