OAI/Computability/DepthThree/LanguageInputBlockWords.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DepthThreeLowerBound.list_eq_ofFn_of_getD line 9
  2. theorem OAI.DepthThreeLowerBound.inputBlockData_data_length line 17
  3. theorem OAI.DepthThreeLowerBound.inputBlockData_hash_length line 21
  4. theorem OAI.DepthThreeLowerBound.inputBlockData_polynomial_length line 26
  5. theorem OAI.DepthThreeLowerBound.inputBlockData_coefficients_length line 30
  6. theorem OAI.DepthThreeLowerBound.decoded_ringDegree_ne_zero line 35
  7. theorem OAI.DepthThreeLowerBound.inputBlockData_data_eq_ofFn line 39
  8. theorem OAI.DepthThreeLowerBound.inputBlockData_hash_eq_ofFn line 44
  9. theorem OAI.DepthThreeLowerBound.inputBlockData_polynomial_eq_ofFn line 49
  10. def OAI.DepthThreeLowerBound.decodedCoefficientBlocks line 54
  11. theorem OAI.DepthThreeLowerBound.decodedCoefficientBlocks_length line 57
  12. theorem OAI.DepthThreeLowerBound.decodedCoefficientBlocks_row_length line 61
  13. theorem OAI.DepthThreeLowerBound.decodedCoefficientBlocks_flatten_length line 67
  14. theorem OAI.DepthThreeLowerBound.inputBlockData_coefficients_eq_flatten line 73
  15. theorem OAI.DepthThreeLowerBound.hornerBitLists_ofFn line 87
  16. theorem OAI.DepthThreeLowerBound.hashByUpdates_inputBlocks line 103
  17. theorem OAI.DepthThreeLowerBound.hornerBitLists_inputBlocks line 110
  18. theorem OAI.DepthThreeLowerBound.hornerFrom_inputBlocks line 119
  19. theorem OAI.DepthThreeLowerBound.evaluateBits_eq_final_bit line 129
  20. theorem OAI.DepthThreeLowerBound.language_eq_final_bit line 140