OAI/Computability/DepthThree/LanguageBitConvolutionUpdates.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DepthThreeLowerBound.xorListAt line 8
  2. theorem OAI.DepthThreeLowerBound.xorListAt_length line 11
  3. theorem OAI.DepthThreeLowerBound.xorListAt_getD line 15
  4. theorem OAI.DepthThreeLowerBound.xorListAt_split line 24
  5. def OAI.DepthThreeLowerBound.convolutionUpdateRow line 31
  6. theorem OAI.DepthThreeLowerBound.convolutionUpdateRow_nil line 37
  7. theorem OAI.DepthThreeLowerBound.convolutionUpdateRow_step line 40
  8. theorem OAI.DepthThreeLowerBound.convolutionUpdateRow_length line 46
  9. theorem OAI.DepthThreeLowerBound.convolutionUpdateRow_getD line 54
  10. def OAI.DepthThreeLowerBound.convolutionUpdateRows line 74
  11. theorem OAI.DepthThreeLowerBound.convolutionUpdateRows_nil line 79
  12. theorem OAI.DepthThreeLowerBound.convolutionUpdateRows_step line 82
  13. theorem OAI.DepthThreeLowerBound.convolutionUpdateRows_length line 88
  14. theorem OAI.DepthThreeLowerBound.convolutionUpdateRows_getD line 96
  15. def OAI.DepthThreeLowerBound.convolveByUpdates line 117
  16. theorem OAI.DepthThreeLowerBound.convolveByUpdates_length line 121
  17. theorem OAI.DepthThreeLowerBound.convolutionUpdate_index_lt line 125
  18. theorem OAI.DepthThreeLowerBound.convolveByUpdates_getD line 130
  19. theorem OAI.DepthThreeLowerBound.convolveByUpdates_eq line 142