OAI/Computability/DepthThree/LanguageParameters.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DepthThreeLowerBound.dataDimension line 9
  2. theorem OAI.DepthThreeLowerBound.five_mul_dataDimension_le line 11
  3. theorem OAI.DepthThreeLowerBound.lt_five_mul_dataDimension_add_five line 15
  4. theorem OAI.DepthThreeLowerBound.dataDimension_eq_zero_iff line 20
  5. theorem OAI.DepthThreeLowerBound.hashDimension_exists line 24
  6. def OAI.DepthThreeLowerBound.hashDimension line 28
  7. theorem OAI.DepthThreeLowerBound.hashDimension_zero line 32
  8. theorem OAI.DepthThreeLowerBound.hashDimension_spec line 35
  9. theorem OAI.DepthThreeLowerBound.hashDimension_pos line 40
  10. theorem OAI.DepthThreeLowerBound.hashDimension_cube_bound line 43
  11. theorem OAI.DepthThreeLowerBound.hashDimension_minimal line 49
  12. theorem OAI.DepthThreeLowerBound.hashDimension_le line 54
  13. theorem OAI.DepthThreeLowerBound.hashDimension_le_iff line 61
  14. theorem OAI.DepthThreeLowerBound.nat_le_sixth_power line 70
  15. theorem OAI.DepthThreeLowerBound.sixth_power_le_implies_le line 77
  16. def OAI.DepthThreeLowerBound.independenceOrder line 80
  17. theorem OAI.DepthThreeLowerBound.independenceOrder_zero line 83
  18. theorem OAI.DepthThreeLowerBound.independenceOrder_spec line 85
  19. theorem OAI.DepthThreeLowerBound.independenceOrder_even line 90
  20. theorem OAI.DepthThreeLowerBound.independenceOrder_pow_le line 93
  21. theorem OAI.DepthThreeLowerBound.independenceOrder_le line 96
  22. theorem OAI.DepthThreeLowerBound.independenceOrder_greatest line 99
  23. theorem OAI.DepthThreeLowerBound.independenceOrder_two_le_iff line 103
  24. theorem OAI.DepthThreeLowerBound.independenceOrder_eq_zero_iff line 114
  25. theorem OAI.DepthThreeLowerBound.independenceOrder_next_pow_gt line 120
  26. theorem OAI.DepthThreeLowerBound.independenceOrder_eq_iff line 130
  27. theorem OAI.DepthThreeLowerBound.independenceOrder_dataDimension_two_le_iff line 142
  28. def OAI.DepthThreeLowerBound.hashBlockLength line 148
  29. def OAI.DepthThreeLowerBound.hashOffset line 150
  30. def OAI.DepthThreeLowerBound.polynomialOffset line 152
  31. def OAI.DepthThreeLowerBound.coefficientsOffset line 154
  32. def OAI.DepthThreeLowerBound.coefficientOffset line 156
  33. def OAI.DepthThreeLowerBound.blockLen line 158
  34. theorem OAI.DepthThreeLowerBound.polynomialOffset_eq line 161
  35. theorem OAI.DepthThreeLowerBound.coefficientsOffset_eq line 164
  36. theorem OAI.DepthThreeLowerBound.blockLen_eq_sum line 167
  37. theorem OAI.DepthThreeLowerBound.blockLen_eq line 171
  38. theorem OAI.DepthThreeLowerBound.hashBlockLength_pos line 177
  39. theorem OAI.DepthThreeLowerBound.hashOffset_le_polynomialOffset line 182
  40. theorem OAI.DepthThreeLowerBound.polynomialOffset_le_coefficientsOffset line 186
  41. theorem OAI.DepthThreeLowerBound.coefficientsOffset_le_blockLen line 191
  42. theorem OAI.DepthThreeLowerBound.coefficientOffset_zero line 195
  43. theorem OAI.DepthThreeLowerBound.coefficientOffset_succ line 199
  44. theorem OAI.DepthThreeLowerBound.coefficientOffset_last line 203
  45. theorem OAI.DepthThreeLowerBound.coefficientOffset_mono line 206
  46. theorem OAI.DepthThreeLowerBound.hash_index_lt line 210
  47. theorem OAI.DepthThreeLowerBound.hash_absolute_index_lt line 215
  48. theorem OAI.DepthThreeLowerBound.polynomial_index_lt line 220
  49. theorem OAI.DepthThreeLowerBound.coefficient_index_lt line 224
  50. theorem OAI.DepthThreeLowerBound.blockLen_le_quad line 232
  51. theorem OAI.DepthThreeLowerBound.blockLen_le_four_mul_sub_one line 238