OAI/Geometry/TranslativeCovering/SourceParameters.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SourceParameters.ε line 19
  2. def OAI.SourceParameters.a line 20
  3. def OAI.SourceParameters.D line 21
  4. def OAI.SourceParameters.v line 22
  5. def OAI.SourceParameters.b line 23
  6. def OAI.SourceParameters.rminus line 24
  7. def OAI.SourceParameters.h line 25
  8. def OAI.SourceParameters.L line 26
  9. def OAI.SourceParameters.Cloc line 27
  10. def OAI.SourceParameters.N line 28
  11. def OAI.SourceParameters.M line 29
  12. lemma OAI.SourceParameters.a_pos line 30
  13. lemma OAI.SourceParameters.a_one line 31
  14. lemma OAI.SourceParameters.D_pos line 32
  15. lemma OAI.SourceParameters.L_limit line 33
  16. lemma OAI.SourceParameters.base_limit line 38
  17. lemma OAI.SourceParameters.base_log line 40
  18. lemma OAI.SourceParameters.length_rate line 45
  19. lemma OAI.SourceParameters.coarse_base line 74