OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/ExpBound.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.OrdinaryUniformWidth.ExpBound line 24
  2. def OAI.OrdinaryUniformWidth.WideBound line 25
  3. lemma OAI.OrdinaryUniformWidth.ExpBound.mono line 27
  4. lemma OAI.OrdinaryUniformWidth.WideBound.mono line 32
  5. lemma OAI.OrdinaryUniformWidth.ExpBound.weaken line 37
  6. lemma OAI.OrdinaryUniformWidth.WideBound.weaken line 42
  7. lemma OAI.OrdinaryUniformWidth.expBound_const line 48
  8. lemma OAI.OrdinaryUniformWidth.expBound_id line 54
  9. lemma OAI.OrdinaryUniformWidth.ExpBound.add line 60
  10. lemma OAI.OrdinaryUniformWidth.ExpBound.mul line 72
  11. lemma OAI.OrdinaryUniformWidth.ExpBound.toWide line 84
  12. lemma OAI.OrdinaryUniformWidth.wideBound_const line 88
  13. lemma OAI.OrdinaryUniformWidth.WideBound.mul line 90
  14. lemma OAI.OrdinaryUniformWidth.WideBound.add line 108
  15. lemma OAI.OrdinaryUniformWidth.WideBound.ceil line 126
  16. lemma OAI.OrdinaryUniformWidth.ExpBound.pow_two line 135