OAI/Computability/DepthThree/SparseThresholds.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.DepthThreeLowerBound.SparseLevel line 13
  2. def OAI.DepthThreeLowerBound.nextSparseLevel line 19
  3. def OAI.DepthThreeLowerBound.sparseLevel line 26
  4. def OAI.DepthThreeLowerBound.sparseR line 31
  5. def OAI.DepthThreeLowerBound.sparseE line 32
  6. def OAI.DepthThreeLowerBound.sparseD line 33
  7. def OAI.DepthThreeLowerBound.sparseF line 34
  8. theorem OAI.DepthThreeLowerBound.sparseE_zero line 38
  9. theorem OAI.DepthThreeLowerBound.sparseD_zero line 39
  10. theorem OAI.DepthThreeLowerBound.sparseF_zero line 40
  11. theorem OAI.DepthThreeLowerBound.sparseE_one line 41
  12. theorem OAI.DepthThreeLowerBound.sparseD_one line 42
  13. theorem OAI.DepthThreeLowerBound.sparseF_one line 43
  14. theorem OAI.DepthThreeLowerBound.sparseR_succ_succ line 45
  15. theorem OAI.DepthThreeLowerBound.sparseF_succ_succ line 50
  16. theorem OAI.DepthThreeLowerBound.sparseE_succ_succ line 53
  17. theorem OAI.DepthThreeLowerBound.sparseD_succ_succ line 57
  18. theorem OAI.DepthThreeLowerBound.sparseR_ge_two line 61
  19. theorem OAI.DepthThreeLowerBound.sparseF_eq_sum_Ico line 73
  20. theorem OAI.DepthThreeLowerBound.sparseE_succ line 84
  21. theorem OAI.DepthThreeLowerBound.sparseD_eq line 90
  22. theorem OAI.DepthThreeLowerBound.sparseE_pos line 100
  23. theorem OAI.DepthThreeLowerBound.sparseD_pos line 111
  24. theorem OAI.DepthThreeLowerBound.sparse_entropy_bound line 115
  25. theorem OAI.DepthThreeLowerBound.sparseNumerics line 128
  26. def OAI.DepthThreeLowerBound.sparseM line 135
  27. theorem OAI.DepthThreeLowerBound.sparseM_eq line 137
  28. theorem OAI.DepthThreeLowerBound.sparseM_pos line 140
  29. theorem OAI.DepthThreeLowerBound.sparse_tolerance_pos line 144
  30. theorem OAI.DepthThreeLowerBound.exists_sparse_numerics line 149