OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/MajorWidth.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.OrdinaryUniformWidth.majorWidth line 27
  2. def OAI.OrdinaryUniformWidth.primeEnd line 28
  3. def OAI.OrdinaryUniformWidth.approxBound line 29
  4. def OAI.OrdinaryUniformWidth.shortWidth line 31
  5. def OAI.OrdinaryUniformWidth.longGate line 35
  6. lemma OAI.OrdinaryUniformWidth.majorWidth_pos line 37
  7. lemma OAI.OrdinaryUniformWidth.primeEnd_pos line 39
  8. lemma OAI.OrdinaryUniformWidth.approxBound_pos line 40
  9. lemma OAI.OrdinaryUniformWidth.shortWidth_pos line 41
  10. lemma OAI.OrdinaryUniformWidth.expBound_affine line 43
  11. lemma OAI.OrdinaryUniformWidth.pow_wide line 47
  12. lemma OAI.OrdinaryUniformWidth.majorWidth_wide line 49
  13. lemma OAI.OrdinaryUniformWidth.primeEnd_wide line 77
  14. lemma OAI.OrdinaryUniformWidth.primeSpan_wide line 86
  15. lemma OAI.OrdinaryUniformWidth.approxBound_wide line 94
  16. lemma OAI.OrdinaryUniformWidth.shortWidth_wide line 104
  17. lemma OAI.OrdinaryUniformWidth.longGate_wide line 120