OAI/Combinatorics/HadwigerCounterexample/ExponentialRates.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Exponential Rates

  1. def OAI.HadwigerCounterexample.bp line 16
  2. theorem OAI.HadwigerCounterexample.bp_zero line 17
  3. theorem OAI.HadwigerCounterexample.bp_one line 18
  4. theorem OAI.HadwigerCounterexample.bp_pos line 19
  5. theorem OAI.HadwigerCounterexample.bp_nat line 20
  6. theorem OAI.HadwigerCounterexample.bp_add line 21
  7. theorem OAI.HadwigerCounterexample.bp_sub line 23
  8. theorem OAI.HadwigerCounterexample.bp_neg line 25
  9. theorem OAI.HadwigerCounterexample.bp_mul_nat line 26
  10. theorem OAI.HadwigerCounterexample.bp_le line 28
  11. theorem OAI.HadwigerCounterexample.bp_lt line 30
  12. theorem OAI.HadwigerCounterexample.log_bp line 32
  13. theorem OAI.HadwigerCounterexample.bp_poly_dom line 34
  14. theorem OAI.HadwigerCounterexample.bp_poly_dom_nat line 43
  15. theorem OAI.HadwigerCounterexample.bp_tendsto line 48
  16. theorem OAI.HadwigerCounterexample.bp_tendsto_zero line 53
  17. def OAI.HadwigerCounterexample.ExpSmall line 61

    Source documentation

    Exponentially small at scale n.

    def ExpSmall (l : Filter ι) (n f : ι → ℝ) :=
…
  18. def OAI.HadwigerCounterexample.ExpO line 65

    Source documentation

    Subexponential upper bound at scale n.

    def ExpO (l : Filter ι) (n f : ι → ℝ) :=
…
  19. theorem OAI.HadwigerCounterexample.ExpSmall.mono line 69
  20. theorem OAI.HadwigerCounterexample.ExpSmall.zero line 73
  21. theorem OAI.HadwigerCounterexample.ExpSmall.mul line 77
  22. theorem OAI.HadwigerCounterexample.ExpSmall.add line 85
  23. theorem OAI.HadwigerCounterexample.ExpSmall.lim line 104
  24. theorem OAI.HadwigerCounterexample.expO_const line 114