OAI/Computability/DepthThree/LanguageBitWord.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DepthThreeLowerBound.BitWord line 9
  2. def OAI.DepthThreeLowerBound.wordPoly line 11
  3. def OAI.DepthThreeLowerBound.wordXor line 14
  4. def OAI.DepthThreeLowerBound.wordGet line 17
  5. def OAI.DepthThreeLowerBound.shiftModulus line 20
  6. theorem OAI.DepthThreeLowerBound.wordGet_fin line 26
  7. theorem OAI.DepthThreeLowerBound.wordGet_of_lt line 30
  8. theorem OAI.DepthThreeLowerBound.wordGet_of_le line 34
  9. theorem OAI.DepthThreeLowerBound.wordGet_wordXor line 38
  10. theorem OAI.DepthThreeLowerBound.coeff_wordPoly line 42
  11. theorem OAI.DepthThreeLowerBound.coeff_wordPoly_fin line 47
  12. theorem OAI.DepthThreeLowerBound.wordPoly_injective line 51
  13. theorem OAI.DepthThreeLowerBound.wordPoly_zero line 59
  14. theorem OAI.DepthThreeLowerBound.wordPoly_xor line 64
  15. theorem OAI.DepthThreeLowerBound.degree_wordPoly_lt line 72
  16. theorem OAI.DepthThreeLowerBound.degree_wordPoly_lt_of_zero_tail line 76
  17. theorem OAI.DepthThreeLowerBound.degree_wordPoly_lt_of_tail_false line 83
  18. theorem OAI.DepthThreeLowerBound.inputPolynomialBits_eq_wordPoly line 93
  19. theorem OAI.DepthThreeLowerBound.shiftModulus_top line 96
  20. theorem OAI.DepthThreeLowerBound.shiftModulus_above line 101
  21. theorem OAI.DepthThreeLowerBound.wordPoly_shiftModulus line 108